BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Theory of Indirection via Approximation - Aquinas Hobor
DTSTART:20091027T150000Z
DTEND:20091027T160000Z
UID:TALK21202@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:Building semantic models that account for various kinds of ind
 irect reference has traditionally been a difficult problem. Indirect refer
 ence can appear in many guises\, such as heap pointers\, higher-order func
 tions\, object references\, and shared-memory mutexes.\nWe give a general 
 method to construct models containing indirect reference by presenting a 
 “theory of indirection”. Our method can be applied in a wide variety o
 f settings and uses only simple\, elementary mathematics. In addition to v
 arious forms of indirect reference\, the resulting models support powerful
  features such as impredicative quantification and equirecursion\; moreove
 r they are compatible with the kind of powerful substructural accounting r
 equired to model (higher-order) separation logic. In contrast to previous 
 work\, our model is easy to apply to new settings and has a simple axiomat
 ization\, which is complete in the sense that all models of it are isomorp
 hic. Our proofs are machine-checked in Coq.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR