Abstract
Type theory and constructive logics allow us, from a proof of a formula, to extract a program that satisfies the specification expressed by this formula. Normally, programs extracted in this way are inefficient. Optimization algorithms for these programs have been developed. In this paper we show an algorithm to optimize programs represented by second order typed λ-terms. We prove also that the simplified programs are observational equivalent to the original ones.
Chapter PDF
Similar content being viewed by others
Bibliography
M. Beeson, Foundations of Constructive Mathematics, Berlin, Springer-Verlag, 1985
S. Berardi, Extensional Equality for Simply Typed λ-calculi, Technical Report, Turin University, 1993.
S. Berardi, A canonical Projection between Simply Typed λ-calculi, Technical Report, Turin University, 1993.
S. Berardi, Pruning Simply Typed λ-terms, Technical Report, Turin University, 1993.
R. L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986.
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Pauling-Mohring, B. Werner, The Coq Proof Assistant-User's Guide, INRIA — Rocquencourt, 1983.
J.-Y. Girard, Interpretation Fonctionelle et Elimination des Coupures de l'Arithmetique d'Ordre Superieur, These de Doctorat d'Etat, Soutenue le 26 Juin 1972.
W.A. Howard, The Formulae-as-Types notion of Construction, in ‘Essays on Combinatory Logic, Lambda Calculus and Formlism', Eds J. P. Seldin and j. R. Hindley, Accademic Press, 1980.
C. Paulin-Mohring, Extracting F ω 's Programs from Proofs in the Calculus of Constructions, In: Association for Computing Machinery, editor, Sixteenth Annual ACM Symposium on Priciples of Programming Languages, 1989.
Y. Takayama, Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs, Journal of Symbolic Computation, 1991, 12, 29–69
A. S. Troelstra, Mathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, 344, Springer-Verlag, 1973
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boerio, L. (1994). Extending pruning techniques to polymorphic second order λ-calculus. In: Sannella, D. (eds) Programming Languages and Systems — ESOP '94. ESOP 1994. Lecture Notes in Computer Science, vol 788. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57880-3_8
Download citation
DOI: https://doi.org/10.1007/3-540-57880-3_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57880-2
Online ISBN: 978-3-540-48376-2
eBook Packages: Springer Book Archive