TY - GEN
T1 - Proof pearl
T2 - 2nd International Conference on Certified Programs and Proofs, CPP 2012
AU - Accattoli, Beniamino
PY - 2012/11/27
Y1 - 2012/11/27
N2 - 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.
AB - 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.
U2 - 10.1007/978-3-642-35308-6_15
DO - 10.1007/978-3-642-35308-6_15
M3 - Conference contribution
AN - SCOPUS:84869832043
SN - 9783642353079
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 173
EP - 187
BT - Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings
Y2 - 13 December 2012 through 15 December 2012
ER -