Un logical framework è un formalismo che permette di rappresentare una logica, o più in generale un sistema formale deduttivo, in una teoria di tipi di ordine superiore, in modo tale che la dimostrabilità di una formula nella logica originale corrisponde ad un problema di “type inhabitation" nel logical framework. Questo approccio è stato utilizzato con successo per l’implementazione di sistemi di prova semi-automatizzati, chiamati “proof assistant” o "dimostratori interattivi". Molti strumenti recenti, come Coq, Isabelle, Twelf, si basano su questa idea. All’interno di un logical framework coesistono definizioni matematiche, algoritmi eseguibili, teoremi e relative dimostrazioni, ed un ambiente interattivo che tiene traccia dello stato corrente delle prove, e le aggiorna in funzione dei comandi (tattiche) impartiti dall'utente. Essendo le dimostrazioni una parte integrale del formalismo, attraverso l' isomorfismo di Curry Howard si può ottenere una efficace integrazione tra specifica e ragionamento.

Questo corso mira a dare le basi dei logical framework, e più specificatamente verranno esaminati:
(1) strumenti di base di logica per fare e giustificare affermazioni precise sui programmi;
(2) l'uso di assistenti di prova per costruire argomentazioni logiche rigorose;
(3) l'idea di programmazione funzionale, sia come metodo di programmazione sia come ponte tra la programmazione e la logica;
(4) tecniche formali per ragionare sulle proprietà di programmi specifici (ad esempio, il fatto che un ciclo termina su tutti gli ingressi, o che una funzione selezione o un compilatore obbedisce una particolare specifica).