Publication:4282613
From MaRDI portal
zbMath0805.03012MaRDI QIDQ4282613
Publication date: 29 January 1995
natural deduction; confluence; proofs-as-programs paradigm; functional programs; second order classical proofs
03B70: Logic in computer science
03F03: Proof theory in general (including proof-theoretic semantics)
68M01: General theory of computer systems
Related Items
Non deterministic classical logic: the $\lambda\mu^{++}$-calculus, POLYMORPHISM AND THE OBSTINATE CIRCULARITY OF SECOND ORDER LOGIC: A VICTIMS’ TALE, An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus, Intuitionistic Letcc via Labelled Deduction, Subtractive logic, Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\), 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, Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus, A proof-theoretic foundation of abortive continuations, Domain-Freeλµ-Calculus