Indexed realizability for bounded-time programming with references and type fixpoints
Logic in Computer Science
2012-06-22 v1 Programming Languages
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.
Cite
@article{arxiv.1206.4833,
title = {Indexed realizability for bounded-time programming with references and type fixpoints},
author = {Aloïs Brunel and Antoine Madet},
journal= {arXiv preprint arXiv:1206.4833},
year = {2012}
}