scientific article; zbMATH DE number 1324438

Publication date: 16 August 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

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