Abstract
This paper describes a translation of the complex calculus of dependent type theory into the relatively simpler higher order logic originally introduced by Church. In particular, it shows how type dependency as found in Martin-Löf's Intuitionistic Type Theory can be simulated in the formulation of higher order logic mechanized by the HOL theoremproving system. The outcome is a theorem prover for dependent type theory, built on top of HOL, that allows natural and flexible use of set-theoretic notions. A bit more technically, the language of the resulting theorem-prover is the internal language of a (boolean) topos (as formulated by Phoa).
Research carried out during 1991–92 at the University of Cambridge under SERC grant GR/F 36675.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Church, ‘A Formulation of the Simple Theory of Types', The Journal of Symbolic Logic, vol. 5 (1940), pp. 56–68.
A. Felty, ‘Encoding Dependent Types in an Intuitionistic Logic', in Logical Frameworks, edited by G. Huet and G. Plotkin (Cambridge University Press, 1991), pp. 215–251.
M. Gordon, ‘HOL: A Machine Oriented Formulation of Higher Order Logic', Technical Report 68, Computer Laboratory, University of Cambridge, revised version (July 1985).
M. J. C. Gordon, ‘HOL: A Proof Generating System for Higher-Order Logic', in VLSI Specification, Verification and Synthesis, edited by G. Birtwistle and P. A. Subrahmanyam, Kluwer International Series in Engineering and Computer Science (Kluwer, 1988), pp. 73–128.
M. J. C. Gordon and T. F. Melham (eds.), Introduction to HOL: A theorem proving environment for higher order logic, forthcoming book (Cambridge University Press, 1993).
M. J. Gordon, A. J. Milner, and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science, vol. 78 (Springer-Verlag, 1979).
F. K. Hanna, N. Daeche, and M. Longley, ‘Specification and Verification Using Dependent Types', IEEE Transactions on Software Engineering, vol. 16, no. 9 (September 1990), pp. 949–964.
B. P. F. Jacobs, Categorical Type Theory (Ph.D. dissertation, University of Nijmgen, 1991).
M. Leeser, ‘Using Nuprl for the verification and synthesis of hardware', in Mechanized Reasoning and Hardware Design: a Discussion Meeting held at the Royal Society, October 1991, edited by C. A. R. Hoare and M. J. C. Gordon, Prentice Hall International Series in Computer Science (Prentice Hall, 1992), pp. 49–68.
A. C. Leisenring, Mathematical Logic and Hubert's e-Symbol, University Mathematical Series (Macdonald & Co., 1969).
P. Martin-Löf, Intuitionistic Type Theory (Bibliopolis, Naples, 1984).
T. F. Melham, ‘Automating Recursive Type Definitions in Higher Order Logic', in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341–386.
B. Nordström, K. Petersson, and J. M. Smith, Programming in Martin-Lof's Type Theory: An Introduction, International Series of Monographs on Computer Science 7 (Oxford University Press, 1990).
W. Phoa, ‘An introduction to fibrations, topos theory, the effective topos and modest sets', Technical Report ECS-LFCS-92-208, LFCS, Department of Computer Science, University of Edinburgh (April 1992).
G. Sundholm, ‘Proof Theory and Meaning', in Alternatives in Classical Logic, vol. 3 of Handbook of Philosophical Logic, edited by D. Gabbay and F. Guenthner, 4 vols. (D. Reidel, 1983–9), pp. 471–506.
A. S. Troelstra, ‘On the Syntax of Martin-Löf's Theories', Theoretical Computer Science, vol. 51, nos. 1–2 (1987), pp. 1–26.
A. S. Troelstra and D. van Dalen, Constructivism in Mathematics: An Introduction, Studies in Logic and the Foundations of Mathematics, 2 vols. (North Holland, 1988).
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacobs, B., Melham, T. (1993). Translating dependent type theory into higher order logic. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037108
Download citation
DOI: https://doi.org/10.1007/BFb0037108
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56517-8
Online ISBN: 978-3-540-47586-6
eBook Packages: Springer Book Archive