Hostname: page-component-8448b6f56d-qsmjn Total loading time: 0 Render date: 2024-04-18T23:29:29.241Z Has data issue: false hasContentIssue false
  • English
  • Français

Calculating correct compilers

Part of: JFP Research Articles

Published online by Cambridge University Press:  16 September 2015

PATRICK BAHR  and
GRAHAM HUTTON
PATRICK BAHR
Affiliation:
Department of Computer Science, University of Copenhagen, Denmark (e-mail: paba@diku.dk)
GRAHAM HUTTON
Affiliation:
School of Computer Science, University of Nottingham, UK (e-mail: graham.hutton@nottingham.ac.uk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

In this article, we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high-level semantics by systematic calculation, with all details of the implementation of the compilers falling naturally out of the calculation process. Our approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic expressions, exceptions, state, various forms of lambda calculi, bounded and unbounded loops, non-determinism and interrupts. All the calculations in the article have been formalised using the Coq proof assistant, which serves as a convenient interactive tool for developing and verifying the calculations.

Type
Articles
Information
Journal of Functional Programming , Volume 25 , 2015 , e14
Copyright
Copyright © Cambridge University Press 2015 

References

Adams, N., Kranz, D., Kelsey, R., Rees, J., Hudak, P. & Philbin, J. (1986) ORBIT: An optimizing compiler for scheme. In Proceedings of the 1986 SIGPLAN Symposium on Compiler Construction. New York, NY, USA: ACM, pp. 219–233.CrossRefGoogle Scholar
Ager, M. S., Biernacki, D., Danvy, O. & Midtgaard, J. (2003a) A functional correspondence between evaluators and abstract machines. In Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. New York, NY, USA: ACM, pp. 8–19.CrossRefGoogle Scholar
Ager, M. S., Biernacki, D., Danvy, O. & Midtgaard, J. (2003b) From Interpreter to Compiler and Virtual Machine: A Functional Derivation. Technical Report RS-03-14. BRICS, Department of Computer Science, Aarhus, Denmark: University of Aarhus.CrossRefGoogle Scholar
Appel, A. (1991) Compiling with Continuations. New York, NY, USA: Cambridge University Press.CrossRefGoogle Scholar
Backhouse, R. (2003) Program Construction: Calculating Implementations from Specifications. West Sussex, UK: John Wiley and Sons, Inc.Google Scholar
Bahr, P. (2014) Proving correctness of compilers using structured graphs. Functional and Logic Programming, Lecture Notes in Computer Science, vol. 8475. Springer International Publishing, pp. 221–237.CrossRefGoogle Scholar
Chase, D. (1994a) Implementation of exception handling, Part I. J. C Lang. Transl. 5 (4), 229–240.Google Scholar
Chase, D. (1994b) Implementation of exception handling, Part II. J. C Lang. Transl. 6 (1), 20–32.Google Scholar
Day, L. E. & Hutton, G. (2014) Compilation à la Carte. In Proceedings of the 25th Symposium on Implementation and Application of Functional Languages. New York, NY, USA: ACM, pp. 13–24.Google Scholar
Dybjer, P. (1994) Inductive families. Formal Asp. Comput. 6 (4), 440–465.CrossRefGoogle Scholar
Hutton, G. (2007) Programming in Haskell. New York, NY, USA: Cambridge University Press.CrossRefGoogle Scholar
Hutton, G. & Wright, J. (2004) Compiling exceptions correctly. Mathematics of Program Construction, Lecture Notes in Computer Science, vol. 3125. Berlin/Heidelberg: Springer, pp. 211–227.CrossRefGoogle Scholar
Hutton, G. & Wright, J. (2007) What is the meaning of these constant interruptions? J. Funct. Program. 17 (06), 777–792.CrossRefGoogle Scholar
Letouzey, P. (2008) Extraction in Coq: An overview. Logic and Theory of Algorithms: 4th Conference on Computability in Europe, Lecture Notes in Computer Science, vol. 5028. Berlin, Germany: Springer-Verlag.Google Scholar
McCarthy, J. & Painter, J. (1967) Correctness of a compiler for arithmetic expressions. Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, vol. 19. American Mathematical Society, Providence, RI, USA: pp. 33–41.CrossRefGoogle Scholar
McKinna, J. & Wright, J. (2006) A Type-Correct, Stack-Safe, Provably Correct Expression Compiler in Epigram. Unpublished manuscript.Google Scholar
Meijer, E. (1992) Calculating Compilers. Ph.D. thesis, Katholieke Universiteit Nijmegen.Google Scholar
Reynolds, J. C. (1972) Definitional interpreters for higher-order programming languages. In Proceedings of the ACM Annual Conference. New York, NY, USA: ACM, pp. 717–740.CrossRefGoogle Scholar
Sculthorpe, N., Farmer, A. & Gill, A. (2013) The HERMIT in the tree: Mechanizing program transformations in the GHC Core language. Implementation and Application of Functional Languages 2012, Lecture Notes in Computer Science, vol. 8241. New York, NY, USA: Springer.CrossRefGoogle Scholar
Sestoft, P. (1997) Deriving a lazy abstract machine. J. Funct. Program. 7 (03), 231–264.CrossRefGoogle Scholar
Spivey, M. (1990) A functional theory of exceptions. Sci. Comput. Program. 14 (1), 25–42.CrossRefGoogle Scholar
Steele, G. L. Jr., (1978) Rabbit: A Compiler for Scheme. Technical Report AI-TR-474. Cambridge, MA, USA: MIT AI Lab.Google Scholar
Thielecke, H. (2002) Comparing control constructs by double-barrelled CPS. Higher-Order Symb. Comput. 15 (2–3), 141–160.CrossRefGoogle Scholar
Wadler, P. (1989) Theorems for free! In Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture. New York, NY, USA: ACM Press.CrossRefGoogle Scholar
Wand, M. (1982a) Deriving target code as a representation of continuation semantics. ACM Trans. Program. Lang. Syst. 4 (3), 496–517.CrossRefGoogle Scholar
Wand, M. (1982b) Semantics-directed machine architecture. In Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, pp. 234–241.CrossRefGoogle Scholar
Winskel, G. (1993) The Formal Semantics of Programming Languages – An Introduction, Foundation of Computing Series. Cambridge, MA, USA: MIT Press.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.