Constructive Mathematics as a Programming Logic I: Some Principles of Theory
by Robert L. Constable
1985
Annals of Mathematics, vol. 24
- Published version in Topics in the Theory of Computation 1985
- Technical Report 83-554 http://hdl.handle.net/1813/6394
- unofficial copies PDF, PS
Abstract
The design of a programming system is guided by certain beliefs, principles, and practical constraints. These considerations are not always manifest from the rules defining the system. In this paper, the author discusses some of the principles which have guided the design of the programming logics built at Cornell in the last decade. Most of the necessarily brief discussion concerns type theory with stress on the concepts of function space and quotient types.
bibTex ref: Con85
cite link