University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Classical Linear Logic considered as a programming language

Classical Linear Logic considered as a programming language

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity