{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T14:05:23Z","timestamp":1761919523806},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540513056"},{"type":"electronic","value":"9783540461913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51305-1_13","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:54:19Z","timestamp":1330203259000},"page":"239-255","source":"Crossref","is-referenced-by-count":6,"title":["Deriving mixed evaluation from standard evaluation for a simple functional language"],"prefix":"10.1007","author":[{"given":"John","family":"Hannan","sequence":"first","affiliation":[]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"R. Burstall and Furio Honsell. A natural deduction treatment of operational semantics. In Foundations of Software Technology and Theoretical Computer Science, pages 250\u2013269, Springer-Verlag LNCS, Vol. 338, 1988.","DOI":"10.1007\/3-540-50517-2_85"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"A. Felty and D. Miller. Specifying theorem provers in a higher-order logic programming language. In Proceedings of the Ninth International Conference on Automated Deduction, 1988.","DOI":"10.1007\/BFb0012823"},{"issue":"5","key":"13_CR3","first-page":"45","volume":"2","author":"Y. Futamura","year":"1971","unstructured":"Y. Futamura. Partial evaluation of computation process \u2014 an approach to a compilercompiler. Computer, Systems, Controls, 2(5):45\u201350, 1971.","journal-title":"Computer, Systems, Controls"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"G. Gentzen. Investigations into logical deduction. In M. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68\u2013131, North-Holland Publishing Co., 1969.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"issue":"2","key":"13_CR5","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/0167-6423(87)90031-1","volume":"9","author":"F. Giannotti","year":"1987","unstructured":"F. Giannotti, A. Matteucci, D. Pedreschi, and F. Turini. Symbolic evaluation with structural recursive symbolic constants. Science of Computer Programming, 9(2):161\u2013177, 1987.","journal-title":"Science of Computer Programming"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"13_CR7","unstructured":"J. Hannan and D. Miller. A meta-logic for functional programming. In M. Rogers and H. Abramson, editors, Proceedings of the META88 Workshop, MIT Press, 1989. (to appear)."},{"key":"13_CR8","unstructured":"J. Hannan and D. Miller. Uses of higher-order unification for implementing program transformers. In K. Bowen and R. Kowalski, editors, Fifth International Conference and Symposium on Logic Programming, MIT Press, 1988. Also available as University of Pennsylvania Technical Report MS-CIS-88-46."},{"issue":"2\u20133","key":"13_CR9","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/BF03037137","volume":"6","author":"L. Hasco\u00ebt","year":"1988","unstructured":"L. Hasco\u00ebt. Partial evaluation with inference rules. New Generation Computing, 6(2\u20133):187\u2013209, 1988.","journal-title":"New Generation Computing"},{"key":"13_CR10","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/0304-3975(86)90173-8","volume":"43","author":"J. Heering","year":"1986","unstructured":"J. Heering. Partial evaluation and \u03c9-completeness of algebraic specifications. Theoretical Computer Science, 43:149\u2013167, 1986.","journal-title":"Theoretical Computer Science"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet and B. Lang. Proving and applying program transformations expressed with second-order logic. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"13_CR12","first-page":"22","volume":"247","author":"G. Kahn","year":"1987","unstructured":"G. Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 22\u201339, Springer-Verlag LNCS, Vol. 247, 1987.","journal-title":"LNCS"},{"key":"13_CR13","unstructured":"D. Miller and G. Nadathur. A logic programming approach to manipulating formulas and programs. In Proceedings of the IEEE Fourth Symposium on Logic Programming, IEEE Press, 1987."},{"key":"13_CR14","unstructured":"D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. To appear in the Annals of Pure and Applied Logic."},{"key":"13_CR15","unstructured":"G. Nadathur and D. Miller. An overview of \u03bbProlog. In K. Bowen and R. Kowalski, editors, Fifth International Conference and Symposium on Logic Programming, MIT Press, 1988."},{"issue":"2","key":"13_CR16","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1016\/0167-6423(88)90025-1","volume":"10","author":"H. Nielson","year":"1988","unstructured":"H. Nielson and F. Nielson. Automatic binding time analysis for a typed \u03bb-calculus. Science of Computer Programming, 10(2):139\u2013176, 1988.","journal-title":"Science of Computer Programming"},{"key":"13_CR17","unstructured":"L. Paulson. The foundation of a generic theorem prover. (To appear in the Journal of Automated Reasoning)."},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, 1988.","DOI":"10.1145\/53990.54010"},{"key":"13_CR19","volume-title":"A Structural Approach to Operational Semantics. DAIMI FN-19","author":"G. Plotkin","year":"1981","unstructured":"G. Plotkin. A Structural Approach to Operational Semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark, September 1981."},{"key":"13_CR20","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Uppsala, 1965."},{"key":"13_CR21","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0019-9958(85)80001-2","volume":"65","author":"R. Statman","year":"1985","unstructured":"R. Statman. Logical relations and the typed \u03bb-calculus. Information and Control, 65:85\u201397, 1985.","journal-title":"Information and Control"},{"key":"13_CR22","volume-title":"The Art of Prolog: Advanced Programming Techniques","author":"L. Sterling","year":"1986","unstructured":"L. Sterling and E. Shapiro. The Art of Prolog: Advanced Programming Techniques. MIT Press, Cambridge, MA, 1986."}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51305-1_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:20:56Z","timestamp":1605648056000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51305-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540513056","9783540461913"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-51305-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}