2009/05/18 by René David, David, René, Karim Nour +1
Computer Science · Mathematics · #FOS: Computer and information sciences #FOS: Mathematics #Image and Signal Denoising Methods #Logic (math.LO) #Logic in Computer Science (cs.LO) #cs.LO #math.LO
paper · pdf · doi:10.48550/arxiv.0905.2892
Submitted to APAL
arxiv created 2009/05/18 · openalex publication_date 2009/05/18 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.