Typed syntactic meta-programming

Dominique Devriese, Frank Piessens

Research output: Chapter in Book/Report/Conference proceedingConference paper

8 Citations (Scopus)


We present a novel set of meta-programming primitives for use in a dependently-typed functional language. The types of our meta-programs 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
Title of host publicationICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming
PublisherAssociation for Computing Machinery, Inc
Number of pages13
ISBN (Print)9781450323260
Publication statusPublished - 12 Nov 2013
Event2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013 - Boston, MA, United States
Duration: 25 Sep 201327 Sep 2013


Conference2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013
CountryUnited States
CityBoston, MA


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


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

Cite this