Translating dependent type theory into higher order logic Export

@incollection{citeulike:2997640, 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\"{o}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).}, author = {Jacobs, Bart and Melham, Tom}, citeulike-article-id = {2997640}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/BFb0037108}, doi = {10.1007/BFb0037108}, journal = {Typed Lambda Calculi and Applications}, keywords = {logic, type-theory}, pages = {209--229}, posted-at = {2008-07-15 02:34:56}, priority = {2}, title = {Translating dependent type theory into higher order logic}, url = {http://dx.doi.org/10.1007/BFb0037108}, year = {1993} }

TY - CHAP ID - citeulike:2997640 L3 - citeulike-article-id:2997640 N2 - 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). JF - Typed Lambda Calculi and Applications EP - 229 TI - Translating dependent type theory into higher order logic SP - 209 KW - logic KW - type-theory AU - Jacobs, Bart AU - Melham, Tom PY - 1993/// UR - http://dx.doi.org/10.1007/BFb0037108 ER -