PRL Seminars

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.