UNIVERSITÀ DEGLI STUDI DI MILANO

Scuola di Dottorato in Informatica

via Comelico 39/41, 20135 Milano


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:


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 – 17z30<.p>


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

Programma della II parte:

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