44 articles – 42 references  [version française]

hal-00617254, version 1

Intuitionistic Dual-intuitionistic Nets

Olivier Laurent () 1

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:  Laboratoire de l'Informatique du Parallélisme (LIP)
  • 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
  • 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