University of Cambridge > > Semantics Lunch (Computer Laboratory) > Strongly-typed term representations in Coq

Strongly-typed term representations in Coq

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity