Indexed realizability for bounded-time programming with references and type fixpoints

TL;DR

This paper introduces a realizability semantics for a higher-order functional language with recursive types and store, based on linear logic, enabling precise complexity bounds and termination proofs for PTIME functions.

Contribution

It develops a novel realizability approach combining biorthogonality, step-indexing, and quantitative analysis for a PTIME-characterizing language with recursive types.

Findings

Semantic proof of termination for typed programs

Derivation of bounds on computational steps

Characterization of PTIME functions via linear logic fragment

Abstract

The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity class. We here present a realizability semantics for a higher-order functional language based on a fragment of linear logic called LAL which characterizes the complexity class PTIME. This language features recursive types and higher-order store. Our realizability is based on biorthogonality, step-indexing and is moreover quantitative. This last feature enables us not only to derive a semantical proof of termination, but also to give bounds on the number of computational steps needed by typed programs to terminate.