BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Denotation of Contextual Modal Type theory - Murdoch Gabbay
DTSTART:20130701T130000Z
DTEND:20130701T140000Z
UID:TALK46103@talks.cam.ac.uk
CONTACT:Dominic Orchard
DESCRIPTION:Nanevski in his PhD thesis introduced and studied Contextual M
 odal Theory\nTheory.  This is a lambda-calculus based via the Curry-Howard
 \ncorrespondence on an extension of the modal logic S4 with multiple\nmoda
 lities\, one for each variable.  The application is to meta-programming\,\
 nwhere the intuitive denotation of Box A is "syntax of type A".\n\nThe lan
 guage itself is pretty\, and we developed a denotational semantics\nfor th
 is which is quite attractive and displays some interesting\nproperties.  I
  will give a tour of the system and discuss future work.\nThe associated j
 ournal paper on "Denotations of CMTT" is online\n(http://gabbay.org.uk/pap
 ers.html#dencmt\nhttp://www.sciencedirect.com/science/article/pii/S1570868
 31200050X)
LOCATION:FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR