Tecniche logiche e semantiche per computazioni funzionali e quantistiche

Starting date
September 22, 2008
Duration (months)
24
Managers or local contacts
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
dimensions:
(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.

Project participants

Andrea Masini
Full Professor

Collaboratori esterni

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

Activities

Research facilities

Share