# * Aspects of the Implementation of Type Theory *

## by Robert W. Harper

1985

Cornell University Ph.D. Thesis

- Tech Report TR85-675 http://hdl.handle.net/1813/6515
- unofficial copies PDF, PS

**Abstract**

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