Classical proofs as programs: how, what and why

DOI10.1007/BFB0021084MaRDI QIDQ4594253zbMATH OpenOpenAlexFDO

Authors Chetan R. Murthy

Publication date 17 November 2017

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

Full work available at URL https://doi.org/10.1007/bfb0021084

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 517083
• scientific article; zbMATH DE number 65537
• scientific article; zbMATH DE number 1678362
• scientific article; zbMATH DE number 895269
• Practical program extraction from classical proofs

Cited in

(15)

• Maximal ideals in countable rings, constructively
• Automated constructivization of proofs
• scientific article; zbMATH DE number 65537 (Why is no real title available?)
• scientific article; zbMATH DE number 517083 (Why is no real title available?)
• What Is the Difference Between Proofs and Programs?
• On the Weihrauch degree of the additive Ramsey theorem
• Hilbert's tenth problem for term algebras with a substitution operator
• Complemented subsets and Boolean-valued, partial functions
• Defining long words succinctly in FO and MSO
• On the first-order parts of problems in the Weihrauch degrees
• Algorithmically random series
• Ideal presentations and numberings of some classes of effective quasi-Polish spaces
• Lower bounds on () and other properties of -register machines
• Reifying dynamical algebra: maximal ideals in countable rings, constructively
• Categorical proof theory of classical propositional calculus

This page was built for publication: Classical proofs as programs: how, what and why

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