Publication:4255509

Publication date: 16 August 1999

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

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items

On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem, A semantical proof of the strong normalization theorem for full propositional classical natural deduction, Classical logic, storage operators and second-order lambda-calculus, A general storage theorem for integers in call-by-name $\lambda$- calculus, Applicative bisimilarities for call-by-name and call-by-value $\lambda\mu$-calculus, Strong normalization of the second-order symmetric $\lambda \mu$-calculus, Getting results from programs extracted from classical proofs, Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective), Dependent choice, `quote' and the clock, Limiting partial combinatory algebras, Polarized games, The differential $\lambda \mu$-calculus, Continuation Models for the Lambda Calculus With Constructors, Strong normalization proofs by CPS-translations, 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, A strong normalization result for classical logic, Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less), Categorical proof theory of classical propositional calculus, Strong normalisation in the $\pi$-calculus, Resource operators for $\lambda$-calculus, Combining algebraic effects with continuations, A syntactic correspondence between context-sensitive calculi and abstract machines, Some properties of the -calculus, Semantic types and approximation for Featherweight Java, Intuitionistic and classical natural deduction systems with the catch and the throw rules, Call-by-Value Is Dual to Call-by-Name, Extended, Simple free star-autonomous categories and full coherence, Computational isomorphisms in classical logic, Reduction rules for intuitionistic $\lambda\rho$-calculus, A curry-style semantics of interaction: from untyped to second-order lazy $\lambda\mu$-calculus, Böhm theorem and Böhm trees for the $\varLambda \mu$-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}$, Dualized Simple Type Theory, The Cooper storage idiom, Unnamed Item, Linearity, Control Effects, and Behavioral Types, Type checking and typability in domain-free lambda calculi, A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract), Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence, Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage, Conjunctive, Disjunctive, Negative Objects and Generalized Quantification, Domain-Freeλµ-Calculus, Verificationism and Classical Realizability, Validating Brouwer's continuity principle for numbers using named exceptions, Proof nets for classical logic, The next 700 Krivine machines, A proof-theoretic foundation of abortive continuations, CERES: An analysis of Fürstenberg's proof of the infinity of primes, Classical Call-by-Need and Duality, A Filter Model for the λμ-Calculus, Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming, On the intuitionistic force of classical search (Extended abstract), Covert Movement in Logical Grammar, Compositional Z: confluence proofs for permutative conversion, Second-order type isomorphisms through game semantics, Classical natural deduction for S4 modal logic, Hypothetical logic of proofs, Preface to the special volume, 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, The computational content of arithmetical proofs, A type-theoretic foundation of delimited continuations, Polarized and focalized linear and classical proofs, Uniform Heyting arithmetic, Non-strictly positive fixed points for classical natural deduction, An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus, Investigations on the dual calculus, 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 Classical Realizability Model for a Semantical Value Restriction, Classical By-Need, Game Semantics for Access Control, Quantifiers in Japanese, Counting proofs in propositional logic, Nominal Confluence Tool, 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, About classical logic and imperative programming, Confluence proofs of lambda-mu-calculi by Z theorem, Intersection Types for the Resource Control Lambda Calculi, A Third-Order Representation of the λμ-Calculus, On the intuitionistic force of classical search, Search algorithms in type theory, Proof-search in type-theoretic languages: An introduction, CPS-translation as adjoint, Order-enriched categorical models of the classical sequent calculus, 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, On the Computational Representation of Classical Logical Connectives, Full intuitionistic linear logic, Church-Rosser property of a simple reduction for full first-order classical natural deduction, Strong reduction of combinatory calculus with streams, Normalization in the simply typed -calculus, Programming and Proving with Classical Types, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Machine Deduction, Deciding contextual equivalence of $\nu $-calculus with effectful contexts, Entiers intuitionnistes et entiers classiques en $\lambda \, C$-calcul, Classical (co)recursion: Mechanics, Adding Negation to Lambda Mu, Constructive forcing, CPS translations and witness extraction in Interactive realizability, Structural Rules in Natural Deduction with Alternatives, Call-by-name extensionality and confluence, Unnamed Item, Unnamed Item, Focused linear logic and the $\lambda$-calculus, Proof-terms for classical and intuitionistic resolution, Proof Terms for Generalized Natural Deduction, 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, Functional Type Assignment for Featherweight Java, Termination checking with types, On the semantics of classical disjunction, Subtractive logic, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, 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, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, Unnamed Item, Unnamed Item, Unnamed Item, Deriving Natural Deduction Rules from Truth Tables, GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION, Denotational Semantics of Call-by-name Normalization in Lambda-mu Calculus, Intuitionistic Letcc via Labelled Deduction, Expansion trees with cut, On the unification of classical, intuitionistic and affine logics, Towards Ludics Programming: Interactive Proof Search, Proofs, Reasoning and the Metamorphosis of Logic, Assertions, Hypotheses, Conjectures, Expectations: Rough-Sets Semantics and Proof Theory, CUT ELIMINATION AND NORMALIZATION FOR GENERALIZED SINGLE AND MULTI-CONCLUSION SEQUENT AND NATURAL DEDUCTION CALCULI, The approximation theorem for the Λμ-calculus