{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T10:54:03Z","timestamp":1766400843130},"publisher-location":"Berlin\/Heidelberg","reference-count":17,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540565175"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037108","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"209-229","source":"Crossref","is-referenced-by-count":10,"title":["Translating dependent type theory into higher order logic"],"prefix":"10.1007","author":[{"given":"Bart","family":"Jacobs","sequence":"first","affiliation":[]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, \u2018A Formulation of the Simple Theory of Types', The Journal of Symbolic Logic, vol. 5 (1940), pp. 56\u201368.","journal-title":"The Journal of Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"A. Felty, \u2018Encoding Dependent Types in an Intuitionistic Logic', in Logical Frameworks, edited by G. Huet and G. Plotkin (Cambridge University Press, 1991), pp. 215\u2013251.","key":"15_CR2","DOI":"10.1017\/CBO9780511569807.010"},{"unstructured":"M. Gordon, \u2018HOL: A Machine Oriented Formulation of Higher Order Logic', Technical Report 68, Computer Laboratory, University of Cambridge, revised version (July 1985).","key":"15_CR3"},{"doi-asserted-by":"crossref","unstructured":"M. J. C. Gordon, \u2018HOL: 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\u2013128.","key":"15_CR4","DOI":"10.1007\/978-1-4613-2007-4_3"},{"unstructured":"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).","key":"15_CR5"},{"doi-asserted-by":"crossref","unstructured":"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).","key":"15_CR6","DOI":"10.1007\/3-540-09724-4"},{"issue":"no.9","key":"15_CR7","doi-asserted-by":"crossref","first-page":"949","DOI":"10.1109\/32.58783","volume":"16","author":"F. K. Hanna","year":"1990","unstructured":"F. K. Hanna, N. Daeche, and M. Longley, \u2018Specification and Verification Using Dependent Types', IEEE Transactions on Software Engineering, vol. 16, no. 9 (September 1990), pp. 949\u2013964.","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"B. P. F. Jacobs, Categorical Type Theory (Ph.D. dissertation, University of Nijmgen, 1991).","key":"15_CR8"},{"doi-asserted-by":"crossref","unstructured":"M. Leeser, \u2018Using 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\u201368.","key":"15_CR9","DOI":"10.1098\/rsta.1992.0025"},{"unstructured":"A. C. Leisenring, Mathematical Logic and Hubert's e-Symbol, University Mathematical Series (Macdonald & Co., 1969).","key":"15_CR10"},{"key":"15_CR11","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"P. Martin-L\u00f6f, Intuitionistic Type Theory (Bibliopolis, Naples, 1984)."},{"doi-asserted-by":"crossref","unstructured":"T. F. Melham, \u2018Automating 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\u2013386.","key":"15_CR12","DOI":"10.1007\/978-1-4612-3658-0_9"},{"unstructured":"B. Nordstr\u00f6m, 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).","key":"15_CR13"},{"unstructured":"W. Phoa, \u2018An 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).","key":"15_CR14"},{"doi-asserted-by":"crossref","unstructured":"G. Sundholm, \u2018Proof 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\u20139), pp. 471\u2013506.","key":"15_CR15","DOI":"10.1007\/978-94-009-5203-4_8"},{"issue":"nos.1\u20132","key":"15_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90047-8","volume":"51","author":"A. S. Troelstra","year":"1987","unstructured":"A. S. Troelstra, \u2018On the Syntax of Martin-L\u00f6f's Theories', Theoretical Computer Science, vol. 51, nos. 1\u20132 (1987), pp. 1\u201326.","journal-title":"Theoretical Computer Science"},{"unstructured":"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).","key":"15_CR17"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037108.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:22:03Z","timestamp":1607552523000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037108"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0037108","relation":{},"subject":[]}}