# * 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).