University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > A Syntactic View of Computational Adequacy

A Syntactic View of Computational Adequacy

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity