This repository contains the Abella formalization accompanying the ITP25 paper "Barendregt's Theory of the Lambda-Calculus, Refreshed and Formalized", authored by Adrienne Lancelot, Beniamino Accattoli and Maxime Vemclefs (doi to appear).

Version note

Proof development written in Abella, version 2.0.8.

Compilation

abella file.thm compiles an abella file (by default compiles automatically dependencies if they are not compiled already) to a compiled format file.thc

There exists a ProofGeneral fork that supports Abella: https://github.com/abella-prover/PG

We also provide a compilation script that checks all the Abella .thm files of the current repertory at once bash try_abella.sh and a cleaning script that removes all compilated file from the current repertory.

Skip as Axioms

There is one "skip" in the 11-maximality.thm file, that is used to represent an Axiom. See more in the section 11 of the paper.