Authors: Wen Kokke, Fabrizio Montesi and Marco Peressotti
Paper Information
Title: | Taking Linear Logic Apart |
Authors: | Wen Kokke, Fabrizio Montesi and Marco Peressotti |
Proceedings: | Linearity/TLLA Pre-proceedings |
Editors: | Maribel Fernandez, Valeria de Paiva, Thomas Ehrhard and Lorenzo Tortora De Falco |
Keywords: | linear logic, process calculus, hypersequents |
Abstract: | ABSTRACT. Process calculi based in logic, such as πDill and CP, provide a foundation for deadlock-free concurrent programming. However, there is a mismatch between the structures of operators used as proof terms in previous work, and the term constructs of the standard π-calculus. We introduce the Hypersequent Classical Processes (HCP), which addresses this mismatch. The key insight is to register parallelism in the typing judgements using hypersequents, a technique from logic which generalises judgements from one sequent to many. This allows us to take apart the term constructs used in Classical Processes (CP) to more closely match those of the standard π-calculus. We prove that HCP enjoys subject reduction and progress, and prove several properties relating it back to CP. |
Pages: | 12 |
Talk: | Jul 07 12:00 (Session 26J) |
Paper: |