21778 articles – 15587 Notices  [english version]

ensl-00681296, version 1

Computational interpretation of classical logic with explicit structural rules

Silvia Ghilezan (, http://imft.ftn.uns.ac.rs/~silvia/) 1, Pierre Lescanne (, http://perso.ens-lyon.fr/pierre.lescanne/) 2, Dragisa Zunic () 3

Résumé : We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and duplication of terms, respectively. We present a type system for which we prove the type-preservation under reduction. A mutual relation with classical calculus featuring implicit structural rules has been studied in detail. From this analysis we derive strong normalisation property.

  • 1 :  Faculty of engineering, University of Novi Sad
  • University of Novi Sad
  • 2 :  Laboratoire de l'Informatique du Parallélisme (LIP)
  • Université de Lyon – CNRS : UMR5668 – INRIA – École Normale Supérieure - Lyon – Université Claude Bernard - Lyon I
  • 3 :  Faculty of Economics and Engineering Management
  • Faculty of Economics and Engineering Management
  • Domaine : Informatique/Logique en informatique
    Mathématiques/Logique
    Informatique/Calcul parallèle, distribué et partagé
  • Mots-clés : F.4.1 [Mathematical Logic]: Lambda calculus and related systems – F.3.1 [Specifying and Verifying and Reasoning about Programs]: Logics of programs – F.3.2 [Semantics of Programming Languages]: Operational semantics – F.3.3 [Studies of Program Constructs]: T
 
  • ensl-00681296, version 1
  • http://hal-ens-lyon.archives-ouvertes.fr/ensl-00681296
  • oai:hal-ens-lyon.archives-ouvertes.fr:ensl-00681296
  • Contributeur : Pierre Lescanne <>
  • Soumis le : Mercredi 21 Mars 2012, 10:56:59
  • Dernière modification le : Mercredi 13 Mars 2013, 16:39:28