Abstract
Nuprl's constructive type theory, like conventional set theory, buys much of its expressive power and flexibility at the cost of giving up the more manageable kind of type system found in other logics. Many of the benefits and costs of Nuprl's approach to type theory are related to the fact that terms are untyped in the sense that there is no algorithm to determine from the syntax of an expression what type, if any, it is a member of. We have designed and implemented an annotation scheme where terms are decorated with types in such a way that types can (almost always) be efficiently maintained during inference. These type annotations in a term are obtained using Nuprl's existing type checking and type inference machinery, which use contextual information in the term to determine types for subterms.
Our implementation still needs some tuning for performance, but the current working prototype already gives roughly a factor of 10 speedup in term rewriting (the main workhorse in Nuprl proofs). In addition, tactics such as conditional rewriting are now more effective because they can quickly and more reliably obtain the types of terms.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
C.-T. Chou and D. Peled. Verifying a model-checking algorithm. In Tools and Algorithms for the Construction and Analysis of Systems, number 1055 in LNCS, pages 241–257, Passau, Germany, 1996. Springer-Verlag.
R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.
A. Felty, D. Howe, and F. Stomp. Protocol verification in nuprl. In CAV'98, Lecture Notes in Computer Science. Springer-Verlag, 1998.
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge, UK, 1993.
D. J. Howe. On computational open-endedness in Martin-Löf's type theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 162–172. IEEE Computer Society, 1991.
D. J. Howe. Semantics foundations for embedding HOL in Nuprl. In M. Wirsing and M. Nivat, editors, Algebraic Methodology and Software Technology, volume 1101 of Lecture Notes in Computer Science, pages 85–101, Berlin, 1996. Springer-Verlag.
P. B. Jackson. Exploring abstract algebra in constructive type theory. In A. Bundy, editor, 12th Conference on Automated Deduction, Lecture Notes in Artifical Intelligence. Springer, June 1994.
S. Owre and N. Shankar. The formal semantics of PVS. Technical report, SRI, August 1997.
B. Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Howe, D.J. (1998). A type annotation scheme for Nuprl. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055138
Download citation
DOI: https://doi.org/10.1007/BFb0055138
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64987-8
Online ISBN: 978-3-540-49801-8
eBook Packages: Springer Book Archive