Advertisement
Published in:
2012 | OriginalPaper | Chapter
Indexed Realizability for Bounded-Time Programming with References and Type Fixpoints
Authors : Aloïs Brunel, Antoine Madet
Published in: Programming Languages and Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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 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, indexing and is 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 of typed programs.