Short proofs of strong normalization

This paper presents simple, syntactic strong normalization proofs for the simply-typed -calculus and the polymorphic -calculus (system F) with the full set of logical connectives, and all the permutative reductions. The normalization proofs use translations of terms and types of ,,, to terms and types of and from F,,,,, to F,.

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Aleksander Wojdyga
• Keywords: CORR 2008, Education, Logical Connectives, Paper, Permutative Reductions