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+语言，其创新之处在于改编了Aehlig和Schwichtenberg (2002)的技术，通过构造显式多项式来约束基于大步代价语义的LFPL+表达式代价。完备性证明表明LFPL程序可在仅依赖受限线性函数与列表的条件下模拟多项式时间图灵机，其结构与Hofmann (2002)的原始证明一致，但通过新型栈式数据结构大幅简化了核心论证，该结构由一等函数与列表实现。机械化方案包含了完整的可靠性证明与完备性证明，并成为新兴证明助手Istari中机械化元理论的首批案例研究之一。