Abstract
Within a framework of correct code-generation from HOL-specifications, we present a particular instance concerned with the optimized compilation of a lazy language (called MiniHaskell) to a strict language (called MiniML).
Both languages are defined as shallow embeddings into denotational semantics based on Scott’s cpo’s, leading to a derivation of the corresponding operational semantics in order to cross-check the basic definitions.
On this basis, translation rules from one language to the other were formally derived in Isabelle/HOL. Particular emphasis is put on the optimized compilation of function applications leading to the side-calculi inferring e.g. strictness of functions.
The derived rules were grouped and set-up as an instance of our generic, tactic-based translator for specifications to code.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in HOL. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds.) Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP Transactions, vol. A-10, Nijmegen, The Netherlands, pp. 129–156. North-Holland/Elsevier, Amsterdam (1992)
Danvy, O., Filinski, A.: Representing control: a study of the CPS transformation. Mathematical Structures in Computer Science 2(4), 361–391 (1992)
Glesner, S.: Using program checking to ensure the correctness of compiler implementations. JUCS 9(3) (2003)
Klein, G., Nipkow, T.: A machine-checked model for a java-like language, virtual machine and compiler. Technical report, TUM (March 2003)
Meyer, T., Wolff, B.: Correct code-generation in a generic framework. In: Aargaard, M., Harrison, J., Schubert, T. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 213–230. Springer, Heidelberg (2000)
Milner, R., Tofte, M., Harper, R. (eds.): The Definition of Standard ML (revised). MIT Press, Cambridge (1997)
Müller, O., Nipkow, T., Oheimb, D.v., Slotosch, O.: HOLCF = HOL + LCF. Journal of Functional Programming 9, 191–223 (1999)
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10, 171–186 (1998)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Tej, H., Wolff, B.: A corrected failure-divergence model for csp in isabelle/hol. In: Fitzgerald, J., Jones, C., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 318–337. Springer, Heidelberg (1997)
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press, Cambridge (1993)
Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: A methodology for the translation validation of optimizingcompilers. JUCS 9(3) (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, T., Wolff, B. (2006). Tactic-Based Optimized Compilation of Functional Programs. In: Filliâtre, JC., Paulin-Mohring, C., Werner, B. (eds) Types for Proofs and Programs. TYPES 2004. Lecture Notes in Computer Science, vol 3839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11617990_13
Download citation
DOI: https://doi.org/10.1007/11617990_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31428-8
Online ISBN: 978-3-540-31429-5
eBook Packages: Computer ScienceComputer Science (R0)