Realizability models and implicit complexity

8 years 1 months ago
Realizability models and implicit complexity
New, simple, proofs of soundness (every representable function lies in a given complexity class) for Elementary Affine Logic, LFPL and Soft Affine Logic are presented. The proofs are obtained by instantiating a semantic framework previously introduced by the authors and based on an innovative modification of realizability. The proof is a notable simplification on the original already semantic proof of soundness for the above mentioned logical systems and programming languages. A new result made possible by the semantic framework is the addition of polymorphism and a modality to LFPL, thus allowing for an internal definition of inductive datatypes. The methodology presented proceeds by asboth abstract resource bounds in the form of elements from a resource monoid and resource-bounded computations to proofs (respectively, programs).
Ugo Dal Lago, Martin Hofmann
Added 15 May 2011
Updated 15 May 2011
Type Journal
Year 2011
Where TCS
Authors Ugo Dal Lago, Martin Hofmann
Comments (0)