Hostname: page-component-745bb68f8f-grxwn Total loading time: 0 Render date: 2025-01-24T00:47:32.023Z Has data issue: false hasContentIssue false
  • English
  • Français

Classical linear logic of implications

Published online by Cambridge University Press:  14 March 2005

MASAHITO HASEGAWA
MASAHITO HASEGAWA
Affiliation:
Research Institute for Mathematical Sciences, Kyoto University, Kyoto 606-8502 Japan PRESTO, Japan Science and Technology Agency Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We give a simple term calculus for the multiplicative exponential fragment of Classical Linear Logic, by extending Barber and Plotkin's dual-context system for the intuitionistic case. The calculus has the non-linear and linear implications as the basic constructs, and this design choice allows a technically manageable axiomatisation without commuting conversions. Despite this simplicity, the calculus is shown to be sound and complete for category-theoretic models given by *-autonomous categories with linear exponential comonads.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 15 , Issue 2 , April 2005 , pp. 323 - 342
Copyright
2005 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)