Abstract
A ”linear — style” sequent calculus makes it possible to explore the close structural relationships between primitive recursive programs and their inductive termination proofs, and between program transformations and their corresponding proof transformations. In this context the recursive — to — tail — recursive transformation corresponds proof theoretically to a certain kind of cut elimination, called here ”call by value cut elimination”.
The second author thanks the Department of Philosophy at Carnegie Mellon University for generous hospitality during a sabbatical year as a Fulbright Scholar 1992–93.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Anderson, Program Derivation by Proof Transformation, Carnegie Mellon Technical Report CS-93–206, 1993.
L. Colson, About Primitive Recursive Algorithms, in Proceedings ICALP '89, Springer Lecture Notes in Computer Science 372, 194–206.
M.V. Fairtlough and S.S. Wainer, Ordinal Complexity of Recursive Definitions, Information and Computation Vol. 99, 1992, 123–153.
S. Feferman, Logics for Termination and Correctness of Functional Programs II, Logics of Strength PRA, in ”Proof Theory”, Eds. P.Aczel, H. Simmons, S. Wainer; Cambridge 1992, 195–225.
J.Y. Girard, Linear Logic, Theor. Comp. Science Vol.50, 1987, 1–102.
C. Goad, Computational Uses of the Manipulation of Formal Proofs, Stanford Technical Report CS-80–819, 1980.
P. Madden, Automatic Program Optimization through Proof Transformation, Proc. 11th. Intl. Conf. on Automatic Deduction, Ed. D. Kapur, Springer-Verlag LNAI 607, 1992, 446–460.
R. Péter, Recursive Functions, Academic Press 1967.
F. Pfenning, Program Development through Proof Transformation, AMS Contemporary Mathematics Vol.106, 1990, 251–262.
H. Schwichtenberg, Proofs as Programs, in ”Proof Theory”, Eds. P.Aczel, H. Simmons, S. Wainer; Cambridge 1992, 79–113.
W. Sieg, Herbrand Analyses, Archive Math Logic Vol.30, 1991, 409–441.
S.S. Wainer, Four Lectures on Primitive Recursion, in ”Logic and Algebra of Specification”, Eds. F. Bauer, W. Brauer, H. Schwichtenberg; Springer-Verlag ASI Series F Vol. 94, 1993, 377–410.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sieg, W., Wainer, S.S. (1994). Program transformation and proof transformation. In: Börger, E., Gurevich, Y., Meinke, K. (eds) Computer Science Logic. CSL 1993. Lecture Notes in Computer Science, vol 832. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0049339
Download citation
DOI: https://doi.org/10.1007/BFb0049339
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58277-9
Online ISBN: 978-3-540-48599-5
eBook Packages: Springer Book Archive