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 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 language | English |
---|---|
Title of host publication | ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming |
Publisher | Association for Computing Machinery, Inc |
Pages | 73-85 |
Number of pages | 13 |
ISBN (Print) | 9781450323260 |
DOIs | |
Publication status | Published - 12 Nov 2013 |
Event | 2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013 - Boston, MA, United States Duration: 25 Sep 2013 → 27 Sep 2013 |
Conference
Conference | 2013 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013 |
---|---|
Country | United States |
City | Boston, MA |
Period | 25/09/13 → 27/09/13 |
Keywords
- Datatype-generic programming
- Dependent types
- Meta-programming
- Tactics