Automating Reasoning in an Implementation of Constructive Type Theory

Other Titles


The starting point for this thesis is the Nuprl proof development system. Nuprl is an environment for the development of formal computational mathematics and has a rich constructive type theory as a logical basis. It provides sophisticated editors and an integrated tactic mechanism that allows the programming of guaranteed-sound extensions to the inference system. The work presented in this thesis concerns the automation of reasoning in Nuprl, and consists of three parts. The first is a collection of general-purpose tactics. These tactics are simple enough that their function can be readily understood, yet powerful enough to support development of substantial formal mathematics. The second part is the use of Nuprl to solve an open problem in the theory of programming languages. The set of basic tactics together with various tools provided by Nuprl play a crucial role in the solution, and it seems that this problem is not tractable without computer assistance. The third part is an implementation within Nuprl of mechanisms that support the use of Nuprl's type theory as a language for constructing theorem-proving procedures. The main component of the implementation is a large library of definitions, theorems and proofs. This library may be regarded as the beginning of a book of formal mathematics; it contains a complete formal development and explanation of a useful subset of Nuprl's metatheory, and of a mechanism for translating results established about this embedded metatheory to the object level. The type theory, besides permitting the internal development of this partial reflection mechanism, allows us to make abstractions that drastically reduce the burden of establishing the correctness of new theorem-proving procedures. Our library includes a formally verified term-rewriting system.

Journal / Series

Volume & Issue



Date Issued



Cornell University


computer science; technical report


Effective Date

Expiration Date




Union Local


Number of Workers

Committee Chair

Committee Co-Chair

Committee Member

Degree Discipline

Degree Name

Degree Level

Related Version

Related DOI

Related To

Related Part

Based on Related Item

Has Other Format(s)

Part of Related Item

Related To

Related Publication(s)

Link(s) to Related Publication(s)


Link(s) to Reference(s)

Previously Published As

Government Document




Other Identifiers


Rights URI


technical report

Accessibility Feature

Accessibility Hazard

Accessibility Summary

Link(s) to Catalog Record