{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T04:24:24Z","timestamp":1648787064207},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540633792","type":"print"},{"value":"9783540695264","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0028383","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:50:11Z","timestamp":1132642211000},"page":"17-32","source":"Crossref","is-referenced-by-count":4,"title":["Executing formal specifications by translation to higher order logic programming"],"prefix":"10.1007","author":[{"given":"James H.","family":"Andrews","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,17]]},"reference":[{"issue":"3\/4","key":"2_CR1","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0743-1066(93)90043-G","volume":"16","author":"H. Ait-Kaci","year":"1993","unstructured":"Hassan Ait-Kaci and Andreas Podelski. Towards a meaning of Life. Journal of Logic Programming, 16(3\/4):195, July 1993.","journal-title":"Journal of Logic Programming"},{"key":"2_CR2","unstructured":"Pascal Brisset and Olivier Ridoux. The compilation of Lambda Prolog and its execution with MALI. Technical Report 1831, INRIA, 1993."},{"key":"2_CR3","unstructured":"Albert Camilleri. Simulation as an aid to verification using the HOL theorem prover. Technical Report 150, University of Cambridge Computer Laboratory, October 1988."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Michael R. Donat. Automating formal specification-based testing. In TAPSOFT: 7th International Joint Conference on Theory and Practice of Software Engineering, April 1997.","DOI":"10.1007\/BFb0030644"},{"key":"2_CR5","first-page":"323","volume-title":"Proceedings of the ACM Conference on Lisp and Functional Programming","author":"J. Harman","year":"1990","unstructured":"John Harman and Dale Miller. From operational semantics to abstract machines: Preliminary results. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 323\u2013332, Nice, France, June 1990. ACM Press."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Jeffrey J. Joyce, Nancy A. Day, and Michael R. Donat. S: A machine readable specification notation based on higher order logic. In Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, volume 859 of LNCS. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58450-1_49"},{"key":"2_CR7","unstructured":"Jeffrey J. Joyce, Nancy A. Day, and Michael R. Donat. S \u2014 a general-purpose specification notation. Draft report, 1996."},{"issue":"3","key":"2_CR8","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1145\/129393.129398","volume":"14","author":"J. Jaffar","year":"1992","unstructured":"Joxan Jaffar, Spiro Michaylov, Peter J. Stuckey, and Roland H. C. Yap. The CLP(R) language and system. ACM Transactions on Programming Languages and Systems, 14(3):339\u2013395, July 1992.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR9","first-page":"22","volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science","author":"G. Kahn","year":"1987","unstructured":"G. Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, volume 247 of LNCS, pages 22\u201339, Passau, Federal Republic of Germany, Feb 1987. Springer."},{"key":"2_CR10","volume-title":"Computational Logic: Essays in Honor of Alan Robinson","author":"D. W. Loveland","year":"1991","unstructured":"Donald W. Loveland and David W. Reed. near-Horn Prolog for compilation. In Computational Logic: Essays in Honor of Alan Robinson, Cambridge, Mass., 1991. MIT Press."},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"2_CR12","unstructured":"Dale A. Miller. Lambda Prolog homepage. http:\/\/www.cis.upenn.edu\/ dale\/lProlog\/index. html\/,1996."},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Dale A. Miller and Gopalan Nadathur. Higher-order logic programming. In Proceedings of the Third International Logic Programming Conference, Imperial College, London, July 1986.","DOI":"10.1007\/3-540-16492-8_94"},{"key":"2_CR14","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Chetan R. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science. IEEE, 1991.","DOI":"10.1109\/LICS.1991.151634"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Monica Nesi. Value-passing CCS in HOL. In HOL Users' Group Workshop, Vancouver, August 1993.","DOI":"10.1007\/3-540-57826-9_147"},{"key":"2_CR17","unstructured":"SICS (Swedish Institute of Computer Science). SICStus Prolog user's manual. Technical report, Swedish Institute of Computer Science, Kista, Sweden, April 1994."},{"key":"2_CR18","volume-title":"Higher Order Logic Theorem Proving and its Applications","author":"P. Sreeranga Rajan","year":"1992","unstructured":"P. Sreeranga Rajan. Executing HOL specifications: Towards an evaluation semantics for classical higher order logic. In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium, September 1992. Elsevier."}],"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\/BFb0028383","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:49:16Z","timestamp":1586573356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0028383"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540633792","9783540695264"],"references-count":18,"URL":"http:\/\/dx.doi.org\/10.1007\/bfb0028383","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1997]]}}}