LFPL: Revisited and Mechanized

TL;DR

This paper provides a modern, mechanized presentation of LFPL, a functional language characterizing polynomial-time computable functions, including proofs of soundness and completeness within a proof assistant.

Contribution

It offers a self-contained, streamlined account and mechanization of LFPL and its metatheory, with novel proofs and a simplified core argument.

Findings

Mechanized full proofs of LFPL's soundness and completeness.

LFPL+ extends LFPL with additional features and maintains soundness.

LFPL programs can simulate polynomial-time Turing machines efficiently.

Abstract

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.