Skip to main content
PRL Project

Aspects of the Implementation of Type Theory

by Robert W. Harper

Cornell University Ph.D. Thesis

This thesis is about building an automated programming logic. For our purposes an automated programming logic consists of:

  • A formal system for reasoning about programs
  • A proof development environment, which includes at least, an editor for the construction of proofs in the logic
  • Mechanized decision methods to assist in the proof development process
  • A library mechanism for managing collections of theorems

bibTex ref: Har85

cite link