30214 - Logical basis of Computer Science

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

Teaching methods

The course is in the first semester. All lessons are frontal lessons.

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