COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## Strongly-typed term representations in CoqAdd 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
- Interested Talks
- Room FW26, Computer Laboratory, William Gates Building
- School of Technology
- Semantics Lunch (Computer Laboratory)
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsSusan Gathercole Motivic stable homotopy theory study group Climate and Sustainable Development Finance for Industrial Sustainability in Developing Countries## Other talksHow T-cells cause autoimmune disease and hold the key to curing cancer Biosensor Technologies (Biacore SPR, Switchsense, Octet) Britain, Jamaica and the modern global financial order, 1800-50 Emulation for model discrepancy Changing languages in European Higher Education: from official policies to unofficial classroom practices |