The essential interaction between classical and intuitionistic features in the system of linear logic is best described in the language of category theory. Given a symmetric monoidal closed category C with products, the category C x C^op can be given the structure of a *-autonomous category by a special case of the Chu construction. The main result of the paper is to show that the intuitionistic translations induced by Girard trips on a proof net determine the functor from the free *-autonomous category on a set of atoms {P, P',...} to C x C^op, where C is the free monoidal closed category with products and coproducts on the set of atoms {P_O, P_I, P'_O, P'_I, ...} (a pair P_O, P_I in C for each atom P of A).

Chu's construction: a proof-theoretic approach

BELLIN, Gianluigi
2003-01-01

Abstract

The essential interaction between classical and intuitionistic features in the system of linear logic is best described in the language of category theory. Given a symmetric monoidal closed category C with products, the category C x C^op can be given the structure of a *-autonomous category by a special case of the Chu construction. The main result of the paper is to show that the intuitionistic translations induced by Girard trips on a proof net determine the functor from the free *-autonomous category on a set of atoms {P, P',...} to C x C^op, where C is the free monoidal closed category with products and coproducts on the set of atoms {P_O, P_I, P'_O, P'_I, ...} (a pair P_O, P_I in C for each atom P of A).
2003
Chu spaces; proof nets; linear logic
File in questo prodotto:
File Dimensione Formato  
chu's_construction.pdf

accesso aperto

Tipologia: Documento in Post-print
Licenza: Dominio pubblico
Dimensione 1.23 MB
Formato Adobe PDF
1.23 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/312318
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact