a.a. 2025/26

Responsabile didattico: Emanuele D'Osualdo

Periodo: annuale

Durata: 28 ore

Programma: 

1. Cenni Storici: Logica Matematica, Paradosso di Russel, Lambda-calcolo, CIC.

2. Simple types, Isomorfismo di Curry-Howard

3. The Calculus of Constructions

4. Basi di Rocq: Types, Prop, Programmazione Funzionale

5. Polimorfismo e ordine superiore

6. Inductive Data Types

7. Tattiche e Automazione

8. Formalizzazione di un linguaggio di programmazione imperativo

9. Equivalenze di programmi

10. Formalizzazione di Hoare Logic

11. Formalizzazione di Sistemi di Tipi

12. Simply Typed Lambda Calculus e normalizzazione

13. Mutable References e Cenni di Separation Logic

Corsi a.a. 2025/2026