Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics

DOI10.1007/11814771_16MaRDI QIDQ3613407zbMATH OpenOpenAlexFDO

Authors Wojciech Moczydłowski, Robert Constable

Publication date 12 March 2009

Published in Automated Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
• scientific article; zbMATH DE number 2003148
• scientific article; zbMATH DE number 177798
• Practical program extraction from classical proofs
• Extraction and verification of programs by analysis of formal proofs

Cited in

(5)

• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics
• Unifying Sets and Programs via Dependent Types
• Unifying sets and programs via dependent types
• A Normalizing Intuitionistic Set Theory with Inaccessible Sets
• Extracting the resolution algorithm from a completeness proof for the propositional calculus

Describes a project that uses

Uses Software

• PVS

This page was built for publication: Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics

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