hal-00617254, version 1
Intuitionistic Dual-intuitionistic Nets
Journal of Logic and Computation 21, 4 (2011) 561-587
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.
- 1:
- Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I
- Domain : Mathematics/Logic
- Keywords : classical logic – intuitionistic logic – computational duality – proof-nets
- hal-00617254, version 1
- http://hal.archives-ouvertes.fr/hal-00617254
- oai:hal.archives-ouvertes.fr:hal-00617254
- From:
- Submitted on: Friday, 26 August 2011 16:25:42
- Updated on: Friday, 26 August 2011 16:25:42


Associated documents
Export