A graduate course:
Proof Search and Computation

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.

Venue

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.

Week 1

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:

Times and places for Week 1

15/03/2010 Aula Beta - Via Comelico 39/41 14:30 - 16:30
16/03/2010 No class, but there will be an informal logic workshop in Aula Riunioni 2 Piano, 15:00 – 18:00. Here is the provisional program.
17/03/2010 Sala lauree - Via Comelico 39/41 14:30 - 17:30
18/03/2010 Sala lauree - Via Comelico 39/41 14:30 - 17:30
19/03/2010 Sala lauree - Via Comelico 39/41 14:30 - 17:30

References for Week 1

[BEATCS08]
Formalizing operational semantic specifications in logic, by Dale Miller. Concurrency Column of the Bulletin of the EATCS, edited by Luca Aceto. October 2008. (pdf).
[LPAR07]
Least and greatest fixed points in linear logic by David Baelde and Dale Miller. LPAR 2007: Logic for Programming Artificial Intelligence and Reasoning (pdf). Extended version: pdf.
[LN2010]
Proof Search and Computation, by Dale Miller. pdf format (draft dated February 2010).

Week 2

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.

Provisional times and places for Week 2

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

References for Week 2

[MFS]
Mixing Finite Success and Failure in an Automated Prover, by Alwen Tiu, Gopalan Nadathur and Dale Miller. Proceedings of ESHOL'05. (pdf).
[2LEV]
A two-level logic approach to reasoning about computations, by Andrew Gacek, Dale Miller, and Gopalan Nadathur. Draft. (pdf).
[ASOS]
Reasoning in Abella about structural operational semantics specifications, by Andrew Gacek, Dale Miller, and Gopalan Nadathur. Electronic Notes in Theoretical Computer Science Volume 228, Jan 2009, (pdf).
[OPT]
Operationally-Based Theories of Program Equivalence, by Andrew Pitts. Semantics and Logics of Computation, (Cambridge University Press, 1997). (pdf).

Additional References and Links

Students wanting more material related to the background of this class can find additional references below.