BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Classical Linear Logic considered as a programming language - Robe
 rt Atkey\, University of Strathclyde
DTSTART:20160729T130000Z
DTEND:20160729T140000Z
UID:TALK66449@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Classical Linear Logic (CLL) has long inspired readings of its
  proofs as concurrent processes. Wadler's CP calculus is one of these read
 ings that views the formulas of CLL as session types and proofs as process
 es. Wadler gave CP an operational semantics by selecting a subset of the c
 ut-elimination rules of CLL to use as reduction rules. This semantics has 
 an appealing close connection to the logic\, but does not resolve the stat
 us of the other cut-elimination rules\, and does not admit an obvious noti
 on of observational equivalence.\n\nIn this talk\, I will propose a new op
 erational semantics for CP based on the idea of observing communication be
 tween communicating processes. I'll use this semantics to define an intuit
 ively reasonable notion of observational equivalence. To reason about obse
 rvational equivalence\, I use of the standard relational denotational sema
 ntics of CLL. This denotational semantics is adequate for our operational 
 semantics\, and enables a proof that all the cut-elimination rules of CLL 
 are observational equivalences.\n
LOCATION:FW26
END:VEVENT
END:VCALENDAR