30214 - Logical basis of Computer Science

Learning outcomes

At the end of this course, students have acquired the logical foundations of areas of theoretical computer science such as ambda-calculus, rewriting systems, computational complexity, database theory and formal methods. He is able to encode programming constructs in lambda-calculus, to describe simple algorithms in logical form, to express queries to databases in predicative form and to specify properties of reactive systems as formulas of temporal logic.

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.

 

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 (minimal introduction to System-F). Minimal introduction to 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 Formal Methods

LTL and CTL: syntax and semantics. Reactive systems and their verifications. Model Checking.

4. Logic and Artifcial Intelligence

Epistemic logic: syntax, semantics, applications

 

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.  http://people.cs.umass.edu/~immerman/book/descriptiveComplexity.html

- 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 Fabio Zanasi