Strongly-typed term representations in Coq

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

• Andrew Kennedy (Microsoft Research)
• Monday 30 March 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Computer Laboratory talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• de239's list

Note that ex-directory lists are not shown.