Nuprl combined constructive type theory, refinement-style proof development, tactics and computational interpretation of proofs. Complete proofs could be used to obtain programs meeting formal specifications, linking theorem proving, formal mathematics and verified programming in a single…
The CADE-8 proceedings, published on 1 July 1986, included Douglas Howe's experiment using Nuprl together with simple proof-assisting programs to constructively prove a substantial theorem of number theory. Cornell's official Nuprl documentation states that the system had been in use since June 1984 and was already accumulating a library of formal algorithmic mathematics.
Nuprl combined constructive type theory, refinement-style proof development, tactics and computational interpretation of proofs. Complete proofs could be used to obtain programs meeting formal specifications, linking theorem proving, formal mathematics and verified programming in a single environment.
Nuprl represents a distinct foundational branch of machine-checked mathematics: rather than only certifying propositions, its constructive type theory treats proofs as computational objects. This lineage influenced proof assistants and formal-mathematics systems built around dependent and constructive type theories.
Significance rationale: Nuprl established a constructive type-theoretic proof-development environment in which formal proofs could carry computational content and support program extraction. Its early use on substantial number theory showed that interactive proof development could serve formal mathematics, not only program verification.
—
—
The CADE-8 proceedings provide an exact publication anchor for the Nuprl number-theory experiment; Cornell's project documentation independently records that Nuprl had been used since June 1984.
No corrections recorded.
