TY - GEN

T1 - A Syntactic View of Computational Adequacy

AU - Devesas Campos, Marco

AU - Levy, Paul Blain

PY - 2018/4/14

Y1 - 2018/4/14

N2 - 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 a domain. We explain how to view such a theorem as a purely syntactic result. Any theory (congruence) that includes basic laws and is closed under an inﬁnitary 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 suﬃces 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. The purpose of the paper is to present this syntactic result for call-bypush-value extended with term-level recursion and polymorphic types. Our account begins with PCF, then includes sum types, then moves to call-by-push-value, and ﬁnally includes polymorphic types.

AB - 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 a domain. We explain how to view such a theorem as a purely syntactic result. Any theory (congruence) that includes basic laws and is closed under an inﬁnitary 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 suﬃces 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. The purpose of the paper is to present this syntactic result for call-bypush-value extended with term-level recursion and polymorphic types. Our account begins with PCF, then includes sum types, then moves to call-by-push-value, and ﬁnally includes polymorphic types.

U2 - 10.1007/978-3-319-89366-2_4

DO - 10.1007/978-3-319-89366-2_4

M3 - Conference contribution

SN - 978-3-319-89365-5

VL - 10803

T3 - Lecture Notes in Computer Science - Advanced Research in Computing and Software Science

SP - 71

EP - 87

BT - Foundations of Software Science and Computation Structures (FOSSACS 2018)

A2 - Baier, Christel

A2 - Dal Lago, Ugo

PB - Springer

T2 - 21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018)

Y2 - 14 April 2018 through 20 April 2018

ER -