|
| This Article | ||
| ||
| Share | ||
| Bibliographic References | ||
| Add to: | ||
| | ||
| Search | ||
| ||
19th Annual IEEE Symposium on Logic in Computer Science (LICS'04)
On the Geometry of Interaction for Classical Logic
Turku, Finland
July 13-July 17
ISBN: 0-7695-2192-4
| ASCII Text | x | ||
| Carsten F?hrmann, David Pym, "On the Geometry of Interaction for Classical Logic," Logic in Computer Science, Symposium on, pp. 211-220, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004. | |||
| BibTex | x | ||
| @article{ 10.1109/LICS.2004.1319615, author = {Carsten F?hrmann and David Pym}, title = {On the Geometry of Interaction for Classical Logic}, journal ={Logic in Computer Science, Symposium on}, volume = {0}, year = {2004}, issn = {1043-6871}, pages = {211-220}, doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2004.1319615}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, } | |||
| RefWorks Procite/RefMan/Endnote | x | ||
| TY - CONF JO - Logic in Computer Science, Symposium on TI - On the Geometry of Interaction for Classical Logic SN - 1043-6871 SP211 EP220 A1 - Carsten F?hrmann, A1 - David Pym, PY - 2004 KW - null VL - 0 JA - Logic in Computer Science, Symposium on ER - | |||
It is well-known that weakening and contraction cause na?ve categorical models of the classical sequent calculus to collapse to Boolean lattices. We introduce sound and complete models that avoid this collapse by interpreting cut-reduction by a partial order between morphisms. We provide concrete examples of such models by applying the geometry-of-interaction construction to quantaloids with finite biproducts, and show how these models illuminate cut reduction in the presence of weakening and contraction. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination.
Citation:
Carsten F?hrmann, David Pym, "On the Geometry of Interaction for Classical Logic," lics, pp.211-220, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.
