Objectives

The Collodi project revolves around two major research axes:

1. foundations of computational complexity, with applications to the analysis and certification of resource use in programming;
2. development of models of concurrent and probabilistic computation.

The connection between these two apparently unrelated areas is in the common methodology proposed, which is mostly based on proof theory (especially linear logic) and the mathematical fields associated with it, which are traditionally combinatorics, algebra, topology, category theory, and, less traditionally, analysis and measure theory.

In particular, our aim is to use ludics and differential linear logic, two theories belonging to the offspring of linear logic proof theory, to provide new foundations and richer, deeper structure to the two above mentioned domains.

Here is a synthetic description of some of the aspects we want to develop:

• a monistic logical approach to complexity;
• denotational semantics and implicit computational complexity;
• resource analysis in differential linear logic;
• concurrent processes and differential linear logic;
• probabilistic differential linear logic;
• differential linear logic, monism, and ludics.