Sciweavers

TLCA
2007
Springer
15 years 3 months ago
An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
Abstract. This paper introduces a cut-elimination procedure of the intuitionistic sequent calculus and shows that it is isomorphic to the proof reduction of the intuitionistic natu...
Koji Nakazawa
87
Voted
RTA
2007
Springer
15 years 3 months ago
Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi
We present a method of lifting to explicit substitution calculi some characterizations of the strongly normalizing terms of λ-calculus by means of intersection type systems. The m...
Kentaro Kikuchi