Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4662702 | Annals of Pure and Applied Logic | 2010 | 9 Pages |
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 λμ-calculus. We also extend Mendler’s result on recursive equations to this system.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic