Document Open Access Logo

Modelling Homogeneous Generative Meta-Programming

Authors Martin Berger, Laurence Tratt, Christian Urban

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.5.pdf
  • Filesize: 0.53 MB
  • 23 pages

Document Identifiers

Author Details

Martin Berger
Laurence Tratt
Christian Urban

Cite AsGet BibTex

Martin Berger, Laurence Tratt, and Christian Urban. Modelling Homogeneous Generative Meta-Programming. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.ECOOP.2017.5

Abstract

Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present a foundational calculus which can model both compile-time and run-time evaluated HGMP, allowing us to model, for the first time, languages such as Template Haskell. The calculus is designed such that it can be gradually enhanced with the features needed to model many of the advanced features of real languages. We demonstrate this by showing how a simple, staged type system as found in Template Haskell can be added to the calculus.
Keywords
  • Formal Methods
  • Meta-Programming
  • Operational Semantics
  • Types
  • Quasi-Quotes
  • Abstract Syntax Trees

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Michael D. Adams. Towards the essence of hygiene. In Proc. POPL, 2015. Google Scholar
  2. Martin Berger and Laurence Tratt. Program Logics for Homogeneous Metaprogramming. In Proc. LPAR, pages 64-81, 2010. Google Scholar
  3. Ana Bove and Laura Arbilla. A confluent calculus of macro expansion and evaluation. In Proc. LFP, pages 278-287, 1992. Google Scholar
  4. Gilad Bracha and David Ungar. Mirrors: design principles for meta-level facilities of object-oriented programming languages. In Proc. OOPSLA, pages 331-344, 2004. Google Scholar
  5. Cristiano Calcagno, Walid Taha, Liwen Huang, and Xavier Leroy. Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection. In Proc. GPCE, pages 57-76, 2003. Google Scholar
  6. Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta. Static Analysis of Multi-staged Programs via Unstaging Translation. In Proc. POPL, pages 81-92, 2011. Google Scholar
  7. William Clinger and Jonathan Rees. Macros that work. In Proc. POPL, pages 155-162, 1991. Google Scholar
  8. Krzysztof Czarnecki, John O'Donnell, Jörg Striegnitz, and Walid Taha. DSL Implementation in MetaOCaml, Template Haskell, and C++. In Proc. Dagstuhl Workshop on Domain-specific Program Generation, volume 3016, pages 50-71, 2004. Google Scholar
  9. Rowan Davies. A temporal-logic approach to binding-time analysis. In Proc. LICS, pages 184-195, 1996. Google Scholar
  10. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555-604, 2001. Google Scholar
  11. William M. Farmer. The formalization of syntax-based mathematical algorithms using quotation and evaluation. In J. Carette, editor, Intelligent Computer Mathematics, pages 35-50, 2013. Google Scholar
  12. William M. Farmer and Pouya Larjani. Frameworks for reasoning about syntax that utilize quotation and evaluation. McSCert Report 9, McMaster University, 2013. Available at URL: http://imps.mcmaster.ca/doc/syntax.pdf.
  13. Matthew Flatt, Ryan Culpepper, David Darais, and Robert Bruce Findler. Macros that work together: Compile-time bindings, partial expansion, and definition contexts. JFP, 22(2):181-216, March 2012. Google Scholar
  14. Fabien Fleutot and Laurence Tratt. Contrasting compile-time meta-programming in Metalua and Converge. In Workshop on Dynamic Languages and Applications, July 2007. Google Scholar
  15. Murdoch J. Gabbay and Dominic P. Mulligan. http://www.gabbay.org.uk/papers/twollc.pdf. In Proc. WFLP, volume 246, pages 107-129, 2009.
  16. Steven E. Ganz, Amr Sabry, and Walid Taha. Macros as multi-stage computations: Type-safe, generative, binding macros in MacroML. In Proc. ICFP, pages 74-85, 2001. Google Scholar
  17. Ronald Garcia and Andrew Lumsdaine. Toward Foundations for Type-Reflective Metaprogramming. SIGPLAN Not., 45(2):25-34, October 2009. Google Scholar
  18. Jim Grundy, Tom Melham, and John O'Leary. A reflective functional language for hardware design and theorem proving. JFP, 16(2):157-196, 2006. Google Scholar
  19. John Harrison. Metatheory and Reflection in Theorem Proving: A Survey and Critique. Technical Report CRC-053, SRI International, 1995. Google Scholar
  20. David Herman and Mitchell Wand. A theory of hygienic macros. In Proc. ESOP, pages 48-62, March 2008. Google Scholar
  21. Jun Inoue, Oleg Kiselyov, and Yukiyoshi Kameyama. Staging beyond terms: Prospects and challenges. In Proc. PEPM, PEPM '16, pages 103-108, 2016. Google Scholar
  22. Jun Inoue and Walid Taha. Reasoning about multi-stage programs. In Proc. ESOP, pages 357-376, 2012. Google Scholar
  23. Ulrik Jørring and William L. Scherlis. Compilers and staging transformations. In Proc. POPL, pages 86-96. ACM, 1986. Google Scholar
  24. Yukiyoshi Kameyama, Oleg Kiselyov, and Chung-chieh Shan. Closing the stage: From staged code to typed closures. In Proc. PEPM, pages 147-157, 2008. Google Scholar
  25. L. Gregory Meredith and Matthias Radestock. A Reflective Higher-order Calculus. ENTCS, 141(5):49-67, 2005. Google Scholar
  26. Robert Muller. M-LISP: A representation-independent dialect of LISP with reduction semantics. TOPLAS, 14(4):589-616, October 1992. Google Scholar
  27. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Transactions on Computational Logic, 2007. Google Scholar
  28. Simon Peyton Jones. New directions for Template Haskell. http://ghc.haskell.org/trac/ghc/blog/Template%20Haskell%20Proposal, October 2010.
  29. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  30. Jon Rafkind and Matthew Flatt. Honu: Syntactic extension for algebraic notation through enforestation. In GPCE, pages 122-131, 2012. Google Scholar
  31. Tiark Rompf and Martin Odersky. Lightweight modular staging: a pragmatic approach to runtime code generation and compiled dsls. Commun. ACM, 55(6):121-130, 2012. Google Scholar
  32. Tim Sheard. Accomplishments and research challenges in meta-programming. Proc. SAIG '01, 2196:2-44, September 2003. Google Scholar
  33. Tim Sheard and Simon Peyton Jones. Template meta-programming for Haskell. In Proc. Haskell workshop, pages 1-16, 2002. Google Scholar
  34. Aaron Stump. Directly reflective meta-programming. Higher Order Symbol. Comput., 22(2):115-144, June 2009. Google Scholar
  35. Walid Taha. Multi-Stage Programming: Its Theory and Applications. PhD thesis, Oregon Graduate Institute of Science and Technology, 1993. Google Scholar
  36. Walid Taha and Michael Florentin Nielsen. Environment classifiers. In Proc. POPL, pages 26-37, 2003. Google Scholar
  37. Laurence Tratt. Compile-time meta-programming in a dynamically typed OO language. In Proc. DLS, pages 49-64, October 2005. Google Scholar
  38. Laurence Tratt. Domain specific language implementation via compile-time meta-programming. TOPLAS, 30(6):1-40, 2008. Google Scholar
  39. Takeshi Tsukada and Atsushi Igarashi. A Logical Foundation for Environment Classifiers. Logical Methods in Computer Science, 6(4:8):1-43, 2010. Google Scholar
  40. Willard van Orman Quine. Mathematical Logic. Harvard Univ. Press, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact