Skip to main content
PRL Project

Efficient Programming by Extract in Nuprl Type Theory

by Aleksey Nogin


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