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

Robert L. Constable, Wojciech Moczydlowski

Browse the full CADE paper archive.