Teorie dei Tipi. Si studiano in particolare le teorie dei tipi soggiacenti ai Logical Frameworks, linguaggi di programmazione fortemente tipati, che combinano due modalità computazionali tra loro duali: la riduzione e il pattern-matching. Sono di fatto anche teorie fondazionali in logica costruttiva, che hanno recentemente ricevuto molta attenzione anche nel contesto della Geometria Algebrica, dando origine alle Homotopy Type Theory. Questo filone è strettamente legato a tematiche di ricerca nell’area dei Linguaggi e dei Metodi Formali.

Fondamenti della Semantica della Computazione e dei Processi. Nella Semantica c’è una dualità tra processi e computazioni, tra sistemi di evoluzione (behavioural semantics) e sistemi di riduzione (reduction semantics), che non è stata ancora perfettamente chiarita. L’obiettivo è la composizionalità al fine di permettere una trasparenza referenziale. Da un lato ci sono le semantiche denotazionali, iniziali, bottom-up da analizzare attraverso principi di induzione, dall’altro le semantiche operazionali, finali, top-down, da analizzare attraverso principi di co-induzione. Queste ultime si collegano agli iperinsiemi, e alle bisimulazioni che furono introdotte indipendentemente in vari settori della logica nei primi anni ’80 e da Forti e Honsell nella Teoria degli Insiemi nel 1982. Riprendendo proprio questi spunti originari, è stata recentemente studiata e implementata in LLFP la Teoria degli Insiemi di Fitch, una teoria molto vicina alla teoria ideale di Cantor. Ancorché paraconsistente, non è banale in quanto consente solamente dimostrazioni in forma normale. È però particolarmente appropriata per la verifica di programmi perché molto espressiva, in quanto permette di ragionare liberamente con il Principio di Comprensione e di posticipare la verifica di normalizzazione a quando è davvero necessario. Inoltre, opportuni quozienti dei term models della Teoria di Fitch danno interessanti iperuniversi, ad esempio un’ulteriore descrizione degli iperinsiemi finitari. Strumenti tipici della semantica denotazionale, i domini di Scott, sono usati per descrivere l’analisi costruttiva. In particolare si affronta il problema di definire in maniera costruttiva l’operatore differenziale, scegliendo opportune rappresentazioni per i numeri reali e per le funzioni su queste.

Semantica dei Giochi e Giochi per la Semantica dei Linguaggi di Programmazione e dell’Interazione. Negli anni ’90, J.-Y. Girard, ha introdotto la Geometria delle Interazioni, che permette di studiare in modo rivoluzionario la dualità tra semantica operazionale e semantica denotazionale, perché introduce uno spazio concettualmente nuovo intermedio tra le due. Dalla Geometria delle Interazioni è derivata la semantica dei giochi che ha permesso di dare modelli fully-abstract per linguaggi di programmazione funzionali con svariate sorte di primitive anche non-funzionali. Attraverso il concetto di gioco, come alternanza di interazioni, sono emerse inaspettate connessioni della teoria della computazione con svariati rami dalla logica alla fisica teorica. Abramsky e Lenisa studiarono nei primi anni 2000 un modello di Geometria delle Interazioni che si è dimostrato particolarmente adatto per discutere la computazione reversibile. L’obiettivo specifico più recente è quello di studiare le proprietà dei pattern-matching automata che danno un modello della Logica Combinatoria Lineare. In particolare è stato introdotto un lambda-calcolo esteso con una disciplina di tipi dotati di un’intersezione non simmetrica, i cui tipi principali permettono di derivare la semantica della Geometria delle Interazioni per la logica combinatoria lineare in modo diretto. Questo approccio è molto promettente e potrebbe offrire la chiave per comprendere la natura profonda di questo regno intermedio, composizionale eppure operazionale, che si chiama Geometria delle Interazioni.