Typed syntactic meta-programmi

Dominique Devriese, Frank Piessens

Research output: Contribution to journalArticlepeer-review

5 Citations (Scopus)


We present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our metaprograms provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.

Original languageEnglish
Pages (from-to)73-85
Number of pages13
JournalACM SIGPLAN Notices
Issue number9
Publication statusPublished - 1 Sep 2013


  • Datatype-generic programming
  • Dependent types
  • Meta-programming
  • Tactics


Dive into the research topics of 'Typed syntactic meta-programmi'. Together they form a unique fingerprint.

Cite this