Publication:4255509

Publication date: 16 August 1999

natural deduction; classical logic; proofs-as-programs paradigm; classical proofs; algorithmic content of cut-elimination

Mathematics Subject Classification ID

03B70: Logic in computer science

03F05: Cut-elimination and normal-form theorems

03B40: Combinatory logic and lambda calculus

Related Items

Strong normalization proof with CPS-translation for second order classical natural deduction, A short proof of the strong normalization of classical natural deduction with disjunction, Termination checking with types, Entiers intuitionnistes et entiers classiques en $\lambda \, C$-calcul, Towards Ludics Programming: Interactive Proof Search, On the semantics of classical disjunction, Subtractive logic, Refined program extraction from classical proofs, Proof theory in the abstract, Towards the animation of proofs -- testing proofs by examples, Strong normalizability of the non-deterministic catch/throw calculi, Preface to the special volume, Polarized and focalized linear and classical proofs, Strong normalisation in the $\pi$-calculus, Strong normalization results by translation, Kripke models for classical logic, Completeness and partial soundness results for intersection and union typing for $\overline{\lambda}\mu\tilde{\mu}$, Type checking and typability in domain-free lambda calculi, Pedagogical second-order $\lambda $-calculus, A completeness result for the simply typed $\lambda \mu $-calculus, The $\lambda $-calculus and the unity of structural proof theory, A semantical proof of the strong normalization theorem for full propositional classical natural deduction, Strong normalization proofs by CPS-translations, Categorical proof theory of classical propositional calculus, Resource operators for $\lambda$-calculus, Combining algebraic effects with continuations, A syntactic correspondence between context-sensitive calculi and abstract machines, Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage, CERES: An analysis of Fürstenberg's proof of the infinity of primes, A type-theoretic foundation of delimited continuations, Counting proofs in propositional logic, CPS-translation as adjoint, Full intuitionistic linear logic, Classical logic, storage operators and second-order lambda-calculus, A general storage theorem for integers in call-by-name $\lambda$- calculus, Intuitionistic and classical natural deduction systems with the catch and the throw rules, Computational isomorphisms in classical logic, On the intuitionistic force of classical search, Search algorithms in type theory, Proof-search in type-theoretic languages: An introduction, Uniform Heyting arithmetic, Non-strictly positive fixed points for classical natural deduction, About classical logic and imperative programming, An interpretation of $\lambda \mu$-calculus in $\lambda$-calculus., Polarized proof-nets and $\lambda \mu$-calculus, Confluency and strong normalizability of call-by-value $\lambda \mu$-calculus, Structural cut elimination. I: Intuitionistic and classical logic, Church-Rosser property of a simple reduction for full first-order classical natural deduction, Strong normalization of the second-order symmetric $\lambda \mu$-calculus, Getting results from programs extracted from classical proofs, Dependent choice, `quote' and the clock, Limiting partial combinatory algebras, Polarized games, A strong normalization result for classical logic, The differential $\lambda \mu$-calculus, The next 700 Krivine machines, A proof-theoretic foundation of abortive continuations, Second-order type isomorphisms through game semantics, Classical $F_{\omega}$, orthogonality and symmetric candidates, Strong normalization of classical natural deduction with disjunctions, Call-by-name reduction and cut-elimination in classical logic, On the unity of duality, Investigations on the dual calculus, Order-enriched categorical models of the classical sequent calculus, Domain-Freeλµ-Calculus, Classical Call-by-Need and Duality, A Filter Model for the λμ-Calculus, Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming, Covert Movement in Logical Grammar, Intersection Types for the Resource Control Lambda Calculi, A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types, A Complete, Co-inductive Syntactic Theory of Sequential Control and State, Call-by-Value Is Dual to Call-by-Name, Extended, A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract), Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence, Quantifiers in Japanese, An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form, Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus