A Syntactic View of Computational Adequacy

Add to your list(s) Download to your calendar using vCal

• Marco Devesas Campos, University of Birmingham
• Thursday 12 March 2020, 13:00-13:20
• Computer Lab, GC22.

If you have a question about this talk, please contact Jean Pichon-Pharabod.

When presenting a denotational semantics of a language with recursion, it is necessary to show that the semantics is computationally adequate, i.e. that every divergent term denotes the “bottom” element of its associated domain.

We will explain how to view such a theorem as a purely syntactic result. Any theory (congruence) that includes basic laws and is closed under an infinitary rule that we call “rational continuity” has the property that every divergent term is equated with the divergent constant. Therefore, to prove a model adequate, it suffices to show that it validates the basic laws and the rational continuity rule. While this approach was inspired by the categorical, ordered framework of Abramsky et. al., neither category theory nor order is needed.

To show the applicability of our approach, we will present this syntactic result in various contexts: we will start with PCF ; then we will see what complications arise when we try to add sum types; these complications will be much amplified when we handle our next target, Levy’s Call-by-push-value; and, finally, time-permitting, we will talk briefly about polymorphic types.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Lab, GC22
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.