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:A Syntactic View of Computational Adequacy - Marco
  Devesas Campos\, University of Birmingham
DTSTART;TZID=Europe/London:20200312T130000
DTEND;TZID=Europe/London:20200312T132000
UID:TALK140644AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/140644
DESCRIPTION: When presenting a denotational semantics of a lan
 guage with recursion\, it is necessary to show tha
 t the semantics is computationally adequate\, i.e.
  that every divergent term denotes the “bottom” el
 ement of its associated domain. \n\nWe will explai
 n how to view such a theorem as a purely syntactic
  result. Any theory (congruence) that includes bas
 ic laws and is closed under an infinitary rule tha
 t we call “rational continuity” has the property t
 hat every divergent term is equated with the diver
 gent constant. Therefore\, to prove a model adequa
 te\, it suffices to show that it validates the bas
 ic laws and the rational continuity rule. While th
 is approach was inspired by the categorical\, orde
 red framework of Abramsky et. al.\, neither catego
 ry theory nor order is needed. \n\nTo show the app
 licability of our approach\, we will present this 
 syntactic result in various contexts: we will star
 t with PCF\; then we will see what complications a
 rise when we try to add sum types\; these complica
 tions will be much amplified when we handle our ne
 xt target\, Levy’s Call-by-push-value\;  and\, fin
 ally\, time-permitting\, we will talk briefly abou
 t polymorphic types.
LOCATION:Computer Lab\, GC22
CONTACT:Jean Pichon-Pharabod
END:VEVENT
END:VCALENDAR