BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:First steps in synthetic guarded domain theory: step-indexing in t
 he topos of trees - Rasmus Møgelberg\, IT University\, Copenhagen
DTSTART:20120413T130000Z
DTEND:20120413T140000Z
UID:TALK37013@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:We show how the topos of trees\, i.e.\, the category of preshe
 aves over the ordered\nnatural numbers\, models guarded recursive terms\, 
 predicates and types.\nWe have two motivations for this work: one is as a 
 model of\ncomputation with streams\, using guards to ensure well-definedne
 ss of\nrecursive definitions. The other is the construction of\nmodels of 
 programming languages with higher-order store\, which involves \nsolving r
 ecursive domain equations. But since guarded recursion is commonplace\nin 
 computer science we expect many more applications.\n\nIn the talk I will g
 ive a computational intuition for the topos of trees and\nshow how the int
 ernal logic of this model can be used as an expressive \nlanguage combinin
 g dependent types and subset types with guarded recursion.\nI will also sk
 etch how to construct a model of higher-order store entirely inside\nthis 
 language\, using a combination of set-like constructions and guarded recur
 sion.\nRelations to step-indexing and metric space models of guarded recur
 sion will be discussed.\n\nThis talk is based on joint work with Lars Birk
 edal\, Kristian Stovring\nand Jan Schwinghammer
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR