- Docente: Ugo Dal Lago
- 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)
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
- Logic and Computational Compelxity: Finite Model Theory, Fagin's Theorem, Immerman-Vardi Theorem.
- Logic and Databases: Relational Algebra, Relational Calculus, The correspondence Theorem.
- Logic and System Verification: Kripke Structures, CTL*, CTL, LTL. Decidability of the Model Checking Problem.
Readings/Bibliography
Joseph Y. Halpern, Robert Harper, Neil Immerman, Phokion G. Kolaitis, Moshe Y. Vardi, Victor Vianu. On the unusual effectiveness of logic in computer science. Bulletin of Symbolic Logic 7(2) pages 213--236. 2001.
Teaching methods
Class Lectures.
Assessment methods
Written Exams.
Office hours
See the website of Ugo Dal Lago
See the website of Claudio Sacerdoti Coen