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.
