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

https://hal.inria.fr/hal-00780337
Contributor : Beniamino Accattoli <>
Submitted on : Wednesday, January 23, 2013 - 5:18:09 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Wednesday, April 24, 2013 - 3:59:41 AM

File

CPP2012.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00780337, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

328

Files downloads

188