Arithmetical proofs of strong normalization results for the symmetric $\lambda \mu$-calculus
Logic
2009-05-08 v1
Abstract
The symmetric -calculus is the -calculus introduced by Parigot in which the reduction rule , which is the symmetric of , is added. We give arithmetical proofs of some strong normalization results for this calculus. We show (this is a new result) that the -reduction is strongly normalizing for the un-typed calculus. We also show the strong normalization of the -reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical.
Keywords
Cite
@article{arxiv.0905.1034,
title = {Arithmetical proofs of strong normalization results for the symmetric $\lambda \mu$-calculus},
author = {René David and Karim Nour},
journal= {arXiv preprint arXiv:0905.1034},
year = {2009}
}