Abstract
We present an approach to compiler implementation using Oliveira and Cook’s structured graphs that avoids the use of explicit jumps in the generated code. The advantage of our method is that it takes the implementation of a compiler using a tree type along with its correctness proof and turns it into a compiler implementation using a graph type along with a correctness proof. The implementation and correctness proof of a compiler using a tree type without explicit jumps is simple, but yields code duplication. Our method provides a convenient way of improving such a compiler without giving up the benefits of simple reasoning.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ager, M.S., Biernacki, D., Danvy, O., Midtgaard, J.: From interpreter to compiler and virtual machine: A functional derivation. Tech. Rep. RS-03-14, BRICS, Department of Computer Science, University of Aarhus (2003)
Bahr, P.: Proving correctness of compilers using structured graphs (extended version). Tech. rep., University of Copenhagen (2014)
Bahr, P., Hutton, G.: Calculating correct compilers (2014) (unpublished manuscript)
Bernardy, J.P., Pouillard, N.: Names for free: polymorphic views of names and binders. In: Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell, pp. 13–24. ACM (2013)
Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 143–156. ACM (2008)
Chlipala, A.: A verified compiler for an impure functional language. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 93–106. ACM (2010)
Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28(6), 2 (2003)
Gill, A., Launchbury, J., Peyton Jones, S.L.: A short cut to deforestation. In: Proceedings of the Conference on Functional Programming Languages and Computer Architecture, pp. 223–232. ACM (1993)
Hutton, G.: Programming in Haskell, vol. 2. Cambridge University Press, Cambridge (2007)
Hutton, G., Wright, J.: Compiling exceptions correctly. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 211–227. Springer, Heidelberg (2004)
Hutton, G., Wright, J.: What is the meaning of these constant interruptions? J. Funct. Program. 17(6), 777–792 (2007)
Johann, P.: A generalization of short-cut fusion and its correctness proof. Higher Order Symbol. Comput. 15(4), 273–300 (2002)
Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42–54. ACM (2006)
Marlow, S.: Haskell 2010 language report (2010)
Matsuda, K., Inaba, K., Nakano, K.: Polynomial-time inverse computation for accumulative functions with multiple data traversals. In: Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, pp. 5–14. ACM (2012)
Meijer, E.: Calculating Compilers. Ph.D. thesis, Katholieke Universiteit Nijmegen (1992)
Oliveira, B.C.D.S., Löh, A.: Abstract syntax graphs for domain specific languages. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, pp. 87–96. ACM (2013)
Oliveira, B.C., Cook, W.R.: Functional programming with structured graphs. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, pp. 77–88. ACM (2012)
Ramsey, N., Dias, J.A., Peyton Jones, S.: Hoopl: a modular, reusable library for dataflow analysis and transformation. In: Proceedings of the Third ACM Haskell Symposium on Haskell, pp. 121–134. ACM (2010)
Ramsey, N., Dias, J.: An applicative control-flow graph based on huet’s zipper. In: Proceedings of the ACM-SIGPLAN Workshop on ML, pp. 105–126 (2006)
Wand, M.: Deriving target code as a representation of continuation semantics. ACM Trans. Program. Lang. Syst. 4(3), 496–517 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bahr, P. (2014). Proving Correctness of Compilers Using Structured Graphs. In: Codish, M., Sumii, E. (eds) Functional and Logic Programming. FLOPS 2014. Lecture Notes in Computer Science, vol 8475. Springer, Cham. https://doi.org/10.1007/978-3-319-07151-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-07151-0_14
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-07150-3
Online ISBN: 978-3-319-07151-0
eBook Packages: Computer ScienceComputer Science (R0)