A Syntactic View of Computational Adequacy

Marco Devesas Campos, Paul Blain Levy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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 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. 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 finally includes polymorphic types.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures (FOSSACS 2018)
Subtitle of host publication21st International Conference, FOSSACS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 Thessaloniki, Greece, April 14–20, 2018 Proceedings
EditorsChristel Baier, Ugo Dal Lago
PublisherSpringer
Pages71-87
Volume10803
ISBN (Electronic)978-3-319-89366-2
ISBN (Print)978-3-319-89365-5
DOIs
Publication statusPublished - 14 Apr 2018
Event21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018) - Thessaloniki, Greece
Duration: 14 Apr 201820 Apr 2018

Publication series

NameLecture Notes in Computer Science - Advanced Research in Computing and Software Science
PublisherSpringer
Volume10803
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018)
Country/TerritoryGreece
CityThessaloniki
Period14/04/1820/04/18

Fingerprint

Dive into the research topics of 'A Syntactic View of Computational Adequacy'. Together they form a unique fingerprint.

Cite this