Logica e Informatica

(Descrizione provvisoria)

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:

1. I teoremi principali sulla logica considerati dal punto di vista della sintassi trascendentale,  analitico e sintetico in logica
2. Rappresentazione geometrica (attraverso proof-nets) delle leggi della grammatica categoriale, geometria dei sillogismi
3. Quantificazione e oggetto generico, dimostrazioni e tipi nella logica del secondo ordine
4. Nuovi approcci in economia e in scienze della formazione, ispirati dalla sintassi trascendentale.
5. 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.
6. Uso della proprietà  di connessione delle reti di prova per caratterizzarle mediante un unico punto della loro espansione di Taylor.
7. Estensione del paradigma di costruzione delle dimostrazioni ricorrendo all'uso delle reti dimostrative del frammento moltiplicativo ed additivo della logica lineare.
8. 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.
9. 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.

Membri:

Collaborazioni