{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T18:40:56Z","timestamp":1771008056497,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540615873","type":"print"},{"value":"9783540706410","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105393","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"1-16","source":"Crossref","is-referenced-by-count":7,"title":["Translating specifications in VDM-SL to PVS"],"prefix":"10.1007","author":[{"given":"Sten","family":"Agerholm","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"S. Agerholm. A HOL Basis for Reasoning about Functional Programs. PhD thesis, BRICS, Department of Computer Science, University of Aarhus, December 1994. Available as Technical Report RS-94-44.","DOI":"10.7146\/brics.v1i44.21598"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"S. Agerholm. LCF examples in HOL. The Computer Journal, 38(2), 1995.","DOI":"10.1093\/comjnl\/38.2.121"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"J. Bicarregui, J. Fitzgerald, P. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner's Guide. FACIT. Springer-Verlag, 1994. ISBN 3-540-19813-X.","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"1_CR4","unstructured":"R. J. Boulton, A. D. Gordon, M. J. C. Gordon, J. R. Harrison, J. M. 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, Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10\/WG 10.2 International Conference, IFIP Transactions A-10, pages 129\u2013156. North-Holland, June 1992."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"G. Collins and D. Syme. A theory of finite maps. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications. Springer-Verlag, September 1995. LNCS 971.","DOI":"10.1007\/3-540-60275-5_61"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"John Dawes. The VDM-SL Reference Guide. Pitman, 1991. ISBN 0-273-03151-1.","DOI":"10.1201\/9781482267419"},{"issue":"9","key":"1_CR7","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/185009.185028","volume":"29","author":"R. Elmstr\u00f8m","year":"1994","unstructured":"R. Elmstr\u00f8m, P. G. Larsen, and P. B. Lassen. The IFAD VDM-SL Toolbox: A practical approach to formal specifications. ACM Sigplan Notices, 29(9):77\u201380, September 1994.","journal-title":"ACM Sigplan Notices"},{"key":"1_CR8","unstructured":"M. Gordon. Notes on PVS from a HOL perspective. University of Cambridge Computer Laboratory, see http:\/\/www.cl.cam.ac.uk\/users\/mjcg\/PVS\/html, August 1995."},{"key":"1_CR9","unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theoremproving Environment for Higher-Order Logic. Cambridge University Press, 1993."},{"key":"1_CR10","unstructured":"IFAD World Wide Web page. http:\/\/www.ifad.dk."},{"key":"1_CR11","unstructured":"P. G. Larsen. Towards Proof Rules for VDM-SL. PhD thesis, Technical University of Denmark, Department of Computer Science, March 1995. ID-TR:1995-160."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"1_CR13","unstructured":"PVS World Wide Web page. http:\/\/www.csl.sri.com\/pvs\/overview.html."},{"issue":"5","key":"1_CR14","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1093\/comjnl\/35.5.514","volume":"35","author":"H. S\u00f8ndergaard","year":"1992","unstructured":"H. S\u00f8ndergaard and P. Sestoft. Non-determinism in functional languages. The Computer Journal, 35(5):514\u2013523, October 1992.","journal-title":"The Computer Journal"}],"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\/BFb0105393","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,15]],"date-time":"2021-12-15T22:51:42Z","timestamp":1639608702000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105393"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0105393","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}