Skip to main content
PRL Project

Efficient Programming by Extract in Nuprl Type Theory

by Aleksey Nogin
1999-2000

Comment

I am going to talk about efficient programming by extract in Nuprl type theory. I am going to present some general principles of writing Nuprl/MetaPRL proofs that produce efficient extract and I will show how applying these principles allowed me to make the extract from the Myhill--Nerode automata minimization theorem polynomial (from double-exponential).

Papers

http://www.cs.cornell.edu/nogin/papers/effproof.html