Strong normalization results by translation
Logic
2009-05-19 v1 Logic in Computer Science
Abstract
We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system.
Cite
@article{arxiv.0905.2892,
title = {Strong normalization results by translation},
author = {René David and Karim Nour},
journal= {arXiv preprint arXiv:0905.2892},
year = {2009}
}
Comments
Submitted to APAL