CORSO DI DOTTORATO

Area Tematica

Logica Computazionale

Il Prof. Dale Miller

INRIA Saclay & Laboratoire d’Informatique, LIX

Ecole polytechnique, PALAISEAU Cedex, FRANCE,

terrà un corso dal titolo

Proof Search and Computation.

Scopo e contenuto: illustrare il ruolo della logica nella specifica delle computazioni e della "proof search" come approccio alla programmazione logica. Il corso sarà suddiviso in due parti:

1. Fondamenti, lezioni tenute da Dale Miller

2. Applicazioni, lezioni ed esercitazioni tenute da A. Momigliano e M.Ornaghi

Pre-requisiti: conoscenza di base di logica

Programma della I parte:

• 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]).

References and Links

[BEATCS08] Formalizing operational semantic specifications in logic, by Dale Miller. Concurrency Column of the Bulletin of the EATCS, edited by Luca Aceto. 2008.

[LPAR07] Least and greatest fixed points in linear logic by David Baelde and Dale Miller. LPAR 2007: Logic for Programming Artificial Intelligence and Reasoning

[LN2010] Proof Search and Computation, by Dale Miller.(draft, January 2010).

15/03/2010 Aula Beta - Via Comelico 39/41 14:30 – 16:30

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

Homepage del corso: https://www.lix.polytechnique.fr/Labo/Dale.Miller/milan2010.html

Programma della II parte:

• 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].

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

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

Docente di Riferimento: Prof. Mario Ornaghi