Skip to main content
PRL Project

Reasoning About Functional Programs in Nuprl

by Douglas J. Howe

Functional Programming Concurrency Simulation and Automated Reasoning, LNCS

  • unofficial copy PS

There are two ways of reasoning about functional programs in the constructive type theory of the Nuprl proof development system. Nuprl can be used in a conventional program-verification mode, in which functional programs are written in a familiar style and then proven to be correct. It can also be used in an extraction mode, where programs are not written explicitly, but instead are extracted from mathematical proofs. Nuprl is the only constructive type theory to support both of these approaches. These approaches are illustrated by applying Nuprl to Boyer and Moore's "majority" algorithm.

bibTex ref: Howe93

cite link