unofficial copy [PS]

by Douglas J. Howe

Functional Programming Concurrency Simulation and Automated Reasoning (LNCS), 1993.

**Abstract
**

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.