Title: Typed syntactic meta-programming
Authors: Devriese, Dominique ×
Piessens, Frank #
Issue Date: 2013
Publisher: ACM Press
Series Title: ACM SIGPLAN Notices vol:48 issue:9 pages:73-85
Abstract: 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 type-safe 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.
ISSN: 0362-1340
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
icfp002-devriese-authorversion.pdfOA article Published 326KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science