Fondamenti Matematici di Estensioni Quantitative del Lambda-calcolo e dell'Interazione (PRIN 2009)

Data inizio
15 luglio 2011
Durata (mesi) 
24
Dipartimenti
Informatica
Responsabili (o referenti locali)
Masini Andrea
Parole chiave
LAMBDA CALCOLO, SISTEMI DI TIPO, LOGICA

L'attività dell'unità di Verona sarà orientata allo studio di nuovi calcoli quantitativi (lambda-calcoli, logiche, etc.) e di semantiche appropriate. Un'enfasi particolare verrà data agli approcci probabilistici, quantistici, differenziali e sensibili alle risorse. Al fine di definire i temi dell'intero proggetto, il MODELLO A fa riferimento ad uno spazio tridimensionale. Gli assi di tale spazio sono:
“Metodi”, “Paradigmi Computazionali” e “Linguaggi di programmazione paradigmatici”.
Abbiamo individuato i seguenti punti lungo ciascun asse:
Metodi: sistemi di tipo, teoria dei domini, teoria della dimostrazione strutturale, metodi algebrici, geometria dell'interazione, reti di prova;
Paradigmi Computazionali: probabilistico, quantistico, sequenziale;
Linguaggi di programmazione paradigmatici: lambda-calcolo, calcoli della famiglia di PCF, lambda-calcolo differenziale, calcolo di risorse.
Usando i punti appena definiti, possiamo associare ad ogni goal (linea di ricerca) una tripla astratta di punti. Ogni obiettivo della ricerca sarà poi ulteriormente strutturato in sotto-goal, ognuno corrispondente ad un raffinamento del goal in questione.
Goal and sottogoal dell'unità di ricerca:
1. Calcoli probabilistici, tipi, e loro strutture semantiche:
(sistemi di tipo AND teoria dei domini, probabilistico, lambda-calcolo AND calcoli della famiglia di PCF)
Collaborazione: Bologna
Sottogoal:
(a) Lambda-calcolo probabilistico: (NIL, probabilistico, lambda-calcoli)
(b) Tipi probabilistici: (sistemi di tipo, probabilistico, lambda-calcolo AND calcoli della famiglia di PCF)
(c) Semantica denotazionale di calcoli della famiglia di PCF probabilistico: (teoria dei domini, probabilistico, calcoli della famiglia di PCF) (d) Spazi coerenti probabilistici: (sistemi di tipo, probabilistico, lambda-calcoli AND calcoli della famiglia di PCF)
2. Calcoli quantistici:
(geometria dell'interazione AND reti di prova AND teoria della dimostrazione strutturale, quantistico, lambda-calcoli) Collaborazione: Bologna
Sottogoal:
(a) lambda-calcoli quantistici: geometria dell'interazione AND reti di prova, quantistico, lambda-calcoli)
(b) Calcoli logici per la computazione quantistica: (teoria della dimostrazione strutturale, quantistico, NIL)
3. Strutture matematiche per calcoli delle risorse e calcoli differenziali:
(algebraic methods AND teoria dei domini, sequential, lambda-calcolo differenziale AND calcolo di risorse)
Collaborazioni: Torino, Roma
Sottogoal:
(a) Fondamenti algebrici per calcoli delle risorse e calcoli differenziali: (metodi algebrici, NIL, lambda-calcolo differenziale AND calcolo di risorse) (b) Modelli del lambda-calcolo non tipato provanienti dai calcoli di risore e calcoli differenziali:
(teoria dei domini, sequenziale, lambda-calcolo differenziale AND calcolo di risorse)

Enti finanziatori:

PRIN VALUTATO POSITIVAMENTE
Finanziamento: richiesto
Programma: COFIN - Progetti di Ricerca di Interesse Nazionale

Partecipanti al progetto

Alessandra Di Pierro
Professore associato
Andrea Masini
Professore ordinario

Attività

Strutture