Peter Battyanyi ; Karim Nour - Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi

lmcs:3963 - Logical Methods in Computer Science, September 28, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:34)2017
Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculiArticle

Authors: Peter Battyanyi ; Karim Nour

    In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation of classical propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin [3] extended with negation. In this paper we adapt the method of David and Nour [4] for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.


    Volume: Volume 13, Issue 3
    Published on: September 28, 2017
    Accepted on: September 28, 2017
    Submitted on: September 28, 2017
    Keywords: Mathematics - Logic

    Consultation statistics

    This page has been seen 1108 times.
    This article's PDF has been downloaded 233 times.