BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Semantics Lunch (Computer Laboratory)
SUMMARY:Full Abstraction for PCF with Names - Steffen Lösc
h\, University of Cambridge
DTSTART;TZID=Europe/London:20121126T130000
DTEND;TZID=Europe/London:20121126T140000
UID:TALK41246AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/41246
DESCRIPTION:Since its introduction by Plotkin in 1977\, the fu
nctional 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 orig
inal 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.\n\nThis talk shows how
PCF can be extended with naming constructs\, so th
at the language can express object-level name-bind
ing. We call the extended language PNA (Programmin
g with Name Abstractions). Many algorithms that ca
use tedious alpha-equivalence issues in other lang
uages can be expressed in a simple and direct way
in PNA. Moreover\, the operational semantics remai
ns state-free\, so PNA is still a pure\, functiona
l language.\n\nTo 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 qua
ntification over names and ‘definite description’
over names turn out to be compact in the sense app
ropriate for nominal Scott domains. Adding them to
PNA\, together with parallel-or\, we prove a full
abstraction result for nominal Scott domains anal
ogous to Plotkin’s classic result above: two progr
am phrases have the same observable operational be
haviour in all contexts if and only if they denote
equal elements of the nominal Scott domain model.
\n\nThe results mentioned are based on joint work
with Andrew M. Pitts and will be published at POPL
2013. "Link to the paper":http://www.cl.cam.ac.uk
/~sgl27/fullans.pdf
LOCATION:FW26
CONTACT:Peter Sewell
END:VEVENT
END:VCALENDAR