Abstract
We present an on-going project for the development – in Coq – of a language-agnostic framework for building verified supercompilers. While existing supercompilers are not very big in size, they combine many different program transformations in intricate ways, so checking the correctness of their implementation presents challenges. We propose to define the main supercompilation algorithm in terms of abstract operations, which hide the details of the object language. The verification of the generic supercompiler relies then on properties of these operations, which are easier to establish in isolation, for each specific language. While we still need to try the approach on more supercompilers for specific languages, the framework in its current state appears a promising technique for simplifying the formal verification of supercompilers.
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
Bolingbroke, M., Peyton Jones, S.: Supercompilation by evaluation. In: Proceedings of the Third ACM Haskell Symposium on Haskell, pp. 135–146. ACM (2010)
Glück, R., Klimov, A.V.: Occam’s razor in metacomputation: the notion of a perfect process tree. In: Cousot, P., Filé, G., Falaschi, M., Rauzy, A. (eds.) WSA 1993. LNCS, vol. 724, pp. 112–123. Springer, Heidelberg (1993)
Hamilton, G.: Distillation: extracting the essence of programs. In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61–70. ACM (2007)
Jones, N.D.: The essence of program transformation by partial evaluation and driving. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, pp. 62–79. Springer, Heidelberg (2000)
Jonsson, P.A., Nordlander, J.: Positive supercompilation for a higher order call-by-value language. SIGPLAN Not. 44(1), 277–288 (2009)
Klimov, A.V.: A program specialization relation based on supercompilation and its properties. In: Turchin, V. (ed.) International Workshop on Metacomputation in Russia, META 2008 (2008)
Klyuchnikov, I.: The ideas and methods of supercompilation. Practice of Functional Programming (7) (2011) (in Russian)
Klyuchnikov, I.G., Romanenko, S.A.: MRSC: a toolkit for building multi-result supercompilers. preprint 77, Keldysh Institute (2011)
Klyuchnikov, I., Romanenko, S.: Proving the equivalence of higher-order terms by means of supercompilation. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) PSI 2009. LNCS, vol. 5947, pp. 193–205. Springer, Heidelberg (2010)
Krustev, D.: A simple supercompiler formally verified in Coq. In: Nemytykh, A.P. (ed.) Proceedings of the Second International Workshop on Metacomputation in Russia, META 2010, pp. 102–127 (2010)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2011), http://coq.inria.fr , version 8.3pl3
Mendel-Gleason, G.: Types and verification for infinite state systems. PhD thesis, Dublin City University, Dublin, Ireland (2011)
Mitchell, N., Runciman, C.: A supercompiler for core Haskell. In: Chitil, O., Horváth, Z., Zsók, V. (eds.) IFL 2007. LNCS, vol. 5083, pp. 147–164. Springer, Heidelberg (2008)
Reich, J.S., Naylor, M., Runciman, C.: Supercompilation and the Reduceron. In: Nemytykh, A.P. (ed.) Proceedings of the Second International Workshop on Metacomputation in Russia, META 2010, pp. 159–172 (2010)
Sands, D.: Proving the correctness of recursion-based automatic program transformations. Theor. Comput. Sci. 167(1-2), 193–233 (1996)
Sørensen, M.H.: Convergence of program transformers in the metric space of trees. In: Jeuring, J. (ed.) MPC 1998. LNCS, vol. 1422, pp. 315–337. Springer, Heidelberg (1998)
Sørensen, M.H., Glück, R.: Introduction to supercompilation. In: Hatcliff, J., Thiemann, P. (eds.) DIKU 1998. LNCS, vol. 1706, pp. 246–270. Springer, Heidelberg (1999)
Turchin, V.: The concept of a supercompiler. ACM Transactions on Programming Languages and Systems 8(3), 292–325 (1986)
Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full: Adventures in constructive termination. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 250–265. Springer, Heidelberg (2012)
Wadler, P.: Deforestation: Transforming programs to eliminate trees. Theor. Comput. Sci. 73(2), 231–248 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krustev, D.N. (2013). Towards a Framework for Building Formally Verified Supercompilers in Coq. In: Loidl, HW., Peña, R. (eds) Trends in Functional Programming. TFP 2012. Lecture Notes in Computer Science, vol 7829. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40447-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-40447-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40446-7
Online ISBN: 978-3-642-40447-4
eBook Packages: Computer ScienceComputer Science (R0)