Proof pearl: abella formalization of lambda-calculus cube property

Beniamino Accattoli (1, 2)

1 PARSIFAL - Proof search and reasoning with logic specifications
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

In 1994 Gerard Huet formalized in Coq the cube property of lambda-calculus residuals. His development is based on a clever idea, a beautiful inductive definition of residuals. However, in his formalization there is a lot of noise concerning the representation of terms with binders. We re-interpret his work in Abella, a recent proof assistant based on higher-order abstract syntax and provided with a nominal quantifier. By revisiting Huet's approach and exploiting the features of Abella, we get a strikingly compact and natural development, which makes Huet's idea really shine.

Domaines: Logique en informatique [cs.LO]

Beniamino Accattoli. Proof pearl: abella formalization of lambda-calculus cube property. Second international conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. ⟨hal-00780337⟩