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).

• Type: Journal
• Year: 2011
• Where: TCS
• Authors: Ugo Dal Lago, Martin Hofmann
• Keywords: Affine Logic, Elementary Affine Logic, Semantic Framework, TCS 2011, Theoretical Computer Science