Computational open-endedness in a type theory is defined as the property that theorems remain true under extensions to the underlying programming language. Some properties related to open-endedness that are relevant to machine implementations of type theory are established. A class of computation systems, specified by a simple but fairly general kind of structural operational semantics, with respect to which P. Martin-Lof's (6th Int. Congress for Logic, Methodology, and Philosophy of Science, p.153-175, 1982) type theory (and most of its descendants) is open-ended is defined. It is shown that any such system validates a useful form of type free reasoning about program equivalence and that symbolic computation procedures can be automatically derived from these specifications. The main result is the definition of a particular computation system that includes a collection of oracles sufficient to provide a classical semantics for Martin-Lof's type theory in which the excluded middle law holds. >

The authors lay the foundations for reasoning about proofs whose steps include both invocations of programs to build subproofs (tactics) and references to representations of proofs themselves (reflected proofs). The main result is the definition of a single type of proof which can mention itself, using a novel technique which finds a fixed point of a mapping between metalanguage and object language. This single type contrasts with hierarchies of types used in other approaches to accomplish the same classification. It is shown that these proofs are valid, and that every proof can be reduced to a proof involving only primitive inference rules. The extension of the results to proofs from which programs (such as tactics) can be derive and to proofs that can refer to a library of definitions and previously proven theorems is shown. It is believed that the mechanism of reflection is fundamental in building proof development systems, and its power is illustrated with applications to automating reasoning and describing modes of computation.>

The author introduces a general class of lazy computation systems and defines a natural program equivalence for them. He proves that if an extensionality condition holds of each of the operators of a computational system, then the equivalence relation is a congruence, so that the usual kinds of equality reasoning are valid for it. This condition is a simple syntactic one and is easy to verify for the various lazy computation systems considered so far. Conditions are given under which the equivalence coincides with observational congruence. These results have important consequences for type theories.>