A Modal Analysis of Metaprogramming, Revisited (Invited Talk)

Author Brigitte Pientka

Thumbnail PDF


  • Filesize: 261 kB
  • 3 pages

Document Identifiers

Author Details

Brigitte Pientka
  • McGill University, Montreal, QC, Canada


I would like to thank my collaborators: Wilson Cheang, Samuel Gélineau, Junyoung Jang, and Stefan Monnier.

Cite AsGet BibTex

Brigitte Pientka. A Modal Analysis of Metaprogramming, Revisited (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Metaprogramming is the art of writing programs that produce or manipulate other programs. This opens the possibility to eliminate boilerplate code and exploit domain-specific knowledge to build high-performance programs. Unfortunately, designing language extensions to support type-safe multi-staged metaprogramming remains very challenging. In this talk, we outline a modal type-theoretic foundation for multi-staged metaprogramming which supports the generation and the analysis of polymorphic code. It has two main ingredients: first, we exploit contextual modal types to describe open code together with the context in which it is meaningful; second, we model code as a higher-order abstract syntax (HOAS) tree within a context. These two ideas provide the appropriate abstractions for both generating and pattern matching on open code without committing to a concrete representation of variable binding and contexts. Our work is a first step towards building a general type-theoretic foundation for multi-staged metaprogramming which on the one hand enforces strong type guarantees and on the other hand makes it easy to generate and manipulate code. This will allow us to exploit the full potential of metaprogramming without sacrificing reliability of and trust in the code we are producing and running.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Type structures
  • Theory of computation → Lambda calculus
  • Theory of computation → Modal and temporal logics
  • Type systems
  • Metaprogramming
  • Modal Type System


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


  1. Andrew Cave and Brigitte Pientka. Programming with binders and indexed data-types. In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12), pages 413-424. ACM Press, 2012. Google Scholar
  2. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555-604, 2001. URL: https://doi.org/10.1145/382780.382785.
  3. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9(3):1-49, 2008. Google Scholar
  4. Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pages 371-382. ACM Press, 2008. Google Scholar
  5. Brigitte Pientka, Andreas Abel, Francisco Ferreira, David Thibodeau, and Rebecca Zucchini. A type theory for defining logics and proofs. In 34th IEEE/ ACM Symposium on Logic in Computer Science (LICS'19), pages 1-13. IEEE Computer Society, 2019. Google Scholar
  6. Brigitte Pientka and Andrew Cave. Inductive Beluga:Programming Proofs (System Description). In 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Computer Science (LNCS 9195), pages 272-281. Springer, 2015. Google Scholar
  7. Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), pages 163-173. ACM Press, 2008. Google Scholar
  8. Brigitte Pientka and Joshua Dunfield. Beluga: a framework for programming and reasoning with deductive systems (System Description). In Jürgen Giesl and Reiner Haehnle, editors, 5th International Joint Conference on Automated Reasoning (IJCAR'10), Lecture Notes in Artificial Intelligence (LNAI 6173), pages 15-21. Springer, 2010. Google Scholar