NDLI: Denotational Semantics with Nominal Scott Domains

Content Provider	ACM Digital Library
Author	Lsch, Steffen Pitts, Andrew M.
Copyright Year	2014
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.
Starting Page	1
Ending Page	46
Page Count	46
File Format	PDF
ISSN	00045411
e-ISSN	1557735X
DOI	10.1145/2629529
Journal	Journal of the ACM (JACM)
Volume Number	61
Issue Number	4
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-07-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Metaprogramming Denotational semantics Domain theory Full abstraction Nominal sets Symmetry
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Control and Systems Engineering Artificial Intelligence Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Full abstraction for nominal Scott domains

Full abstraction for nominal Scott domains

XX Denotational Semantics with Nominal Scott Domains

Game semantics for a polymorphic programming language

Semantics of the Domain of Flow Diagrams

Full abstraction for nominal scott domains (2013).

Branching time and abstraction in bisimulation semantics

Tape Sets and Automata

Unrecognizable Sets of Numbers

Denotational Semantics with Nominal Scott Domains

Similar Documents

Full abstraction for nominal Scott domains

Full abstraction for nominal Scott domains

XX Denotational Semantics with Nominal Scott Domains

Game semantics for a polymorphic programming language

Semantics of the Domain of Flow Diagrams

Full abstraction for nominal scott domains (2013).

Branching time and abstraction in bisimulation semantics

Tape Sets and Automata

Unrecognizable Sets of Numbers

Denotational Semantics with Nominal Scott Domains