Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
- 12 August 2008
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC in Lecture Notes in Computer Science
Abstract
No abstract availableKeywords
This publication has 12 references indexed in Scilit:
- Barendregt’s Variable Convention in Rule InductionsLecture Notes in Computer Science, 2007
- Principles of SuperdeductionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2007
- Alpha-structural recursion and inductionJournal of the ACM, 2006
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOLLecture Notes in Computer Science, 2006
- On equivalence and canonical forms in the LF type theoryACM Transactions on Computational Logic, 2005
- Structural Cut EliminationInformation and Computation, 2000
- A symmetric lambda calculus for “classical” program extractionLecture Notes in Computer Science, 1994
- Ideas and Results in Proof TheoryPublished by Elsevier BV ,1971
- Disjunction and existence under implication in elementary intuitionistic formalismsThe Journal of Symbolic Logic, 1962
- Untersuchungen ber das logische Schlie en. IMathematische Zeitschrift, 1935