We will develop and apply techniques in the areas of (fragments of) linear logic and of denotational
semantics, to the characterization and verication 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 verication 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 specic 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 certication;
(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.