KnowledgeBase » 
SEMINAR
» ID = 520
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).