Abstract
In 1994 Gerard Huet formalized in Coq the cube property of ł-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. © 2012 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Accattoli, B. (2012). Proof pearl: Abella formalization of λ-calculus cube property. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 173–187). https://doi.org/10.1007/978-3-642-35308-6_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
