Tecniche logiche e semantiche per computazioni funzionali e quantistiche
Profile Card Research project
Share this record with your favourite social network:
- Starting date
- September 22, 2008
- Duration (months)
- 24
- Person in charge
- Masini Andrea
Description
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.
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
- Simone Martini (responsabile)
- Bologna Scienze dell'Informazione Professore Ordinario
