KnowledgeBase » SEMINAR » ID = 369

Extraction

by Judith Underwood
1992-1993

Judith will give a description of how program extraction from Nuprl proofs works. She will also discuss how we can use programs to drive proofs (reverse extraction?) and how to make extracted programs more efficient by simple transformations between justifications of well-foundedness of induction forms.
She will also touch on extraction from classical proofs.