|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Full Abstraction for PCF with Names
If you have a question about this talk, please contact Peter Sewell.
Since its introduction by Plotkin in 1977, the functional programming language PCF , together with its denotational semantics based on Scott domains, has had a significant impact in the programming language community. In particular, Plotkin’s original paper proves a now-famous result: PCF endowed with a ‘parallel-or’ construct is fully abstract with respect to Scott domains, in the sense that two expressions have equal denotations if and only if they the have the same observable operational behaviour in all contexts.
This talk shows how PCF can be extended with naming constructs, so that the language can express object-level name-binding. We call the extended language PNA (Programming with Name Abstractions). Many algorithms that cause tedious alpha-equivalence issues in other languages can be expressed in a simple and direct way in PNA . Moreover, the operational semantics remains state-free, so PNA is still a pure, functional language.
To reflect the name-related changes, we model the denotational semantics of PNA with nominal sets, which leads to a notion of nominal Scott domain. The functionals for existential quantification over names and ‘definite description’ over names turn out to be compact in the sense appropriate for nominal Scott domains. Adding them to PNA , together with parallel-or, we prove a full abstraction result for nominal Scott domains analogous to Plotkin’s classic result above: 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.
The results mentioned are based on joint work with Andrew M. Pitts and will be published at POPL 2013 . Link to the paper
This talk is part of the Semantics Lunch (Computer Laboratory) series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsSpring School 2008 - Translating animal models to patients with Neurodegenerative disorders Departmental Seminar Programme, Department of Veterinary Medicine 4cmr seminar
Other talksDeep consequences: Why syntax (as we know it) isn't a thing, and other (shocking?) conclusions from modelling language with neural nets "Ireland grows up: the debate about how to celebrate the centenary of the 1916 Rising" Thermostabilisation of G protein-coupled receptors to facilitate structure determination Why fracking works and why not well enough Optical Fibres in Oil and Gas; Monitoring at the Speed of Light. Seismic retrofitting of historic masonry structures