{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:22:03Z","timestamp":1725456123453},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603597"},{"type":"electronic","value":"9783540450481"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0026826","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T05:29:45Z","timestamp":1132378185000},"page":"279-298","source":"Crossref","is-referenced-by-count":6,"title":["Mechanically verifying the correctness of an offline partial evaluator"],"prefix":"10.1007","author":[{"given":"John","family":"Hatcliff","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,16]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Yves Bertot and Ranan Fraer. Reasoning with executable specifications. In TAP-SOFT'95 [27], pages 531\u2013545.","key":"18_CR1","DOI":"10.1007\/3-540-59293-8_218"},{"doi-asserted-by":"crossref","unstructured":"Sandrine Blazy and Philippe Facon. Formal specification and prototyping of a program specializer. In TAPSOFT'95 [27], pages 666\u2013680.","key":"18_CR2","DOI":"10.1007\/3-540-59293-8_227"},{"key":"18_CR3","first-page":"493","volume-title":"Tutorial notes on partial evaluation","author":"C. Consel","year":"1993","unstructured":"Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 493\u2013501, Charleston, South Carolina, January 1993. ACM Press."},{"doi-asserted-by":"crossref","unstructured":"Rowan Davies and Frank Pfenning. A modal analysis of staged compuation. In Proceedings of the Workshop on Types for Program Analysis, Aarhus, Denmark, 1995.","key":"18_CR4","DOI":"10.21236\/ADA296537"},{"key":"18_CR5","first-page":"193","volume-title":"Proof of translation in natural semantics","author":"J. Despeyroux","year":"1986","unstructured":"J\u00f6elle Despeyroux. Proof of translation in natural semantics. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science, pages 193\u2013205, Cambridge, Massachusetts, 1986. IEEE Computer Society Press."},{"unstructured":"Robert Gl\u00fcck and Jesper J\u00f8rgensen. Efficient multi-level generating extensions. 1995. To appear in The Proceedings of the Seventh International Symposium on Programming Languages, Implementations, Logics and Programs. Utrecht, The Netherlands, September 20\u201322, 1995.","key":"18_CR6"},{"issue":"1","key":"18_CR7","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1017\/S0956796800000058","volume":"1","author":"C. K. Gomard","year":"1991","unstructured":"Carsten K. Gomard and Neil Jones. A partial evaluator for the untyped lambdacalculus. Journal of Functional Programming, 1(1):21\u201369, 1991.","journal-title":"Journal of Functional Programming"},{"unstructured":"Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.","key":"18_CR8"},{"issue":"2","key":"18_CR9","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1017\/S0956796800000666","volume":"3","author":"J. Hannan","year":"1993","unstructured":"John Hannan. Extended natural semantics. Journal of Functional Programming, 3(2):123\u2013152, 1993.","journal-title":"Journal of Functional Programming"},{"doi-asserted-by":"crossref","unstructured":"John Hannan and Dale Miller. Deriving mixed evaluation from standard evaluation for a simple functional language. In J. van de Snepscheut, editor, Mathematics of Program Construction, number 375 in Lecture Notes in Computer Science, pages 239\u2013255, 1989.","key":"18_CR10","DOI":"10.1007\/3-540-51305-1_13"},{"doi-asserted-by":"crossref","unstructured":"John Hannan and Frank Pfenning. Compiler verification in LF. In Proceedings of the Seventh Symposium on Logic in Computer Science, pages 407\u2013418. IEEE, 1992.","key":"18_CR11","DOI":"10.1109\/LICS.1992.185552"},{"issue":"1","key":"18_CR12","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, 1993. A preliminary version appeared in the proceedings of the First IEEE Symposium on Logic in Computer Science, pages 194\u2013204, June 1987.","journal-title":"Journal of the ACM"},{"key":"18_CR13","volume-title":"DIKU Report 95\/14","author":"J. Hatcliff","year":"1995","unstructured":"John Hatcliff. Mechanically verifying the correctness of an offline partial evaluator (extended version). DIKU Report 95\/14, University of Copenhagen, Copenhagen, Denmark, 1995."},{"key":"18_CR14","volume-title":"DIKU Report 95\/15","author":"J. Hatcliff","year":"1995","unstructured":"John Hatcliff and Olivier Danvy. A computational formalization for partial evaluation. DIKU Report 95\/15, University of Copenhagen, Copenhagen, Denmark, 1995. Presented at the Workshop on Logic, Domains, and Programming Languages. Darmstadt, Germany. May, 1995."},{"unstructured":"Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, 1993.","key":"18_CR15"},{"key":"18_CR16","volume-title":"Technical Report CS-95-178","author":"J. L. Lawall","year":"1995","unstructured":"Julia L. Lawall and Olivier Danvy. Continuation-based partial evaluation. Technical Report CS-95-178, Computer Science Department, Brandeis University, Waltham, Massachusetts, January 1995. An earlier version appeared in the proceedings of the 1994 ACM Conference on Lisp and Functional Programming."},{"key":"18_CR17","volume-title":"Report MPI-I-91-211","author":"S. Michaylov","year":"1991","unstructured":"Spiro Michaylov and Frank Pfenning. Natural semantics and some of its metatheory in Elf. Report MPI-I-91-211, Max-Planck-Institute for Computer Science, Saarbr\u00fccken, Germany, August 1991."},{"key":"18_CR18","series-title":"Research Report 909","first-page":"116","volume-title":"ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation","author":"T. Mogensen","year":"1992","unstructured":"T. Mogensen. Self-applicable partial evaluation for the pure lambda calculus. In Charles Consel, editor, ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, Research Report 909, Department of Computer Science, Yale University, pages 116\u2013121, San Francisco, California, June 1992."},{"issue":"3","key":"18_CR19","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1017\/S0956796800000770","volume":"3","author":"J. Palsberg","year":"1993","unstructured":"Jens Palsberg. Correctness of binding-time analysis. Journal of Functional Programming, 3(3):347\u2013363, 1993.","journal-title":"Journal of Functional Programming"},{"doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Logic programming in the LF logical framework. In G\u00e9rard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149\u2013181. Cambridge University Press, 1991.","key":"18_CR20","DOI":"10.1017\/CBO9780511569807.008"},{"key":"18_CR21","volume-title":"Technical Report CMU-CS-92-186","author":"F. Pfenning","year":"1992","unstructured":"Frank Pfenning. A proof of the church-rosser theorem and its representation in a logical framework. Technical Report CMU-CS-92-186, Carnegie Mellon University, Pittsburgh, Pennsylvania, September 1992. To appear in Journal of Automated Reasoning."},{"doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SLGPLAN'88 Conference on Programming Languages Design and Implementation, pages 199\u2013208, June 1988.","key":"18_CR22","DOI":"10.1145\/53990.54010"},{"key":"18_CR23","first-page":"537","volume-title":"number 607 in Lecture Notes in Artificial Intelligence","author":"F. Pfenning","year":"1992","unstructured":"Frank Pfenning and Ekkehard Rohwedder. Implementing the meta-theory of deductive systems. In D. Kapur, editor, Proceedings of the 11th Eleventh International Conference on Automated Deduction, number 607 in Lecture Notes in Artificial Intelligence, pages 537\u2013551, Saratoga Springs, New York, 1992. Springer-Verlag."},{"key":"18_CR24","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"Dag Prawitz. Natural Deduction. Almquist and Wiksell, Uppsala, 1965."},{"key":"18_CR25","first-page":"221","volume-title":"Total correctness by local improvement in program transformation","author":"D. Sands","year":"1995","unstructured":"David Sands. Total correctness by local improvement in program transformation. In Ron Cytron, editor, Proceedings of the Twenty-first Annual ACM Symposium on Principles of Programming Languages, pages 221\u2013232, San Francisco, California, January 1995. ACM Press."},{"doi-asserted-by":"crossref","unstructured":"Morten Heine S\u00f8rensen, Robert Gl\u00fcck, and Neil Jones. Towards unifying partial evaluation, deforestation, supercompilation, and GPC. In Proceedings of the Fifth European Symposium on Programming, pages 485\u2013500, Edinburgh, U.K., April 1994.","key":"18_CR26","DOI":"10.1007\/3-540-57880-3_32"},{"unstructured":"TAPSOFT '95: Theory and Practice of Software Development, number 915 in Lecture Notes in Computer Science, Aarhus, Denmark, May 1995.","key":"18_CR27"},{"issue":"3","key":"18_CR28","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1017\/S0956796800000782","volume":"3","author":"M. Wand","year":"1993","unstructured":"Mitchell Wand. Specifying the correctness of binding-time analysis. Journal of Functional Programming, 3(3):365\u2013387, 1993.","journal-title":"Journal of Functional Programming"}],"container-title":["Lecture Notes in Computer Science","Programming Languages: Implementations, Logics and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0026826","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T21:53:47Z","timestamp":1586555627000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0026826"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603597","9783540450481"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/bfb0026826","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}