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

Profile Card Research project

Share this record with your favourite social network: Facebook    Delicious    add to CiteUlike
Starting date
July 15, 2011

Duration (months)
24

Departments
Computer Science

Person in charge
Masini Andrea

Keyword
LAMBDA CALCOLO, SISTEMI DI TIPO, LOGICA

Description

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)

Sponsors:

PRIN VALUTATO POSITIVAMENTE
Funds: requested
Syllabus: COFIN - Progetti di Ricerca di Interesse Nazionale

Project participants

Alessandra Di Pierro
Associate Professor
Andrea Masini
Full Professor
ornamento
Top