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)
