Master's degree in Computer Science and Engineering

Logic in computer science

Course code
Name of lecturer
Andrea Masini
Andrea Masini
Number of ECTS credits allocated
Academic sector
Language of instruction
II semestre dal Mar 1, 2021 al Jun 11, 2021.

Lesson timetable

Go to lesson schedule

Learning outcomes

The course aims to provide knowledge of classical and intuitionisitic logic (propositional and first order), and of lambda calculus and type theory. At the end of the course the students must demonstrate to have the necessary knowledge to reason within a formal logical system, both in a classical and intuitionisitic setting. This knowledge will allow the student to: i) carry out formal proofs with a deductive system; ii)reasoning with axiomatic systems. Moreover the students will have to know how to transfer the theoretical notions learned in logical contexts typical of computer science, such as the type systems for functional languages. Students will be able to continue their studies in the field of computer science logic.


1.Propositional logic:
-propositions and connectives
-natural deduction
-soundness and completeness
2. Predicate logics:
-similarity types
-natural deduction
-soundness and completeness
3. normalization in natural deduction.
4. confluence.
5. basic model theory
- equivalence,
- isomporphism.
6. lambda calculus without types and with types.
7. the sequent calculus and the cut elimination theorem.
8, peano Arithmetic
-first and second incompleteness theorems

Reference books
Author Title Publisher Year ISBN Note
Jean Louis Krivine, Rene Cori Lambda-calculus, Types and Models Ellis Horwood 1993 978-0130624079
van Dalen, Dirk Logic and Structure. (Edizione 5) Springer 2013 978-1-4471-4557-8

Assessment methods and criteria

Written examination

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234