PRL Seminars
Aleksey Nogin
Efficient Programming by Extract in Nuprl Type TheoryFebruary 7, 2000
CommentI 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
|
| Home | | Introduction | | Authors | | Topics | | Chronological List | | PRL Project |