This course will present the "proof search" approach to specifying and reasoning about computation.
Prerequisites: basic background of first-order logic. Familiarity with the sequent calculus is useful but not strictly necessary.
This course will take place during the two weeks 15 - 26 March 2010, within the Dipartimento di Scienze dell'Informazione, Università degli studi di Milano. Official flier.
The first week will include 10 hours of lectures by Dale Miller. These lectures will focus on foundational topics in proof theory and computational logic. In particular:
The first three lectures will be taken from the lecture notes [LN2010] and will cover the basics of sequent calculus and its uses in the specification of logic programming languages.
The fourth lecture will show how logic specifications can be applied to the specification of structured operational semantics (following the material in [BEATCS08]).
The fifth lecture will focus on the role of fixed points in the specification and reasoning of computation (following [LPAR07]).
15/03/2010 Aula Beta - Via Comelico 39/41 14:30 - 16:30
The second week of lectures will also be 10 hours of lectures by Alberto Momigliano and Mario Ornaghi, and will focus on applications and on exercises.
The first three lectures will address the use of lambda.tree syntax and the proof search approach to model checking with Bedwyr [MFS], exemplifying it with the specification of a lazy functional programming language, namely its static and operational semantics and the related notion of contextual equivalence.
The last two lectures will introduce interactive theorem proving over this syntax with the Abella system [2LEV] and explore some case studies, such as formally verifying type preservation, and leading to congruence of contextual equivalence [ASOS,OPT].
22/03/2010 Auletta 5 - Via Comelico 39/41 10:00 – 12:00
23/03/2010 Auletta 5 - Via Comelico 39/41 10:00 – 12:00
24/03/2010 Auletta 5 - Via Comelico 39/41 10:00 – 12:00
25/03/2010 Auletta 4 - Via Comelico 39/41 10:30 – 12:30
26/03/2010 Auletta 5 - Via Comelico 39/41 10:00 – 12:00
Students wanting more material related to the background of this class can find additional references below.
Logic for Computer Science: Foundations of Automatic Theorem Proving, by Jean Gallier, Wiley, pp. 511 (1986). This book is now out of print but available for free download.
Proofs and Types by Jean-Yves Girard, Paul Taylor, and Yves Lafont. Cambridge University Press. This book is now available from a number of sources for free download. Try the link above to find locations for downloading.