{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:11Z","timestamp":1725663851198},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_42","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:22:43Z","timestamp":1330269763000},"page":"575-589","source":"Crossref","is-referenced-by-count":5,"title":["Representing proof transformations for program optimization"],"prefix":"10.1007","author":[{"given":"Penny","family":"Anderson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"42_CR1","unstructured":"Penny Anderson. Program Derivation by Proof Transformation. PhD thesis, Department of Computer Science, Carnegie Mellon University, October 1993. Available as Technical Report CMU-CS-93-206."},{"key":"42_CR2","doi-asserted-by":"crossref","unstructured":"Penny Anderson. Program extraction in a logical framework setting. In Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, July 1994. To appear.","DOI":"10.1007\/3-540-58216-9_35"},{"issue":"2","key":"42_CR3","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H. Barendregt","year":"1991","unstructured":"Henk Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125\u2013154, April 1991.","journal-title":"Journal of Functional Programming"},{"issue":"4","key":"42_CR4","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1145\/1780.1781","volume":"6","author":"R. S. Bird","year":"1984","unstructured":"R.S. Bird. The promotion and accumulation strategies in transformational programming. ACM Transactions on Programming Languages and Systems, 6(4):487\u2013504, October 1984.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"42_CR5","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"R. M. Burstall","year":"1977","unstructured":"R. M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the Association for Computing Machinery, 24(1):44\u201367, January 1977.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"42_CR6","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Robert L. L. Constable","year":"1986","unstructured":"Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"42_CR7","volume-title":"Rapport Technique 134","author":"G. Dowek","year":"1991","unstructured":"Gilles Dowek, Amy Felty, Hugo Herbelin, G\u00e9rard Huet, Christine Paulin-Mohring, and Benjamin Werner. The Coq proof assistant user's guide. Rapport Technique 134, INRIA, Rocquencourt, France, December 1991. Version 5.6."},{"key":"42_CR8","unstructured":"Amy Felty. Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, July 1989. Available as Technical Report MS-CIS-89-53."},{"key":"42_CR9","doi-asserted-by":"crossref","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:43\u201381, 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"42_CR10","unstructured":"Christopher A. Goad. Computational uses of the manipulation of formal proofs. Technical Report Stan-CS-80-819, Stanford University, August 1980."},{"key":"42_CR11","doi-asserted-by":"crossref","unstructured":"David Gries. The Science of Programming. Springer-Verlag, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"42_CR12","unstructured":"John Hannan. Investigating a Proof-Theoretic Meta-Language for Functional Programs. PhD thesis, University of Pennsylvania, January 1991. Available as MS-CIS-91-09."},{"key":"42_CR13","unstructured":"John Hannan and Dale Miller. A meta-logic for functional programming. In H. Abramson and M. Rogers, editors, Meta-Programming in Logic Programming, pages 453\u2013476. MIT Press, 1989."},{"issue":"1","key":"42_CR14","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 Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"42_CR15","unstructured":"Susumu Hayashi. An introduction to PX. In Gerard Huet, editor, Logical Foundations of Functional Programming. Addison-Wesley, 1990."},{"key":"42_CR16","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G\u00e9rard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"42_CR17","doi-asserted-by":"crossref","unstructured":"Peter Madden. Automated Program Transformation Through Proof Transformation. PhD thesis, University of Edinburgh, 1991.","DOI":"10.1007\/3-540-55602-8_183"},{"key":"42_CR18","first-page":"446","volume-title":"LNAI 607","author":"P. Madden","year":"1992","unstructured":"Peter Madden. Automatic program optimization through proof transformation. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 446\u2013460, Saratoga Springs, New York, June 1992. Springer-Verlag LNAI 607."},{"key":"42_CR19","first-page":"299","volume-title":"LNAI 596","author":"S. Michaylov","year":"1991","unstructured":"Spiro Michaylov and Frank Pfenning. Natural semantics and some of its metatheory in Elf. In L.-H. Eriksson, L. Halln\u00e4s, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 299\u2013344, Stockholm, Sweden, January 1991. Springer-Verlag LNAI 596."},{"key":"42_CR20","doi-asserted-by":"crossref","unstructured":"Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Peter Schroeder-Heister, editor, Extensions of Logic Programming: International Workshop, T\u00fcbingen FRG, December 1989, pages 253\u2013281. Springer-Verlag LNCS 475, 1991.","DOI":"10.1007\/BFb0038698"},{"key":"42_CR21","unstructured":"Dale Miller. Unification of simply typed lambda-terms as logic programming. In K. Furukawa, editor, Proceedings of the Eighth International Conference on Logic Programming, pages 255\u2013269. MIT Press, July 1991."},{"key":"42_CR22","volume-title":"The Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990."},{"key":"42_CR23","unstructured":"Robert Paige and Shaye Koening. Finite differencing of computable expressions. Technical Report LCSR-TR-8, Laboratory for Computer Science Research, Rutgers University, August 1980."},{"key":"42_CR24","doi-asserted-by":"crossref","unstructured":"Christine Paulin-Mohring. Extracting 589-01 programs from proofs in the calculus of constructions. In Sixteenth Annual Symposium on Principles of Programming Languages, pages 89\u2013104. ACM Press, January 1989.","DOI":"10.1145\/75277.75285"},{"key":"42_CR25","unstructured":"Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 199? To appear. Preliminary version available as Technical Report CMU-CS-92-105, School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, January 1992."},{"key":"42_CR26","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1090\/conm\/106\/1057826","volume":"106","author":"F. Pfenning","year":"1990","unstructured":"Frank Pfenning. Program development through proof transformation. Contemporary Mathematics, 106:251\u2013262, 1990.","journal-title":"Contemporary Mathematics"},{"key":"42_CR27","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.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"42_CR28","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74\u201385, Amsterdam, The Netherlands, July 1991.","DOI":"10.1109\/LICS.1991.151632"},{"key":"42_CR29","first-page":"537","volume-title":"LNAI 607","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 International Conference on Automated Deduction, pages 537\u2013551, Saratoga Springs, New York, June 1992. Springer-Verlag LNAI 607."},{"key":"42_CR30","unstructured":"James T. Sasaki. Extracting Efficient Code from Constructive Proofs. PhD thesis, Cornell University, May 1986. Available as Technical Report TR 86-757."},{"key":"42_CR31","unstructured":"Helmut Schwichtenberg. On Martin-L\u00f6f's theory of types. In Atti Degli Incontri di Logica Mathematica, pages 299\u2013325. Dipartimento di Matematica, Universit\u00e0 di Siena, 1982."},{"key":"42_CR32","first-page":"95","volume-title":"A normal form for natural deductions in a type theory with realizing terms","author":"H. Schwichtenberg","year":"1985","unstructured":"Helmut Schwichtenberg. A normal form for natural deductions in a type theory with realizing terms. In Ettore Casari et al., editors, Atti del Congresso Logica e Filosfia della Scienza, oggi. San Gimignano, December 7\u201311, 1983, pages 95\u2013138, Bologna, Italy, 1985. CLUEB."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:40Z","timestamp":1605647860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}