Hofmann (1999) introduced the functional programming language LFPL to characterize the functions computable in polynomial time using an affine type system. LFPL enables a natural programming style, including nested recursion, and has inspired the development of type systems for automatic cost analysis, linear dependent type theories, and efficient memory management in functional programming languages. Despite its prominence, there does not exist a self-contained presentation, let alone a full mechanization, of LFPL and its core metatheory. This article presents a modern account and mechanization of LFPL and its metatheory with the goal of being self-contained and accessible while streamlining the strongest-known soundness and completeness results. The soundness proof works with the language LFPL+, which extends LFPL with additional language features. The proof is novel, adapting a technique by Aehlig and Schwichtenberg (2002) to construct explicit polynomials that bound the cost of an LFPL+ expression with respect to a big-step cost semantics. The completeness proof shows that LFPL programs can simulate polynomial-time Turing machines while only relying on restricted forms of linear functions and lists. It has the same structure as the original proof by Hofmann (2002) but greatly simplifies the core argument with a novel stack-like data structure that is implemented with first-class functions and lists. The mechanization includes the full soundness and completeness proofs, and serves as one of the first case studies of mechanized metatheory in the recently developed proof assistant Istari.

翻译：霍夫曼（Hofmann，1999）提出的函数式编程语言LFPL，通过仿射类型系统刻画了多项式时间可计算函数。该语言支持包括嵌套递归在内的自然编程风格，并启发了一系列类型系统的发展，包括自动代价分析、线性依赖类型理论以及函数式编程语言中的高效内存管理。尽管LFPL具有重要地位，但目前尚不存在完整的独立阐述，更不用说其核心元理论的完全机械化实现了。本文以可读性与自洽性为目标，对LFPL及其元理论给出现代阐述与机械化实现，同时精简了目前已知最强的可靠性与完备性结果。可靠性证明基于LFPL+语言——这是对LFPL增加额外语言特性的扩展。本证明具有创新性，借鉴了Aehlig与Schwichtenberg（2002）的技术，通过构造显式多项式，在大步代价语义下界定LFPL+表达式的计算代价。完备性证明表明，LFPL程序仅依赖受限形式的线性函数与列表即可模拟多项式时间图灵机。该证明与霍夫曼（2002）原始证明的结构一致，但通过使用一阶函数与列表实现的新型栈式数据结构，大幅简化了核心论证过程。机械化实现包含完整的可靠性与完备性证明，并作为近期开发的证明辅助工具Istari中机械化元理论的首批案例研究之一。