On the Strong Normalisation of Natural Deduction with Permutation-Conversions

13 years 8 months ago

Download www.loria.fr

We present a modular proof of the strong normalisation of intuitionistic logic with permutation-conversions. This proof is based on the notions of negative translation and CPS-simulation.

Philippe de Groote

Real-time Traffic

Modular Proof | RTA 1999 | Strong Normalisation | Theoretical Computer Science |

claim paper

» Strong normalization results by translation

» Refocusing Generalised Normalisation

» Strong Normalization of Classical Natural Deduction with Disjunction

» Characterising Strongly Normalising Intuitionistic Sequent Terms

» Principles of Superdeduction

» A Sequent Calculus for Type Theory

» A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems

» The Intensional Lambda Calculus

Post Info
More Details (n/a)

Added	04 Aug 2010
Updated	04 Aug 2010
Type	Conference
Year	1999
Where	RTA
Authors	Philippe de Groote

Comments (0)

Sciweavers

On the Strong Normalisation of Natural Deduction with Permutation-Conversions

Modular Proof | RTA 1999 | Strong Normalisation | Theoretical Computer Science |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers