{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:45:53Z","timestamp":1754487953087},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_80","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:49:51Z","timestamp":1330292991000},"page":"186-200","source":"Crossref","is-referenced-by-count":2,"title":["An embedding of Ruby in Isabelle"],"prefix":"10.1007","author":[{"given":"Ole","family":"Rasmussen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"17_CR1","first-page":"129","volume-title":"Experience with embedding hardware description languages in HOL","author":"R. Boulton","year":"1992","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van Tassel. Experience with embedding hardware description languages in HOL. In V. Stavridou, T. F. Melham, and R. T. Boute, editors, IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 129\u2013156, Nijmegen, June 1992. North-Holland\/Elsevier."},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"A. Dent and K. Hanna. Reasoning about array structures using a dependently typed logic. In CHDL '93. Elsevier Publishers, 1993.","DOI":"10.1016\/B978-0-444-81641-2.50022-8"},{"key":"17_CR3","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":"17_CR4","unstructured":"F. K. Hanna, M. Longley, and N. Daeche. Formal synthesis of digital systems. In Luc Claesen, editor, VLSI Design Methods. Elsevier Publishers, 1990."},{"key":"17_CR5","unstructured":"G. Jones and M. Sheeran. Circuit design in Ruby. In J. Staunstrup, editor, Formal Methods for VLSI Design. Elsevier Publishers, 1990."},{"key":"17_CR6","unstructured":"G. Jones and M. Sheeran. Relations and refinement in circuit design. In Morgan, editor, Proc. BCS FACS Workshop on Refinement. Springer-Verlag Workshop in Computing, 1990."},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1098\/rsta.1992.0025","volume":"339","author":"M. Leeser","year":"1992","unstructured":"Mariam Leeser. Using Nuprl for the verification and synthesis of hardware. Philosophical Trans. of the Royal Soc. London A, 339:49\u201368, 1992.","journal-title":"Philosophical Trans. of the Royal Soc. London A"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348\u2013375, 1978.","journal-title":"Journal of Computer and System Sciences"},{"issue":"3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"L. C. Paulson","year":"1993","unstructured":"L. C. Paulson. Set theory for verification: I. from foundations to functions. Journal of Automated Reasoning, 11(3):353\u2013389, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Alan Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 148\u2013161, Nancy, France, June 1994. Springer-Verlag LNAI 814.","DOI":"10.1007\/3-540-58156-1_11"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer-Verlag LNCS 828, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"17_CR12","unstructured":"O. Rasmussen. A Ruby proof system. Technical Report ID-TR: 1995-161, Dept. of Computer Science, Technical University of Denmark, 1995."},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Lars Rossen. Ruby algebra. In G. Jones and M. Sheeran, editors, Designing Correct Circuits, Oxford 1990, Workshops in Computing, pages 297\u2013312. Springer-Verlag Workshop in Computing, 1991.","DOI":"10.1007\/978-1-4471-3544-9_16"},{"key":"17_CR14","first-page":"231","volume-title":"CHDL '93","author":"R. Sharp","year":"1993","unstructured":"R. Sharp and O. Rasmussen. Transformational rewriting with Ruby. In CHDL '93, pages 231\u2013248. Elsevier Science Publishers (North-Holland), 1993."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"R. Sharp and O. Rasmussen. Using a language of functions and relations for VLSI specification. In Functional programming and Computer Architecture, FPCA '95, pages 45\u201354, June 1995.","DOI":"10.1145\/224164.224180"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_80.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:40:23Z","timestamp":1640947223000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_80"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_80","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}