Implicit computational complexity studies calculi and languages for which programs have a bounded complexity, in terms of computation time or of memory usage (polynomial, exponential ... in the size of the input). Various approaches have been used to ensure such bounds, in particular: Linear logic and its variants, rewriting systems and quasi-interpretations, linear types with resource types for functional languages. This theory would now need unifying elements, either with more general systems or with more semantical approaches.

Game semantics modelizes programming languages by interpreting types by two player games, programs by strategies for one of the players (the other one representing the evaluation environment) and interactions by plays. This explicit representation of interaction as a sequence of moves should allow to handle complexity at the semantic level.

Objectives:

  A. A semantic unifying approach for various systems of implicit computational complexity by game semantics;
  B. Extension of the results dealing with the existing systems, in particular linear logic;
  C. New and more general systems, or even a unifying framework subsuming several of the existing implicit complexity systems.

Expected results:

  Foundational results, in particular a semantics of polynomial games allowing to compare the existing systems of implicit complexity;
  Improvement of the use of implicit complexity systems for static verification of complexity, in particular with type systems.
  Finally the definition of new systems could allow to obtain more flexible verification methods.

Methodology:

A. Semantics. We will define a game semantics equipped with a notion of complexity for strategies, then a semantics of polynomial strategies. In a second step we will interpret polynomial implicit computational systems in this semantics.

B. Types, lambda-calculus and proof-nets. We will proceed with the study of variants of Linear logic with bounded complexity as type systems for lambda-calculus: we will be interested in type inference, in the applications to optimal reduction and in the extension with recursive types.

C. Implicit complexity and expressivity. Using the results of parts A and B we will try to define a more general system subsuming several of the existing systems, for instance Hofmann’s linear types and a system of polynomial linear logic. Finally we will consider complexity in the BSS model over an arbitrary structure and the adaptation to this setting of the systems of implicit complexity with higher-order.