{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:22Z","timestamp":1725494302502},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_25","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"287-291","source":"Crossref","is-referenced-by-count":38,"title":["System Description: Teyjus\u2014A Compiler and Abstract Machine Based Implementation of \u03bbProlog"],"prefix":"10.1007","author":[{"given":"Gopalan","family":"Nadathur","sequence":"first","affiliation":[]},{"given":"Dustin J.","family":"Mitchell","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"25_CR1","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J.C. Filliatre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin, A. Sa\u00efbi, and B. Werner. The Coq Proof Assistant Reference Manual-Version V6.1. Technical Report 0203, INRIA, August 1997."},{"key":"25_CR2","unstructured":"Pascal Brisset and Olivier Ridoux. The compilation of \u03bbProlog and its execution with MALI. Publication Interne No 687, IRISA, Rennes, November 1992."},{"issue":"1","key":"25_CR3","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"Amy Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43\u201381, August 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR4","unstructured":"Richard A. Hagen and Peter J. Robinson. Qu-Prolog 4.3 reference manual. Technical Report 99-03, Software Verification Research Centre, School of Information Technology, University of Queensland, 1999."},{"issue":"4","key":"25_CR5","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1017\/S0960129500001559","volume":"2","author":"J. Hannan","year":"1992","unstructured":"John Hannan and Dale Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415\u2013459, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"issue":"1","key":"25_CR6","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0096-0551(94)90012-4","volume":"20","author":"K. Kwon","year":"1994","unstructured":"Keehang Kwon, Gopalan Nadathur, and Debra Sue Wilson. Implementing polymorphic typing in a logic programming language. Computer Languages, 20(1):25\u201342, 1994.","journal-title":"Computer Languages"},{"key":"25_CR7","unstructured":"Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379\u2013388. IEEE Computer Society Press, September 1987."},{"key":"25_CR8","doi-asserted-by":"publisher","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"},{"issue":"1","key":"25_CR9","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00881902","volume":"11","author":"G. Nadathur","year":"1993","unstructured":"Gopalan Nadathur. A proof procedure for the logic of hereditary Harrop formulas. Journal of Automated Reasoning, 11(1):115\u2013145, August 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"25_CR10","unstructured":"Gopalan Nadathur. An explicit substitution notation in a \u03bbProlog implementation. Technical Report TR-98-01, Department of Computer Science, University of Chicago, January 1998."},{"issue":"2","key":"25_CR11","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0743-1066(95)00037-K","volume":"25","author":"G. Nadathur","year":"1995","unstructured":"Gopalan Nadathur, Bharat Jayaraman, and Keehang Kwon. Scoping constructs in logic programming: Implementation problems and their solution. Journal of Logic Programming, 25(2):119\u2013161, November 1995.","journal-title":"Journal of Logic Programming"},{"key":"25_CR12","unstructured":"Gopalan Nadathur, Bharat Jayaraman, and Debra Sue Wilson. Implementation considerations for higher-order features in logic programming. Technical Report CS-1993-16, Department of Computer Science, Duke University, June 1993."},{"key":"25_CR13","unstructured":"Gopalan Nadathur and Dale Miller. An overview of \u03bbProlog. In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810\u2013827. MIT Press, August 1988."},{"key":"25_CR14","unstructured":"Gopalan Nadathur and Guanshan Tong. Realizing modularity in \u03bbProlog. Technical Report TR-97-07, Department of Computer Science, University of Chicago, August 1997. To appear in Journal of Functional and Logic Programming."},{"issue":"1-2","key":"25_CR15","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(97)00184-9","volume":"198","author":"G. Nadathur","year":"1998","unstructured":"Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1-2):49\u201398, 1998.","journal-title":"Theoretical Computer Science"},{"key":"25_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828of Lecture Notes in Computer Science. Springer Verlag, 1994."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logic programming in the LF logical framework. In G\u00e9rard Huet and Gordon D. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199\u2013208. ACM Press, June 1988.","DOI":"10.1145\/53990.54010"},{"key":"25_CR19","unstructured":"D.H.D. Warren. An abstract Prolog instruction set. Technical Note 309, SRI International, October 1983."},{"key":"25_CR20","unstructured":"Philip Wickline and Dale Miller. The Terzo 1.1b implementation of \u03bbProlog. Distribution in NJ-SML source files. See \n                    http:\/\/www.cse.psu.edu\/~dale\/lProlog\/\n                    \n                  , April 1997."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T22:08:14Z","timestamp":1551046094000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}