A type annotation scheme for Nuprl
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.
KeywordsInference Rule Type Theory Expressive Power Proof Obligation Annotation Scheme
Unable to display preview. Download preview PDF.
- 1.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.Google Scholar
- 2.R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.Google Scholar
- 3.A. Felty, D. Howe, and F. Stomp. Protocol verification in nuprl. In CAV'98, Lecture Notes in Computer Science. Springer-Verlag, 1998.Google Scholar
- 4.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.Google Scholar
- 5.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.Google Scholar
- 6.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.Google Scholar
- 7.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.Google Scholar
- 8.S. Owre and N. Shankar. The formal semantics of PVS. Technical report, SRI, August 1997.Google Scholar
- 9.B. Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software.Google Scholar