KnowledgeBase » SEMINAR » ID = 474

Extracting Readable and Efficient Programs from Nuprl Proofs

by James L. Caldwell
1997-1998

In this weeks PRL seminar I will talk about a methodology for extracting readable and efficient recursive programs from Nuprl proofs. The methodology depends on careful use of the set type in specifications and on recursion schemes extracted from proofs of induction principles.

A paper entitled Moving Proofs as Programs into Practice describes the methodology.

I will also touch on possible applications of the intersection type.