2012/06/21 by Aloïs Brunel, Brunel, Aloïs, Antoine Madet +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1206.4833
arxiv created 2012/06/21 · arxiv updated 2012/06/22
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.