- Docente: Claudio Sacerdoti Coen
- Credits: 6
- SSD: MAT/01
- Language: Italian
- Moduli: Claudio Sacerdoti Coen (Modulo 1) Ugo Dal Lago (Modulo 2)
- Teaching Mode: Traditional lectures (Modulo 1) Traditional lectures (Modulo 2)
- Campus: Bologna
-
Corso:
Second cycle degree programme (LM) in
Computer Science (cod. 8028)
Also valid for Second cycle degree programme (LM) in Philosophical Sciences (cod. 8773)
Second cycle degree programme (LM) in Physics (cod. 9245)
Learning outcomes
At the end of the course, the student knows the logical and formal basics of computer science. More specifically, the lambda-calclulus and its theory, the correspondence between programs and proofs, the typed lambda-calculus, system T and system F. He or she can write simple numerical functions in the lambda-calculus, and derive their types.
Course contents
First module:
1. Propositional and First-Order Logic (recall)
Syntax, Semantics, Soundness and Completeness, Undecidability of First Order Logic
2. Untyped Lambda Calculus
Syntax and operational semantics. The lambda-calculus as a programming language: evaluation strategies and encodings of data types; Turing completeness
3. Meta-theory of untyped lambda calculus
Confluence; Bohm's separation theore
4. Simply typed lambda-calculus and Curry-Howard isomorphism
Curry's style and Church's style syntaxes. Isomorphism with propositional minimal logic. Type checking and type inference algorithms.
5. Meta-theory of simply typed lambda-calculus
Weak and strong normalization theorems
6. Curry-Howard isomorphism and extensions to the typing system
Products and coproduts, empty and singleton types. Parametric polymorphisms (System-F). Dependent types and Hindley-Milner polymorphisms.
Second module:
1. Logic and Databases
Relational algebra, FO as Query Language, Cilindrical Algebras, Implementation aspects
2. Logic and Computational Complexity
Finite structures and decision problems. NP and PSPACE characterization via first order logics. SAT Solving.
3. Logic and Artifcial Intelligence
Epistemic logic: syntax, semantics, applications
4. Logic and Formal Methods
LTL and CTL: syntax and semantics. Reactive systems and their verifications. Model Checking.
Readings/Bibliography
First module:
- H.P. Barendregt: The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Available on-line at http://www.cs.unibo.it/~sacerdot/fli1718/barendregt.pdf
- J.Y. Girard, Y. Lafont, P. Taylor: Proof and Types. Available on-line at http://www.paultaylor.eu/stable/Proofs+Types.html
The topics in the first book (by Barendregt) that we will study in the course are also explained in the following notes by the same author:
http://www.cs.unibo.it/~sacerdot/fli1718/IntroductionToLambdaCalculus.pdf
Second module:
- N. Immerman. Descriptive Complexity. Springer, 1999. [ WebPage ]
- J. Ullman. Principles of database and knowledge-base systems, Volume I. Computer Science Press, 1990.
- E. Clarke and O. Grumberg and D. Peled. Model Checking. MIT Press, 1999.
Teaching methods
The course is in the first semester. All lessons are frontal lessons, in presence and on-line, unless sanitary requirement force on-line lessons only.
All the topics are presented, with detailed proofs of most theorems.
Depending on the arguments, either slides or the blackboard will be used.
Assessment methods
Oral exam.
Teaching tools
Slides and pointers to scientific articles and books freely downloadable from the Web.
Office hours
See the website of Claudio Sacerdoti Coen
See the website of Ugo Dal Lago