This paper describes a translation of the complex calculus of dependent type theory inLo the relatively simpler higher order logic originally introduced by Church. In particular, it shows how type dependency as Found is Martin-Löf’s Intuitionistic Type Theory can be simulated in the formulation os higher order logic mechanized by the HOD theorem-proving system. The outcome is a theorem prover for dependent type theory, built on top os HOL, that allows natural and flexible use of set-theoretic notions. A bit more technically, the language of the resulting theorem-prover is the in~ernal language of a (boolean) topos (as formulated by Phoa).
CITATION STYLE
Jacobs, B., & Melham, T. (1993). Translating dependent type theory into higher order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 664 LNCS, pp. 209–229). Springer Verlag. https://doi.org/10.1007/bfb0037108
Mendeley helps you to discover research relevant for your work.