Abstract
Compiling syntax to native code requires complex code transformations which rearrange the abstract syntax tree. This can be particularly challenging for languages containing binding constructs, and often leads to subtle, hard to find errors. In this paper, we exploit higherorder abstract syntax (HOAS) to implement a type-preserving compiler for the simply-typed lambda-calculus, including transformations such as closure conversion and hoisting, in the dependently-typed language Beluga. Unlike previous implementations, which have to abandon HOAS locally in favor of a first-order binder representation, we are able to take advantage of HOAS throughout the compiler pipeline, so that we do not have to include any lemmas about binder manipulation. Scope and type safety of the code transformations are statically guaranteed, and our implementation directly mirrors the proofs of type preservation. Our work demonstrates that HOAS encodings offer substantial benefits to certified programming.
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
Cave, A., Pientka, B.: Programming with binders and indexed data-types. In: Symposium on Principles of Programming Languages, pp. 413–424. ACM (2012)
Cheney, J., Urban, C.: αProlog: A logic programming language with names, binding and α-equivalence. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 269–283. Springer, Heidelberg (2004)
Chlipala, A.J.: Parametric higher-order abstract syntax for mechanized semantics. In: International Conference on Functional Programming, pp. 143–156. ACM (2008)
Gacek, A.: The Abella interactive theorem prover (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)
Guillemette, L.-J., Monnier, S.: A type-preserving closure conversion in Haskell. In: Workshop on Haskell, pp. 83–92. ACM (2007)
Guillemette, L.-J., Monnier, S.: A type-preserving compiler in Haskell. In: International Conference on Functional Programming, pp. 75–86. ACM (2008)
Hannan, J.: Type systems for closure conversions. In: Workshop on Types for Program Analysis, pp. 48–62 (1995)
Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM 40(1), 143–184 (1993)
Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. Transactions on Computational Logic 9(3), 1–49 (2008)
Pfenning, F.: Elf: A language for logic definition and verified meta-programming. In: Symposium on Logic in Computer Science, pp. 313–322. IEEE (1989)
Pfenning, F., Schürmann, C.: System description: Twelf - A meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (System description). In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 15–21. Springer, Heidelberg (2010)
Poswolsky, A., Schürmann, C.: Practical programming with higher-order encodings and dependent types. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 93–107. Springer, Heidelberg (2008)
Pottier, F.: Static name control for FreshML. In: Symposium on Logic in Computer Science, pp. 356–365. IEEE (July 2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Savary-Belanger, O., Monnier, S., Pientka, B. (2013). Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. In: Gonthier, G., Norrish, M. (eds) Certified Programs and Proofs. CPP 2013. Lecture Notes in Computer Science, vol 8307. Springer, Cham. https://doi.org/10.1007/978-3-319-03545-1_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-03545-1_16
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03544-4
Online ISBN: 978-3-319-03545-1
eBook Packages: Computer ScienceComputer Science (R0)