scientific article; zbMATH DE number 517083

MaRDI QIDQ4282613zbMATH OpenFDO

Authors Michel Parigot

Publication date 29 January 1995

zbMATH Keywords

confluencefunctional programsnatural deductionproofs-as-programs paradigmsecond 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)

Recommendations

• Classical proofs as programs: how, what and why
• Practical program extraction from classical proofs
• Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique
• Classical Program Extraction in the Calculus of Constructions
• scientific article; zbMATH DE number 895269

Cited in

(29)

• Proof-search in type-theoretic languages: An introduction
• About classical logic and imperative programming
• 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
• On the computational representation of classical logical connectives
• Automated constructivization of proofs
• Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique
• Classical proofs as parallel programs
• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• scientific article; zbMATH DE number 1104448 (Why is no real title available?)
• Non deterministic classical logic: the $\lambda\mu^{++}$-calculus
• An estimation for the lengths of reduction sequences of the \(\lambda\mu\rho\theta\)-calculus
• Classical proofs as programs: how, what and why
• Polymorphism and the obstinate circularity of second order logic: a victims' tale
• scientific article; zbMATH DE number 7393562 (Why is no real title available?)
• Intuitionistic Letcc via Labelled Deduction
• Programming and Proving with Classical Types
• scientific article; zbMATH DE number 2213623 (Why is no real title available?)
• Normalization in the simply typed -calculus
• Subtractive logic
• Structural Rules in Natural Deduction with Alternatives
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• A strong bisimulation for a classical term calculus
• A new conjecture about identity of proofs
• Proofs with star and perp

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4282613)