BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:First steps in synthetic guarded domain theory: st
ep-indexing in the topos of trees - Rasmus Møgelbe
rg\, IT University\, Copenhagen
DTSTART;TZID=Europe/London:20120413T140000
DTEND;TZID=Europe/London:20120413T150000
UID:TALK37013AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/37013
DESCRIPTION:We show how the topos of trees\, i.e.\, the catego
ry of presheaves over the ordered\nnatural numbers
\, models guarded recursive terms\, predicates and
types.\nWe have two motivations for this work: on
e is as a model of\ncomputation with streams\, usi
ng guards to ensure well-definedness of\nrecursive
definitions. The other is the construction of\nmo
dels of programming languages with higher-order st
ore\, which involves \nsolving recursive domain eq
uations. But since guarded recursion is commonplac
e\nin computer science we expect many more applica
tions.\n\nIn the talk I will give a computational
intuition for the topos of trees and\nshow how the
internal logic of this model can be used as an ex
pressive \nlanguage combining dependent types and
subset types with guarded recursion.\nI will also
sketch how to construct a model of higher-order st
ore entirely inside\nthis language\, using a combi
nation of set-like constructions and guarded recur
sion.\nRelations to step-indexing and metric space
models of guarded recursion will be discussed.\n\
nThis talk is based on joint work with Lars Birked
al\, Kristian Stovring\nand Jan Schwinghammer
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Bjarki Holm
END:VEVENT
END:VCALENDAR