BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Syntactic View of Computational Adequacy - Marco Devesas Campos\
 , University of Birmingham
DTSTART:20200312T130000Z
DTEND:20200312T132000Z
UID:TALK140644@talks.cam.ac.uk
CONTACT:Jean Pichon-Pharabod
DESCRIPTION: When presenting a denotational semantics of a language with r
 ecursion\, it is necessary to show that the semantics is computationally a
 dequate\, i.e. that every divergent term denotes the “bottom” element 
 of its associated domain. \n\nWe will explain how to view such a theorem a
 s a purely syntactic result. Any theory (congruence) that includes basic l
 aws and is closed under an infinitary rule that we call “rational contin
 uity” has the property that every divergent term is equated with the div
 ergent constant. Therefore\, to prove a model adequate\, it suffices to sh
 ow that it validates the basic laws and the rational continuity rule. Whil
 e this approach was inspired by the categorical\, ordered framework of Abr
 amsky et. al.\, neither category theory nor order is needed. \n\nTo show t
 he applicability of our approach\, we will present this syntactic result i
 n various contexts: we will start with PCF\; then we will see what complic
 ations arise when we try to add sum types\; these complications will be mu
 ch amplified when we handle our next target\, Levy’s Call-by-push-value\
 ;  and\, finally\, time-permitting\, we will talk briefly about polymorphi
 c types.
LOCATION:Computer Lab\, GC22
END:VEVENT
END:VCALENDAR