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 lambda-calculus, rewriting systems, database theory and formal methods aimed at program analysis and verification. The students are able to encode programming constructs in lambda-calculus, to express queries to databases in predicative form, to specify properties of reactive systems as formulas of temporal logics and to describe communication protocols as formulas of substructural logics.

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. Modeling and static analysis of distributed systems
Syntax and operational semantics of the pi calculus; linear logic; linear logic as type system for the pi calculus; meta-theory of the typed pi-calculus

 

2. 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).

- J.Y. Girard, Y. Lafont, P. Taylor: Proof and Types. Available on-line at http://www.paultaylor.eu/stable/Proofs+Types.html

Together the two books cover all the topics presented during the course.

Second module: 

- E. Clarke and O. Grumberg and D. Peled. Model Checking. MIT Press, 1999.
|

The text only covers topics related to "Logic and Formal Methods".
As for "Modeling and Static Analysis of Distributed Systems", the instructor will provide supplementary teaching materials.

Teaching methods

The course takes place in the first semester and consists of in-person lectures in the classroom.

During the lectures, all course topics are thoroughly covered, with examples provided for each definition and detailed proofs of most theorems.

Depending on the topic being covered, the instructor will either use pre-prepared slides or will write the slides interactively on a tablet and share them with students at the end of the lecture. The latter approach is more suitable for complex proofs, as it allows the instructor to dynamically adapt the explanation to the students’ level of understanding and to proceed more slowly through the material.

Assessment methods

The exam is a single assessment for both modules and consists of an oral examination. The oral exam covers all topics discussed during the lectures. For each module, the respective instructor will ask questions for approximately 10 minutes. The questions are aimed at verifying the student’s actual understanding of the topics presented, as well as their significance. The evaluation will consider the accuracy of the answers and definitions, the clarity and conciseness of the explanations, and the ability to make connections between the different topics covered. The final grade is agreed upon by both instructors at the end of the questioning. The grade is recorded immediately, unless the student is uncertain about accepting it. In that case, the decision must be made within the following 24 hours.

Students with disabilities and Specific Learning Disorders (SLD) have the right to special accommodations according to their condition, following an assessment by the Service for Students with Disabilities and SLD. Please do not contact the teacher but get in touch with the Service directly to schedule an appointment. It will be the responsibility of the Service to determine the appropriate adaptations. For more information, visit the page:

https://site.unibo.it/studenti-con-disabilita-e-dsa/en/for-students

Teaching tools

The slides presented or written interactively during the lectures will be provided. Additionally, references to scientific articles and freely accessible educational texts available online will be shared.

Office hours

See the website of Claudio Sacerdoti Coen

See the website of Luca Padovani