BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Categorical Models of Explicit Substitutions - Valeria de Paiva (T
 opos Institute)
DTSTART:20210601T151500Z
DTEND:20210601T161500Z
UID:TALK160855@talks.cam.ac.uk
CONTACT:José Siqueira
DESCRIPTION:The advantages of functional programming are well-known: progr
 ams are easier to write\, understand and verify than their imperative coun
 terparts. However\, functional languages tend to be more memory intensive 
 and these problems have hindered their wider use in industry. The xSLAM pr
 oject tried\nto address these issues by using explicit substitutions to co
 nstruct and implement more efficient abstract machines.\nIn this work we p
 rovide categorical models for the calculi of explicit substitutions (linea
 r and cartesian) that we are interested in.\n\nIndexed categories provide 
 models of cartesian calculi of explicit substitutions. However\, these str
 uctures are inherently non-linear and hence cannot be used to model linear
  calculi of explicit substitutions. This work replaces indexed categories 
 with pre-sheaves\, thus providing a categorical semantics covering both th
 e linear and cartesian cases. We justify our models by proving soundness a
 nd completeness results. Then we speculate on why there are not many model
 s around\, given the large number of calculi discussed in the community.\n
 \nZoom link: \n https://maths-cam-ac-uk.zoom.us/j/99667325570?pwd=TC9RakFU
 cGZQdEM5bExMbzlraDZOZz09
LOCATION:Zoom (Meeting ID 996 6732 5570\, passcode 109362)
END:VEVENT
END:VCALENDAR