Lambda-Calcolo e Teoria dei Tipi
Scuola Estiva AILA
Agosto 2018

---

Il corso si prepone di introdurre gli studenti al lambda-calcolo e alla teoria dei tipi. In particolare, l'obiettivo sarà quello di capire se la teoria dei tipi possa offrire gli strumenti giusti a controllare l'espressività del lambda-calcolo, così da renderlo capace di caratterizzare classi di funzioni e di problemi.

Syllabus

• Introduzione al Corso
  
• Il Lambda-Calcolo Non Tipato: Termini, Riduzione, Confluenza, Espressività
  
• I Tipi Semplici e la Logica Intuizionista
  
• La Logica Classica e al Second'Ordine
  
• La Complessità Implicita e la Logica Lineare
  

Orario delle Lezioni

• Lunedì 27 Agosto 2018: 9.00-11.00
  
• Martedì 28 Agosto 2018: 11.00-13.00
  
• Mercoledì 29 Agosto 2018: 9.00-11.00
  
• Giovedì 30 Agosto 2018: 11.00-13.00
  
• Venerdì 31 Agosto 2018: 9.00-11.00
  
• Venerdì 31 Agosto 2018: 14.30-16.30
  

Bibliografia

[1]	M. H. B. Sorensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism. Volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006.
[2]	U. Dal Lago. A Short Introduction to Implicit Computational Complexity. ESSLLI 2010 Lecture Notes, 2010. [pdf]

Materiale Didattico
Slides, Parte I (28/8/2018) [ pdf ]
Slides, Parte II (28/8/2018) [ pdf ]
Slides, Parte III (26/8/2018) [ pdf ]
Slides, Parte IV (3/9/2018) [ pdf ]