Abstract

Recently I’ve been working with Nick Benton and Carsten Varming on formalizing in Coq the domain theoretic semantics of call-by-value PCF and call-by-value untyped lambda calculus. We’ll talk about the (more interesting!) domain theory some other time. For this semantics lunch I want to talk about term representations. (Yes, it’s time we had a talk about binding again.) For the simply-typed case it turns out that one can use a “strongly-typed” representation in which terms are well-typed by definition, with “typed” de Bruijn encodings for variables. Although the basic definitions of terms are standard – and have been popularized recently in programming languages that support GAD Ts – the definition of substitution and associated lemmas was tricky to get right. Once this is done, though, statements of theorems and proofs are beautifully straightforward.