A symmetric lambda calculus for ``classical program extraction

DOI10.1007/3-540-57887-0_112MaRDI QIDQ4490745zbMATH OpenFDO

Authors Franco Barbanera, Stefano Berardi

Publication date 20 July 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-57887-0_112

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) First-order arithmetic and fragments (03F30) Functional programming and lambda calculus (68N18)

Recommendations

• A symmetric lambda calculus for classical program extraction
• Classical Program Extraction in the Calculus of Constructions
• scientific article; zbMATH DE number 512771
• scientific article; zbMATH DE number 2080223
• Strong normalization of a symmetric lambda calculus for second-order classical logic

Cited in

(12)

• Intuitionistic and classical natural deduction systems with the catch and the throw rules
• A symmetric lambda calculus for classical program extraction
• Abstracting models of strong normalization for classical calculi
• Classical Program Extraction in the Calculus of Constructions
• ``Classical programming-with-proofs in \(\lambda_{\text{PA}}^{\text{Sym}}\): An analysis of non-confluence
• Non deterministic classical logic: the $\lambda\mu^{++}$-calculus
• A short proof of the strong normalization of classical natural deduction with disjunction
• Programming and Proving with Classical Types
• The true concurrency of Herbrand's theorem
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Normalization in the simply typed -calculus
• A contextual formalization of structural coinduction

This page was built for publication: A symmetric lambda calculus for ``classical program extraction

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