Powered by OpenAIRE graph
Found an issue? Give us feedback
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/ Journal of the ACMarrow_drop_down
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
Journal of the ACM
Article
Data sources: UnpayWall
image/svg+xml art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos Open Access logo, converted into svg, designed by PLoS. This version with transparent background. http://commons.wikimedia.org/wiki/File:Open_Access_logo_PLoS_white.svg art designer at PLoS, modified by Wikipedia users Nina, Beao, JakobVoss, and AnonMoos http://www.plos.org/
Apollo
Article . 2014
Data sources: Apollo
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
image/svg+xml Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao Closed Access logo, derived from PLoS Open Access logo. This version with transparent background. http://commons.wikimedia.org/wiki/File:Closed_Access_logo_transparent.svg Jakob Voss, based on art designer at PLoS, modified by Wikipedia users Nina and Beao
zbMATH Open
Article . 2014
Data sources: zbMATH Open
DBLP
Article
Data sources: DBLP
versions View all 4 versions
addClaim

This Research product is the result of merged Research products in OpenAIRE.

You have already added 0 works in your ORCID record related to the merged Research product.

Denotational Semantics with Nominal Scott Domains

Denotational semantics with nominal Scott domains
Authors: Steffen Lösch; Andrew M. Pitts;

Denotational Semantics with Nominal Scott Domains

Abstract

When defining computations over syntax as data, one often runs into tedious issues concerning α -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, λν -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.

Country
United Kingdom
Related Organizations
Keywords

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.), domain theory, Theory of programming languages, Semantics in the theory of computing, 46 Information and Computing Sciences, full abstraction, nominal sets, metaprogramming, Functional programming and lambda calculus, 4612 Software Engineering, denotational semantics, symmetry

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    3
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
3
Average
Average
Average
Green
bronze