La ricerca si colloca entro gli sviluppi e le applicazioni della logica lineare, nell’ambito della collaborazione esistente da molti anni con gruppi di ricerca in Italia, in Francia , in Gran Bretagna, in Germania, in Giappone, in USA e in Brasile. Nelle applicazioni informatiche, la ricerca risponde ad esigenze avvertite presso i più importanti centri internazionali di ricerca.
La ricerca riguarda le seguenti tematiche:
sintassi trascendentale, ludica, logica del secondo ordine, espansione di Taylor delle reti di prova connesse, approccio semantico alla proprietà di forte normalizzazione, programmazione e costruzione (o ricerca) delle dimostrazioni, linguaggi di programmazione funzionale e loro valutazione parallela e distribuita, sistemi logici per la complessità computazionale implicita.
Alcuni degli obiettivi correnti sono:
- I teoremi principali sulla logica considerati dal punto di vista della sintassi trascendentale, analitico e sintetico in logica
- Rappresentazione geometrica (attraverso proof-nets) delle leggi della grammatica categoriale, geometria dei sillogismi
- Quantificazione e oggetto generico, dimostrazioni e tipi nella logica del secondo ordine
- Nuovi approcci in economia e in scienze della formazione, ispirati dalla sintassi trascendentale.
- Analisi della proprietà di forte normalizzazione nell’ambito generale delle reti di prova non tipate, usando gli invarianti forniti dall’interpretazione abituale nel modello relazionale.
- Uso della proprietà di connessione delle reti di prova per caratterizzarle mediante un unico punto della loro espansione di Taylor.
- Estensione del paradigma di costruzione delle dimostrazioni ricorrendo all’uso delle reti dimostrative del frammento moltiplicativo ed additivo della logica lineare.
- Descrizione di famiglie di macchine astratte per la riduzione ottimale, usando la struttura algebrica degli “streams” (J.J.M.M. Rutten ) e la Geometria dell’Interazione per la Logica Lineare nella sua variante (Danos-Pedicini-Regnier) denominata Directed Virtual Reduction.
- Estensioni del sistema TFA (typeable functional assembly; Cesena- Pedicini – Roversi.) per un sistema di programmazione dichiarativa in cui l’aritmetica per i campi finiti possa essere programmata in un ambiente che certifica la complessità polinomiale dei programmi.