Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics
From MaRDI portal
Publication:3613407
DOI10.1007/11814771_16zbMath1222.68359OpenAlexW1944542258MaRDI QIDQ3613407
Wojciech Moczydłowski, Robert L. 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
Related Items
Unifying sets and programs via dependent types, Extracting the resolution algorithm from a completeness proof for the propositional calculus, Unifying Sets and Programs via Dependent Types
Uses Software