Short proofs of strong normalization
Logic in Computer Science
2008-04-17 v1
Abstract
This paper presents simple, syntactic strong normalization proofs for the simply-typed lambda-calculus and the polymorphic lambda-calculus (system F) with the full set of logical connectives, and all the permutative reductions. The normalization proofs use translations of terms and types to systems, for which strong normalization property is known.
Keywords
Cite
@article{arxiv.0804.2535,
title = {Short proofs of strong normalization},
author = {Aleksander Wojdyga},
journal= {arXiv preprint arXiv:0804.2535},
year = {2008}
}