BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Strongly-typed term representations in Coq - Andrew Kennedy (Micro
 soft Research)
DTSTART:20090330T114500Z
DTEND:20090330T130000Z
UID:TALK17602@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Recently I've been working with Nick Benton and Carsten Varmin
 g on formalizing in Coq the domain theoretic semantics of call-by-value PC
 F and call-by-value untyped lambda calculus. We'll talk about the (more in
 teresting!) 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 definitio
 n\, with "typed" de Bruijn encodings for variables. Although the basic def
 initions of terms are standard - and have been popularized recently in pro
 gramming languages that support GADTs - the definition of substitution and
  associated lemmas was tricky to get right. Once this is done\, though\, s
 tatements of theorems and proofs are beautifully straightforward.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR