首页 | 本学科首页   官方微博 | 高级检索  
     


Realizability models and implicit complexity
Authors:Ugo Dal Lago  Martin Hofmann
Affiliation:
  • a Dipartimento di Scienze dell’Informazione, Università di Bologna, Italy
  • b 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 等数据库收录!
    设为首页 | 免责声明 | 关于勤云 | 加入收藏

    Copyright©北京勤云科技发展有限公司  京ICP备09084417号