Classical Linear Logic considered as a programming language

Add to your list(s) Download to your calendar using vCal

• Robert Atkey, University of Strathclyde
• Friday 29 July 2016, 14:00-15:00
• FW26.

If you have a question about this talk, please contact Dominic Mulligan.

Classical Linear Logic (CLL) has long inspired readings of its proofs as concurrent processes. Wadler’s CP calculus is one of these readings that views the formulas of CLL as session types and proofs as processes. Wadler gave CP an operational semantics by selecting a subset of the cut-elimination rules of CLL to use as reduction rules. This semantics has an appealing close connection to the logic, but does not resolve the status of the other cut-elimination rules, and does not admit an obvious notion of observational equivalence.

In this talk, I will propose a new operational semantics for CP based on the idea of observing communication between communicating processes. I’ll use this semantics to define an intuitively reasonable notion of observational equivalence. To reason about observational equivalence, I use of the standard relational denotational semantics 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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.