5 found
Order:
  1. Corrigendum to “Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction”.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (4):1415-1416.
    This paper points out an error of Parigot's proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.
    Direct download (12 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2.  7
    Strong Normalization of Classical Natural Deduction with Disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1-3):21-37.
    This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  16
    Strong Reduction of Combinatory Calculus with Streams.Koji Nakazawa & Hiroto Naya - 2015 - Studia Logica 103 (2):375-387.
    This paper gives the strong reduction of the combinatory calculus SCL, which was introduced as a combinatory calculus corresponding to the untyped Lambda-mu calculus. It proves the confluence of the strong reduction. By the confluence, it also proves the conservativity of the extensional equality of SCL over the combinatory calculus CL, and the consistency of SCL.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  4.  7
    Compositional Z: Confluence Proofs for Permutative Conversion.Koji Nakazawa & Ken-Etsu Fujita - 2016 - Studia Logica 104 (6):1205-1224.
    This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, called the Z (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  5.  34
    Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (3):851-859.
    This paper points out an error of Parigot’s proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   1 citation