{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:45Z","timestamp":1725631965186},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105420","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T16:17:00Z","timestamp":1320855420000},"page":"431-446","source":"Crossref","is-referenced-by-count":4,"title":["A mechanisation of computability theory in HOL"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Zammit","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"28_CR1","volume-title":"A User's Guide to ALF","author":"T. Altenkirch","year":"1994","unstructured":"Thorsten Altenkirch, Veronica Gaspes, Bengt Nordstr\u00f6m, and Bj\u00f6rn von Sydow. A User's Guide to ALF. Chalmers University of Technology, Sweden, May 1994."},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"J. Camilleri and V. Zammit. Symbolic animation as a proof tool. In T.F. Melham and J. Camilleri, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 859 of Lecture Notes in Computer Science, pages 113\u2013127, Malta, September 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58450-1_38"},{"key":"28_CR3","unstructured":"C. Cornes et al. The Coq Proof Assistant Reference Manual, Version 5.10. Rapport technique RT-0177, INRIA, 1995."},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"N.J. Cutland. Computability: An introduction to recursive function theory. Cambridge University Press, 1980.","DOI":"10.1017\/CBO9781139171496"},{"key":"28_CR5","unstructured":"M. Gordon. HOL a machine oriented formulation of higher order logic. Technical Report TR-68, Computer Laboratory, Cambridge University, July 1985."},{"key":"28_CR6","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Lena Magnusson and Bengt Nordstr\u00f6m. The ALF proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, pages 213\u2013237. Springer-Verlag LNCS 806, 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"28_CR8","unstructured":"T.F. Melham. Using recursive types to reason about hardware and higher order logic. In G.J. Milne, editor, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 27\u201350, Glasgow, Scotland, July 1988. IFIP WG 10.2, North-Holland."},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"L.C. Paulson. Logic and computation: interactive proof with Cambridge LCF. Cambridge tracts in theoretical computer science, 1987.","DOI":"10.1017\/CBO9780511526602"},{"key":"28_CR10","unstructured":"H. Rogers. Theory of recursive functions and effective computability. McGraw-Hill, 1967."},{"key":"28_CR11","unstructured":"J.C. Shepherdson and H.E. Sturgis. Computability of recursive functions. Technical Report 10, J. Assoc. Computing Machinery, 1967."},{"key":"28_CR12","unstructured":"R. Sommerhalder and S.C. van Westrhenen. The theory of computability: programs, machines, effectiveness and feasibility. Addison-Wesley publishing company, 1988."},{"key":"28_CR13","unstructured":"G.J. Tourlakis. Computability. Reston Publishing Company, 1984."},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"P.J. Windley. Specifying instruction-set architectures in HOL: A primer. In T.F. Melham and J. Camilleri, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 859 of Lecture Notes in Computer Science, pages 440\u2013456, Malta, September 1994. Springer-Verlag.","DOI":"10.1007\/3-540-58450-1_59"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105420","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T05:44:36Z","timestamp":1560923076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105420"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0105420","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}