Strong normalization results by translation
classification
🧮 math.LO
cs.LO
keywords
normalizationstrongtranslationclassicalconjunctionconversionsdeductiondisjunction
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.