COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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 languageAdd 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)
- Computer Laboratory talks
- Computing and Mathematics
- FW26
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
Note that ex-directory lists are not shown. |
## Other listsInstitute of Astronomy Extra Talks Immunology and Medicine Seminars Neuroscience Seminars## Other talksJoinings of higher rank diagonalizable actions TBA Anthropology, mass graves and the politics of the dead Filling box flows in porous media Holonomic D-modules, b-functions, and coadmissibility Feeding your genes: The impact of nitrogen availability on gene and genome sequence evolution |