Section: Application Domains

Principled computation for strong lambda-calculi

The application domain of the cost models and abstract machines for functional programs line of work—when application is intended in concrete terms—is the implementation of proof assistants.

Both functional languages and proof assistants rely on the $\lambda$-calculus has reference model. Functional languages are built on the weak $\lambda$-calculus (where evaluation does not enter function bodies) whose theory is simple and whose implementation has been widely explored in the last decades. Proof assistants instead require the full power of the strong $\lambda$-calculus, whose theory is more involved and whose implementation has mostly been neglected by the literature.

The study of reasonable cost models naturally leads to a refined theory of implementations, where different techniques and optimisations are classified depending on their complexity (with respect to the cost model). This direction is particularly relevant for the strong $\lambda$-calculus, for which most implementations are developed in a ad-hoc way.

The theoretical study in particular pointed out that all available proof assistants are implemented following unreasonable implementation schemas, where unreasonable here means with potentially exponential overhead with respect to the number of steps in the calculus.

Beniamino Accattoli collaborates with Bruno Barras—one of the implementors of Coq, the most used proof assistant—and Claudio Sacerdoti Coen—one of the implementors of Matita—in order to develop a fine theory of implementation for proof assistants.

If applications are intended also at a more theoretical level, the study of reasonable cost models is also applicable to the development of quantitative denotational semantics, to higher-order approaches to complexity theory, and to implicit computational complexity.