- Docente: Simone Martini
- Credits: 6
- SSD: MAT/01
- Language: Italian
- Moduli: Simone Martini (Modulo 1) Claudio Sacerdoti Coen (Modulo 2)
- Teaching Mode: In-person learning (entirely or partially) (Modulo 1); In-person learning (entirely or partially) (Modulo 2)
- Campus: Bologna
-
Corso:
Second cycle degree programme (LM) in
Computer Science (cod. 8028)
Also valid for Second cycle degree programme (LM) in Philosophical Sciences (cod. 8773)
Learning outcomes
Knowing the logical foundations of Computer Science, as expressed by the lambda-calculus and its relations to proofs in natural deduction.
Course contents
The course focusses on the
proofs-as-programs correspondence (also know as Curry-Howard
correspondence).
The first part of the course is an
introduction to the type free lambda calculus: syntax, reduction,
algorithmic completeness, confluence,
separability.
The second part of the course invetigates
typed lambda calculi with increasing expressive power, with special
stress on the logics they correspond to: simply typed lambda
calculus and propositional intuitionistic logic, system T, system
F, dependent type systems and the Caclulus of Constructions. We
will discuss the expressive power of these languages and some
techniques for proving their normalization.
Readings/Bibliography
H.Barendregt. Lambda Calculi with Types.
Handbook of Logic in Computer Science, Volumes 1. Clarendon, 1992
Available online at
http://www.cs.unibo.it/~martini/FLI/barendregt.pdf
.
J.-Y. Girard. Proof and Types.
Cambridge Tracts in Theoretical Computer Science. Cambridge
University press. 1989. Out of print. Available online
at
http://www.paultaylor.eu/stable/prot.pdf
.
Teaching methods
Lectures at the blackboard
Assessment methods
Oral examination
Teaching tools
Lectures at the blackboard.
Office hours
See the website of Simone Martini
See the website of Claudio Sacerdoti Coen