Skip to Main content Skip to Navigation
Conference papers

Proof pearl: abella formalization of lambda-calculus cube property

Beniamino Accattoli 1, 2 
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download
Contributor : Beniamino Accattoli Connect in order to contact the contributor
Submitted on : Wednesday, January 23, 2013 - 5:18:09 PM
Last modification on : Thursday, January 20, 2022 - 5:30:47 PM
Long-term archiving on: : Wednesday, April 24, 2013 - 3:59:41 AM


Files produced by the author(s)


  • HAL Id : hal-00780337, version 1



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⟩



Record views


Files downloads