Skip to main content
PRL Project

Semantic Foundations for Embedding HOL in Nuprl

by Douglas J. Howe

Algebraic Methodology and Software Technology

  • unofficial copies PDF, PS

We give a new semantics for Nuprl's constructive type theory that justifies a useful embedding of the logic of the HOL theorem prover inside Nuprl. The embedding gives Nuprl effective access to most of the large body of formalized mathematics that the HOL community has amassed over the last decade. The new semantics is dramatically simpler than the old, and gives a novel and general way of adding set-theoretic equivalence classes to untyped functional programming languages.

bibTex ref: Howe96

cite link