Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Chu’s construction
Bellin G. In Logic for concurrency and synchronisation. Norwell, MA,  Kluwer Academic Publishers,  2003. Type:Book Chapter
Date Reviewed: Apr 26 2004

The categorical study of linear logic is addressed in this chapter. Specifically, the author demonstrates that a particular functor pertaining to the abstract categorical model of linear logic can be constructed in purely proof-theoretical terms.

Linear logic was introduced as a means to study the dynamics of proofs in classical logic, although some ideas from intuitionistic logic were taken into account in its conception. Regarding category theory, it is well known that monoidal closed categories provide models of intuitionistic linear logic, whereas *-autonomous categories provide a model for classical linear logic.

Chu’s construction was introduced in the appendix of Barr [1], with purely categorical interests, as a method to build a *-autonomous category starting from monoidal closed categories, several years before Girard’s seminal paper [2] was published. The goal of this chapter is to show that the action of a particular functor existing in Chu’s construction can be represented by Girard’s trips on a proof-net of linear logic.

This chapter is part of an edited book, but it seems that it was not subject to a thorough proofreading process; a considerable number of typographical and other minor errors appear throughout the text, including the references.

Reviewer:  Manuel Ojeda Aciego Review #: CR129504 (0411-1374)
1) Barr, M. *-autonomous categories: Lecture Notes in Mathematics 752. Springer-Verlag, Heidelberg, Germany, 1979.
2) Girard, J-Y. Linear logic. Theoretical Computer Science 50, (1987), 1–102.
Bookmark and Share
 
Proof Theory (F.4.1 ... )
 
 
Deduction (I.2.3 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Proof Theory": Date
On the strength of temporal proofs
Andréka H., Németi I., Sain I. Theoretical Computer Science 80(2): 125-151, 1991. Type: Article
Apr 1 1992
Completion for unification
Doggaz N., Kirchner C. (ed) Theoretical Computer Science 85(2): 231-251, 1991. Type: Article
Aug 1 1992
Proof normalization with nonstandard objects
Goto S. Theoretical Computer Science 85(2): 333-351, 1991. Type: Article
Aug 1 1992
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy