vai al contenuto della pagina vai al menu di navigazione

Lambda-Types on the Lambda-Calculus with Abbreviations: a Certified Specification

F. Guidi


University of Bologna (Italy). Department of Computer Science.

In this paper the author presents $\lambda\delta$, a λ-typed λ-calculus with a single λ binder and abbreviations. The formal properties of $\lambda\delta$, that include the standard requirements for a typed λ-calculus, have been certified by the author with the proof assistant Coq. The presentation focuses on motivating the calculus and the corpus of definitions on which its specification in Coq is based.