License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.2
URN: urn:nbn:de:0030-drops-123242
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12324/
Go to the corresponding LIPIcs Volume Portal

Pientka, Brigitte

A Modal Analysis of Metaprogramming, Revisited (Invited Talk)

pdf-format:
LIPIcs-FSCD-2020-2.pdf (0.3 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{pientka:LIPIcs:2020:12324,
  author =	{Brigitte Pientka},
  title =	{{A Modal Analysis of Metaprogramming, Revisited (Invited Talk)}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{2:1--2:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Zena M. Ariola},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/12324},
  URN =		{urn:nbn:de:0030-drops-123242},
  doi =		{10.4230/LIPIcs.FSCD.2020.2},
  annote =	{Keywords: Type systems, Metaprogramming, Modal Type System}
}

Keywords: Type systems, Metaprogramming, Modal Type System
Collection: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Issue Date: 2020
Date of publication: 28.06.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI