{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:42:11Z","timestamp":1747546931865,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"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\/bfb0105400","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"109-124","source":"Crossref","is-referenced-by-count":3,"title":["A proof tool for reasoning about functional programs"],"prefix":"10.1007","author":[{"given":"Graham","family":"Collins","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"8_CR1","unstructured":"Samson Abramsky. The Lazy Lambda Calculus. In David Turner, editor, Research Topics in Functional Programming, pages 65\u2013116. Addison-Wesley, 1990."},{"key":"8_CR2","unstructured":"Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert, and John Van Tassel. Experience with embedding hardware description languages in HOL. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP WG10.2 International Conference, Nijmegen, pages 129\u2013156. North-Holland, June 1992."},{"key":"8_CR3","unstructured":"A. Cant and M.A. Ozols. A verification environment for ML programs. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, San Francisco, California, June 1992."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Graham Collins. Supporting Reasoning about Functional Programs: An Operational Approach. In 1995 Glasgow Workshop on Functional Programming, Electroninc Workshops in Computer Science. Springer-Verlag, 1996.","DOI":"10.14236\/ewic\/FP1995.4"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Graham Collins and Donald Syme. A Theory of Finite Maps. In E. Thomas Schubert, Phillip J. Windley, and Hames Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science, pages 122\u2013137. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60275-5_61"},{"key":"8_CR6","unstructured":"Andrew D. Gordon. Bisimilarity as a Theory of Functional Programming. Technical Report NS-95-3, Basic Research in Computer Science, University of Aarhus, July 1995."},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Andrew D. Gordon. A Tutorial on Co-induction and Functional Programming. In 1994 Glasgow Workshop on Functional Programming, Workshops in Computer Science, pages 78\u201395. Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4471-3573-9_6"},{"key":"8_CR8","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"John Harrison. Inductive definitions: automation and application. In E. Thomas Schubert, Phillip J. Windley, and Hames Alves-Foss, editors, Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science, pages 200\u2013213. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-60275-5_66"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Savi Maharaj and Elsa Gunter. Studying the ML Module System in HOL. In Tom Melham and Juanito Camilleri, editors, Higher Order Logic Theorem Proving and its Applications, volume 859 of Lecture Notes in Computer Science, pages 346\u2013361. Springer-Verlag, September 1994.","DOI":"10.1007\/3-540-58450-1_53"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Tom F. Melham. A Package for Inductive Relation Definitions in HOL. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1992, pages 350\u2013357. IEEE Computer Society Press, 1992.","DOI":"10.1109\/HOL.1991.596299"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Donald Syme. Reasoning with the Formal Definition of Standard ML in HOL. In Higher Order Logic Theorem Proving and Its Applications, volume 780 of Lecture Notes in Computer Science, pages 43\u201360. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57826-9_124"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Myra VanInwegen and Elsa Gunter. HOL-ML. In J. J. Joyce and C. J. H. Seger, editors, Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science, pages 61\u201374. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-57826-9_125"}],"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\/BFb0105400","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T23:11:47Z","timestamp":1741907507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105400"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0105400","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}