Skip to main content
PRL Project

Extracting Readable and Efficient Programs from Nuprl Proofs

by James L. Caldwell

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.