L'obiettivo dell'insegnamento è quello di introdurre i concetti fondamentali che legano la logica alla scienza dei calcolatori così che lo studente possa comprendere gli sviluppi moderni della logica computazionale.

Conoscenza e comprensione: lo studente conoscerà il concetto di Isomorfismo Curry-Howard e come esso si lega alla programmazione funzionale e alla logica intuzionista nell'ambito della correttezza dei programmi. Si introdurranno le logiche modali e si mostrerà come essere si legano alla rappresentazione della conoscenza.

Conoscenza e capacità di comprensione applicate: lo studente sarà in grado di scrivere funzioni in lambda calcolo, svolgere esercizi di tipizzazione di funzioni nell'ambito della correttezza dei programmi, stabilire la validità intuizionista di una formula che rappresenta una specifica ed estrarre dalla dimostrazione un programma in lambda calcolo. Lo studente sarà in grado di stabilire la soddisfacibilità di formule modali e modellare problemi scrivendo formule modali.

Capacità critiche di giudizio: saper scegliere tra diverse rappresentazioni della stessa funzione o della stessa tipizzazione; saper valutare divese formule che rappresentano la stessa conoscenza;

capacità di comunicare: saper definire correttamente i termini introdotti e distinguere cosa catturano le diverse definizioni date; enunciare anche con parole proprie ma in modo matematicamente corretto i teoremi principali mettondone in evidenza il significato;

capacità di proseguire lo studio in modo autonomo: essere in grado di cogliere che i meccanismi introdotti sono istanziabili anche ai linguaggi non funzionali; generalizzare la capacità di usare gli strumenti logici anche su logiche modali non viste la lezione e selezionare il framework logico più adatto per affrontare un problema nuovo.