Abstract
The computation system of constructive type theory is open-ended so that theorems about computation will hold for a broad class of extensions to the system. We show that despite this openness it is possible to completely reflect the computation system into the language in a clear way by adding simple primitive concepts that anticipate the reflection. This work provides a hook for developing methods to modify the built-in evaluator and to treat the issues of intensionality and computational complexity in programming logics and provides a basis for reflecting the deductive apparatus of type theory.
Supported in part by NSF grant CCR-8616552 and ONR grant N00014-88-K-0409.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
S. F. Allen. A non-type-theoretic semantics for type-theoretic language. PhD thesis, Cornell University, 1987.
S. F. Allen, R. L. Constable, D. J. Howe, and W. E. Aitken. The Semantics of Reflected Proof. Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, pp. 95–107, June 1990.
R. L. Constable, S. Allen, H. Bromely, W. Cleaveland, and et al. Implementing Mathematics with the Nuprl Development System. NJ:Prentice-Hall, 1986.
M. Davis and J. Schwartz. Metamathematical extensibility for theorem verifiers and proof checkers. In Comp. Math. with Applications, v. 5, pages 217–230, 1979.
D. Howe. Computational metetheory in nuprl. CADE-9, 230:404–415, 1988.
D. Howe. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1989.
P. Martin-Lof. An intuitionistic theory of types: predicative part. In Logic Colloquium’73., pages 73–118. Amsterdam:North-Holland, 1973.
P. Martin-Lof. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–75. Amsterdam:North Holland, 1982.
P. Mendier. Inductive Definition in Type Theory. PhD thesis, Cornell University, Ithaca, NY, 1988.
N. Shanker. Towrds mechanical metamathematics. Technical report, Institute for Computing Science, University of Texas at Austin, 1984. Tech. report 43.
B. C. Smith. Reflection and semantics in lisp. Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, pages 23–35, 1984.
S. Smith. Partial Objects in Type Theory. PhD thesis, Cornell University, 1989.
R. Weyhrauch. Prolegomena to a theory of formal reasoning. Artificial Intelligence, 13:133–170, 1980.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Constable, R.L., Allen, S.F., Howe, D.J. (1991). Reflecting the Open-Ended Computation System of Constructive Type Theory. In: Bauer, F.L. (eds) Logic, Algebra, and Computation. NATO ASI Series, vol 79. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-76799-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-76799-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-76801-9
Online ISBN: 978-3-642-76799-9
eBook Packages: Springer Book Archive