Journal of Logic and Computation Advance Access published online on August 25, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp044
Original Papers |
Intuitionistic Dual-intuitionistic Nets
Laboratoire de lInformatique du Parallélisme, ENS Lyon – Université de Lyon, UMR 5668 CNRS ENS-Lyon UCBL INRIA, 46, allée dItalie, 69364 Lyon cedex 07, France. E-mail: olivier.laurent{at}ens-lyon.fr
Received 15 December 2008.
| Abstract |
|---|
The intuitionistic sequent calculus (at most one formula on the right-hand side of sequents) comes with a natural dual system: the dual-intuitionistic sequent calculus (at most one formula on the left-hand side). We explain how the duality between these two systems exactly corresponds to the intensively studied duality between call-by-value systems and call-by-name systems for classical logic. Relying on the uniqueness of the computational behaviour underlying these four logics (intuitionistic, dual-intuitionistic, call-by-value classical and call-by-name classical), we define a generic syntax of nets which can be used for any of these logics.
Keywords: Classical logic; intuitionistic logic; computational duality; proof-nets