Finding Computational Content from Classic Proofs
by Robert L. Constable
and Chetan Murthy
Logical Frameworks, G. Huet and G. Plotkin (eds.), pp. 341-362, Cambridge University Press, 1991.
Sorry, there are no downloadable files available for this document at this time.