scientific article; zbMATH DE number 517083

zbMath0805.03012MaRDI QIDQ4282613

Michel Parigot

Publication date: 29 January 1995

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

zbMATH Keywords

natural deductionconfluenceproofs-as-programs paradigmfunctional programssecond order classical proofs

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof theory in general (including proof-theoretic semantics) (03F03) General theory of computer systems (68M01)

Related Items (17)

Normalization in the simply typed -calculus ⋮ Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus ⋮ Programming and Proving with Classical Types ⋮ Unnamed Item ⋮ Structural Rules in Natural Deduction with Alternatives ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ Non deterministic classical logic: the $\lambda\mu^{++}$-calculus ⋮ Domain-Freeλµ-Calculus ⋮ POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE ⋮ A proof-theoretic foundation of abortive continuations ⋮ Subtractive logic ⋮ An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus ⋮ Intuitionistic Letcc via Labelled Deduction ⋮ Proof-search in type-theoretic languages: An introduction ⋮ An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus. ⋮ Polarized proof-nets and \(\lambda \mu\)-calculus ⋮ Church-Rosser property of a simple reduction for full first-order classical natural deduction

This page was built for publication: