COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## A Syntactic View of Computational AdequacyAdd 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
- Computer Laboratory talks
- Computing and Mathematics
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsThe best of Telluride Mountainfilm Festival Humanitarian events Neuropsychological Rehabilitation Seminars## Other talksCANCELLED: Art Speak CANCELLED - Further explorations in Peru CANCELLED: Art Speak The first Egyptian society Rank-Based Independence Testing in Near Linear Time |