BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Full Abstraction for PCF with Names - Steffen Lösch\, University 
 of Cambridge
DTSTART:20121126T130000Z
DTEND:20121126T140000Z
UID:TALK41246@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:Since its introduction by Plotkin in 1977\, the functional pro
 gramming language PCF\, together with its denotational semantics based on 
 Scott domains\, has had a significant impact in the programming language c
 ommunity. In particular\, Plotkin's original paper proves a now-famous res
 ult: PCF endowed with a ‘parallel-or’ construct is fully abstract with
  respect to Scott domains\, in the sense that two expressions have equal d
 enotations if and only if they the have the same observable operational be
 haviour in all contexts.\n\nThis talk shows how PCF can be extended with n
 aming constructs\, so that the language can express object-level name-bind
 ing. We call the extended language PNA (Programming with Name Abstractions
 ). Many algorithms that cause tedious alpha-equivalence issues in other la
 nguages can be expressed in a simple and direct way in PNA. Moreover\, the
  operational semantics remains state-free\, so PNA is still a pure\, funct
 ional language.\n\nTo reflect the name-related changes\, we model the deno
 tational semantics of PNA with nominal sets\, which leads to a notion of n
 ominal Scott domain. The functionals for existential quantification over n
 ames and ‘definite description’ over names turn out to be compact in t
 he sense appropriate for nominal Scott domains. Adding them to PNA\, toget
 her with parallel-or\, we prove a full abstraction result for nominal Scot
 t domains analogous to Plotkin’s classic result above: two program phras
 es have the same observable operational behaviour in all contexts if and o
 nly if they denote equal elements of the nominal Scott domain model.\n\nTh
 e 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/~sg
 l27/fullans.pdf
LOCATION:FW26
END:VEVENT
END:VCALENDAR