Tecniche logiche e semantiche per computazioni funzionali e quantistiche

Data inizio
22 settembre 2008
Durata (mesi) 
Responsabili (o referenti locali)
Masini Andrea

We will develop and apply techniques in the areas of (fragments of) linear logic and of denotational
semantics, to the characterization and veri cation of resource usage of programs.
Moreover, we will investigate languages for the quantum model of computation.
We recall from the general plan of the project (Modello A), that the research will focus on
the two goals:
1. foundational techniques for the analysis and veri cation of runtime properties of programs,
(e.g., new formal systems, type systems, etc.);
2. computational theories modelling the correct interaction with the environment (e.g., unifying
theories explaining with new tools the existing languages).
We therefore classify the speci c research to be performed in Bologna according to those two
(1) Curry-Howard isomorphism and complexity classes;
(1) Type systems and type inference for resource certi cation;
(1) Intersection types and execution time of programs;
(2) Dynamic semantics of linear logic and its \light" fragments (geometry of interaction, game
semantics, context semantics, realizability);
(1) and (2) Optimal lambda-reduction and complexity;
(1) Quantum model of computation (languages, types and complexity);
(2) General formal frameworks for the construction of lambda models;
(2) Global semantical properties of lambda-models.

Partecipanti al progetto

Andrea Masini
Professore ordinario

Collaboratori esterni

Simone Martini (responsabile)
Bologna Scienze dell'Informazione Professore Ordinario