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

DOI10.2168/LMCS-4(3:5)2008MaRDI QIDQ3535610zbMATH OpenOpenAlexFDO

Authors Wojciech Moczydłowski, Robert Constable

Publication date 13 November 2008

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-4(3:5)2008

zbMATH Keywords

higher-order logicprogram extractionintuitionistic set theoryweak normalizationconstructive core of HOL

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Nonclassical and second-order set theories (03E70)

Recommendations

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

Cited in

(3)

• scientific article; zbMATH DE number 4148081 (Why is no real title available?)
• Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
• scientific article; zbMATH DE number 2003148 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nuprl
• MetaPRL
• 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 Q3535610)