I N R I A – Rocquencourt
Amphi Turing du bātiment 1
Lundi 7 mai, 10h30
Beniamino Accatoli
LIX
Abella formalization of lambda-calculus residual theory
Abella is a new proof assistant developed by Andrew Gacek and based on work of Gacek, Miller and Nadathur. Its main feature is a primitive handling of binders via higher order abstract syntax and the nabla quantifier. In the talk we introduce the system and present a formalization of the residual theory of lambda calculus. This development is actually a re-formalization of a work of Huet in Coq. Thanks to the features of Abella and to a re-understanding of the Huet’s work we get an elegant and extremely concise formalization of the cube lemma for residuals. We also discuss some work in progress towards the formalization of more advanced results.
