Strong normalization results by translation

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.
Submitted to APAL

Keywords

Logic, Logic in Computer Science

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/230662

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/0905.2892
 http://arxiv.org/abs/0905.2892

Collections

arXiv