具有引用和类型不动点的有界时间编程的索引可实现性
Indexed realizability for bounded-time programming with references and type fixpoints
摘要：
隐式复杂性领域最近产生了几种有界复杂性程序设计语言。这种语言允许精确地实现属于某个复杂类的函数。我们在这里提出了一个实现语义的高阶函数语言的基础上的线性逻辑称为LAL的复杂性类PTIME的特点的片段。这种语言的特点是递归类型和高阶存储。我们的可实现性是基于双正交性，步进索引，而且是定量的。这最后一个功能，使我们不仅可以得到一个语义证明的终止，但也给类型化程序终止所需的计算步骤的数量上的界限。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
