Realizability models and implicit complexity |
| |
Authors: | Ugo Dal Lago Martin Hofmann |
| |
Affiliation: | a Dipartimento di Scienze dell’Informazione, Università di Bologna, Italyb Institut für Informatik, Ludwig-Maximilians-Universität, München, Germany |
| |
Abstract: | 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 assigning both abstract resource bounds in the form of elements from a resource monoid and resource-bounded computations to proofs (respectively, programs). |
| |
Keywords: | Implicit computational complexity Realizability Linear logic |
本文献已被 ScienceDirect 等数据库收录! |
|