Strong normalization results by translation

13 years 4 months ago

Download www.lama.univ-savoie.fr

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

René David, Karim Nour

Real-time Traffic

APAL 2010 | Classical Natural Deduction | Permutative Conversions | Strong Normalization |

claim paper

Related Content

» Short proofs of strong normalization

» The Simplytyped Pure Pattern Type System Ensures Strong Normalization

» Strong Normalization of the Dual Classical Sequent Calculus

» On strong normalization and type inference in the intersection type discipline

» A Formalization of Strong Normalization for SimplyTyped LambdaCalculus and System F

» Strong Normalization in a NonDeterministic Typed LambdaCalculus

» Harnessing MLF with the Power of System F

» Strong and NVsequentiality of constructor systems

» The Conservation Theorem revisited

Post Info
More Details (n/a)

Added	08 Dec 2010
Updated	08 Dec 2010
Type	Journal
Year	2010
Where	APAL
Authors	René David, Karim Nour

Comments (0)

Sciweavers

Strong normalization results by translation

APAL 2010 | Classical Natural Deduction | Permutative Conversions | Strong Normalization |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers