{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:31:54Z","timestamp":1725467514272},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055130","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T05:09:13Z","timestamp":1153976953000},"page":"67-86","source":"Crossref","is-referenced-by-count":0,"title":["Generating embeddings from denotational descriptions"],"prefix":"10.1007","author":[{"given":"Richard J.","family":"Boulton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1145\/6465.20890","volume":"8","author":"R. Bahlke","year":"1986","unstructured":"R. Bahlke and G. Snelting. The PSG system: Prom formal language definitions to interactive programming environments. ACM Transactions on Programming Languages and Systems, 8(4):547\u2013576, October 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"5_CR2","first-page":"531","volume-title":"volume 915 of Lecture Notes in Computer Science","author":"Y. Bertot","year":"1995","unstructured":"Y. Bertot and R. Fraer. Reasoning with executable specifications. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, Proceedings of the 6th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'95), volume 915 of Lecture Notes in Computer Science, pages 531\u2013545, Aarhus, Denmark, May 1995. Springer-Verlag."},{"key":"5_CR3","unstructured":"L. Birkedal and M. Welinder. Partial evaluation of Standard ML. DIKU-report 93\/22, DIKU, Department of Computer Science, University of Copenhagen, October 1993."},{"key":"5_CR4","unstructured":"R. J. Boulton. Syn: A single language for specifying abstract syntax trees, lexical analysis, parsing and pretty-printing. Technical Report 390, University of Cambridge Computer Laboratory, March 1996."},{"key":"5_CR5","first-page":"81","volume-title":"volume 1217 of Lecture Notes in Computer Science","author":"R. J. Boulton","year":"1997","unstructured":"R. J. Boulton. A tool to support formal reasoning about computer languages. In E. Brinksma, editor, Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), volume 1217 of Lecture Notes in Computer Science, pages 81\u201395, Enschede, The Netherlands, April 1997. Springer."},{"key":"5_CR6","first-page":"122","volume-title":"volume 971 of Lecture Notes in Computer Science","author":"G. Collins","year":"1995","unstructured":"G. Collins and D. Syme. A theory of finite maps. In Schubert et al. [15], pages 122\u2013137."},{"key":"5_CR7","first-page":"141","volume-title":"volume 780 of Lecture Notes in Computer Science","author":"E. L. Gunter","year":"1993","unstructured":"E. L. Gunter. A broader class of trees for recursive type definitions for HOL. In J. J. Joyce and C.-J. H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications (HUG '93), volume 780 of Lecture Notes in Computer Science, pages 141\u2013154, Vancouver, B.C., Canada, August 1993. Springer-Verlag, 1994."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"issue":"1","key":"5_CR9","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55\u201392, July 1991.","journal-title":"Information and Computation"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0167-6423(83)90008-4","volume":"3","author":"L. Paulson","year":"1983","unstructured":"L. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119\u2013149, 1983.","journal-title":"Science of Computer Programming"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"M. Pettersson and P. Pritzson. DML \u2014 a meta-language and system for the generation of practical and efficient compilers from denotational specifications. In Proceedings of the 4th International Conference on Computer Languages (ICCL'92), pages 127\u2013136. IEEE, April 1992.","DOI":"10.1109\/ICCL.1992.185475"},{"key":"5_CR12","first-page":"277","volume-title":"volume 971 of Lecture Notes in Computer Science","author":"R. Reetz","year":"1995","unstructured":"R. Reetz. Deep embedding VHDL. In Schubert et al. [15]., pages 277\u2013292."},{"key":"5_CR13","first-page":"378","volume-title":"volume 859 of Lecture Notes in Computer Science","author":"R. Reetz","year":"1994","unstructured":"R. Reetz and T. Kropf. Simplifying deep embedding: A formalised code generator. In T. F. Melham and J. Camilleri, editors, Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 859 of Lecture Notes in Computer Science, pages 378\u2013390, Valletta, Malta, September 1994. Springer-Verlag."},{"key":"5_CR14","first-page":"293","volume-title":"volume 971 of Lecture Notes in Computer Science","author":"F. Regensburger","year":"1995","unstructured":"F. Regensburger. HOLCF: Higher order logic of computable functions. In Schubert et al. [15]., pages 293\u2013307."},{"volume-title":"volume 971 of Lecture Notes in Computer Science","year":"1995","key":"5_CR15","unstructured":"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, volume 971 of Lecture Notes in Computer Science, Aspen Grove, UT, USA, September 1995. Springer-Verlag."},{"key":"5_CR16","first-page":"381","volume-title":"volume 1125 of Lecture Notes in Computer Science","author":"K. Slind","year":"1996","unstructured":"K. Slind. Function definition in higher-order logic. In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96), volume 1125 of Lecture Notes in Computer Science, pages 381\u2013397, Turku, Finland, August 1996. Springer."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"P. Wadler. The essence of functional programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1\u201314, Albuquerque, New Mexico, USA, January 1992.","DOI":"10.1145\/143165.143169"},{"key":"5_CR18","first-page":"340","volume-title":"volume 971 of Lecture Notes in Computer Science","author":"M. Welinder","year":"1995","unstructured":"M. Welinder. Very efficient conversions. In Schubert et al. [15], pages 340\u2013352."}],"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\/BFb0055130","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,11]],"date-time":"2019-02-11T13:43:11Z","timestamp":1549892591000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055130"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0055130","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}