@InProceedings{chol, author = {Robert Constable and Wojciech Moczyd{\l}owski}, title = {Extracting {P}rograms from {C}onstructive {HOL} {P}roofs via {IZF} {S}et-{T}heoretic {S}emantics}, booktitle = {Proceedings of 3rd International Joint Conference on Automated Reasoning (IJCAR 2006)}, series = {Lecture Notes in Computer Science}, volume = 4130, pages = {162-176}, year = {2006}, publisher = "Springer" }