Beniamino Accatoli speaks at Rocquencourt

I N R I A – Rocquencourt
Amphi Turing du bātiment 1
Lundi 7 mai, 10h30
Beniamino Accatoli

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.