### Denotational Semantics with Nominal Scott DomainsDenotational Semantics with Nominal Scott Domains

Access Restriction
Subscribed

 Author Lsch, Steffen ♦ Pitts, Andrew M. Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2014 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword Metaprogramming ♦ Denotational semantics ♦ Domain theory ♦ Full abstraction ♦ Nominal sets ♦ Symmetry Abstract When defining computations over syntax as data, one often runs into tedious issues concerning $\textit{α}-equivalence$ and semantically correct manipulations of binding constructs. Here we study a semantic framework in which these issues can be dealt with automatically by the programming language. We take the user-friendly “nominal” approach in which bound objects are named. In particular, we develop a version of Scott domains within nominal sets and define two programming languages whose denotational semantics are based on those domains. The first language, $\textit{λν}-PCF,$ is an extension of Plotkin’s PCF with names that can be swapped, tested for equality and locally scoped; although simple, it already exposes most of the semantic subtleties of our approach. The second language, PNA, extends the first with name abstraction and concretion so that it can be used for metaprogramming over syntax with binders. For both languages, we prove a full abstraction result for nominal Scott domains analogous to Plotkin’s classic result about PCF and conventional Scott domains: two program phrases have the same observable operational behaviour in all contexts if and only if they denote equal elements of the nominal Scott domain model. This is the first full abstraction result we know of for languages combining higher-order functions with some form of locally scoped names which uses a domain theory based on ordinary extensional functions, rather than using the more intensional approach of game semantics. To obtain full abstraction, we need to add two functionals, one for existential quantification over names and one for “definite description” over names. Only adding one of them is not enough, as we give counter-examples to full abstraction in both cases. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2014-07-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 61 Issue Number 4 Page Count 46 Starting Page 1 Ending Page 46

#### Open content in new tab

Source: ACM Digital Library