- Docente: Claudio Sacerdoti Coen
- Credits: 6
- SSD: MAT/01
- Language: Italian
- Teaching Mode: Traditional lectures
- Campus: Bologna
-
Corso:
Second cycle degree programme (LM) in
Philosophical Sciences (cod. 8773)
Also valid for Second cycle degree programme (LM) in Computer Science (cod. 8028)
Second cycle degree programme (LM) in Physics (cod. 9245)
Learning outcomes
At the end of the course the student will know the logic bases of computer science. Particular attention will be given to the lambda-calculus and its meta-theory, to the correspondence between proof and programs, and to various flavours of typed lambda-calculi. The student will be able to write simple numeric functions in the lambda-calculus and to derive their types.
The second module of the course is devoted to applications of logic to computer science in several domains like databases, artificial intelligence, formal methods and complexity theory.
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