unofficial copies [PDF], [PS]

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe and William Aitken

Proceedings of Fifth IEEE Symposium on Logic in Computer Science, pp. 95-197, 1990.

We begin to lay the foundations for reasoning about reflected proofs in theories where proofs have computational significance, and we demonstrate several applications of the basic concepts in computer systems which implement these theories. The first key result is the definition of a single type of proof which can mention itself (reflected proof) using a new technique which finds a fixed point of a mapping between object language and metalanguage. The second main result is an argument that the proof type is valid. This single type contrasts with hierarchies of types used in other approaches to accomplish the same classification.

We believe that the mechanism of reflection is fundamental in building proof development systems, and we illustrate its power with applications to automating reasoning, extending type theories and describing modes of computation.