{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:32:38Z","timestamp":1742635958243},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540523352"},{"type":"electronic","value":"9783540469636"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52335-9_58","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:31:02Z","timestamp":1330205462000},"page":"246-274","source":"Crossref","is-referenced-by-count":7,"title":["A formulation of the simple theory of types (for Isabelle)"],"prefix":"10.1007","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"16_CR1","unstructured":"Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press, 1986."},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Peter B. Andrews, Dale A. Miller, Eve L. Cohen, and Frank Pfenning. Automating higher-order logic. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, pages 169\u2013192, American Mathematical Society, 1984.","DOI":"10.1090\/conm\/029\/09"},{"key":"16_CR3","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/BF01887198","volume":"1","author":"B. Roland","year":"1989","unstructured":"Roland Backhouse, Paul Chisholm, Grant Malcolm, and Erik Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1:19\u201384, 1989.","journal-title":"Formal Aspects of Computing"},{"key":"16_CR4","unstructured":"Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, 1987."},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"C. Alonzo","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Avra J. Cohn. A proof of correctness of the VIPER microprocessor: the first level. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 27\u201371, Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"16_CR7","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panagaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall International, 1986."},{"key":"16_CR8","unstructured":"Thierry Coquand. An analysis of Girard's paradox. In Symposium on Logic in Computer Science, pages 227\u2013236, IEEE Computer Society Press, 1986."},{"key":"16_CR9","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"C. Thierry","year":"1988","unstructured":"Thierry Coquand and G\u00e8rard Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"16_CR10","unstructured":"Andrzej Borzyszkowski et al. Towards a Set-Theoretic Type Theory. Technical Report, Polish Academy of Sciences, Institute of Computer Science, Gda\u0144sk, 1988."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Michael P. Fourman. The logic of topoi. In J. Barwise, editor, Handbook of Mathematical Logic, pages 1053\u20131090, North-Holland, 1977.","DOI":"10.1016\/S0049-237X(08)71128-5"},{"key":"16_CR12","unstructured":"Jean-Yves Girard. Proofs and Types. Cambridge University Press, 1989. Translated by Yves LaFont and Paul Taylor."},{"key":"16_CR13","unstructured":"Kurt G\u00f6del. Russell's mathematical logic. In Paul Benacerraf and Hilary Putnam, editors, Philosophy of Mathematics: Selected Readings, Cambridge University Press, 1983. Essay first published in 1944."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Michael J. C. Gordon. HOL: a proof generating system for higher-order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73\u2013128, Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"16_CR15","unstructured":"William S. Hatcher. The Logical Foundations of Mathematics. Pergammon Press, 1982."},{"key":"16_CR16","unstructured":"J. Roger Hindley and Jonathon P. Seldin. Introduction to Combinators and \u03bb-Calculus. Cambridge University Press, 1986."},{"key":"16_CR17","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"G. P. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"16_CR18","unstructured":"G\u00e9rard Huet. Induction principles formalized in the Calculus of Constructions. In Programming of Future Generation Computers, pages 205\u2013216, Elsevier, 1988."},{"key":"16_CR19","unstructured":"J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986."},{"key":"16_CR20","unstructured":"A. C. Leisenring. Mathematical Logic and Hilbert's \u03b5-Symbol. MacDonald, 1969."},{"key":"16_CR21","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In C. A. R. Hoare and J. C. Shepherdson, editors, Mathematical Logic and Programming Languages, pages 167\u2013184, Prentice-Hall International, 1985."},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Thomas F. Melham. Automating recursive type definitions in higher order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341\u2013386, Springer-Verlag, 1989.","DOI":"10.1007\/978-1-4612-3658-0_9"},{"key":"16_CR23","unstructured":"G. Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, 1987."},{"key":"16_CR24","unstructured":"Philippe No\u00ebl. Experimenting with Isabelle in ZF Set Theory. Technical Report, University of Cambridge Computer Laboratory, 1989. Preprint."},{"key":"16_CR25","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan Smith. Programming in Martin-L\u00f6f's type theory. An introduction. Oxford University Press, 1989. In press."},{"key":"16_CR26","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1016\/S0747-7171(86)80002-5","volume":"2","author":"L. C. Paulson","year":"1986","unstructured":"Lawrence C. Paulson. Constructing recursion operators in intuitionistic type theory. Journal of Symbolic Computation, 2:325\u2013355, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"16_CR27","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"L. C. Paulson","year":"1989","unstructured":"Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Auiomaied Reasoning, 5:363\u2013397, 1989.","journal-title":"Journal of Auiomaied Reasoning"},{"key":"16_CR28","unstructured":"Lawrence C. Paulson. Isabelle: the next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, Academic Press, 1989? In press."},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"16_CR30","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0167-6423(85)90009-7","volume":"5","author":"L. C. Paulson","year":"1985","unstructured":"Lawrence C. Paulson. Verifying the unification algorithm in LCF. Science of Computer Programming, 5:143\u2013170, 1985.","journal-title":"Science of Computer Programming"},{"key":"16_CR31","unstructured":"Anne Salvesen. On Information Discharging and Retrieval in Martin-L\u00f6f's Type Theory. PhD thesis, University of Oslo, 1989. Report 803, Norwegian Computing Center, Oslo."},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Dana Scott. Identity and existence in intuitionistic logic. In M. P. Fourman, editor, Applications of Sheaves, pages 660\u2013696, Springer-Verlag, 1979. Lecture Notes in Mathematics 753.","DOI":"10.1007\/BFb0061839"},{"key":"16_CR33","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1145\/9758.11326","volume":"9","author":"S. Soko\u0142owski","year":"1987","unstructured":"Stefan Soko\u0142owski. Soundness of Hoare's logic: an automatic proof using LCF. ACM Transactions on Programming Languages and Systems, 9:100\u2013120, 1987.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR34","unstructured":"J. M. Spivey. Understanding Z: A Specification Language and its Formal Semantics. Cambridge University Press, 1988."},{"key":"16_CR35","unstructured":"Patrick Suppes. Axiomatic Set Theory. Dover, 1972."},{"key":"16_CR36","unstructured":"A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, 1962. Paperback edition to *56, abridged from the 2nd edition (1927)."}],"container-title":["Lecture Notes in Computer Science","COLOG-88"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52335-9_58.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:23:56Z","timestamp":1605648236000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52335-9_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540523352","9783540469636"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-52335-9_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}