Projects per year
Abstract
Many programming languages and proof assistants are defined by elaboration from a high-level language with a great deal of implicit information to a highly explicit core language. In many advanced languages, these elaboration facilities contain powerful tools for program construction, but these tools are rarely designed to be repurposed by users. We describe elaborator reflection, a paradigm for metaprogramming in which the elaboration machinery is made directly available to metaprograms, as well as a concrete realization of elaborator reflection in Idris, a functional language with full dependent types. We demonstrate the applicability of Idris’s reflected elaboration framework to a number of realistic problems, we discuss the motivation for the specific features of its design, and we explore the broader meaning of elaborator reflection as it can relate to other languages.
Original language | English |
---|---|
Title of host publication | Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016) |
Place of Publication | New York |
Publisher | ACM |
Pages | 284-297 |
Number of pages | 14 |
ISBN (Print) | 9781450342193 |
DOIs | |
Publication status | Published - 4 Sept 2016 |
Event | ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming - Nara Kasugano International Forum, Nara, Japan Duration: 18 Sept 2016 → 24 Sept 2016 Conference number: 21 http://conf.researchr.org/home/icfp-2016 |
Publication series
Name | ACM SIGPLAN Notices |
---|---|
Publisher | Association for Computing Machinery |
Number | 9 |
Volume | 51 |
ISSN (Print) | 0362-1340 |
ISSN (Electronic) | 1558-1160 |
Conference
Conference | ICFP 2016 - 21st ACM SIGPLAN International Conference on Functional Programming |
---|---|
Abbreviated title | ICFP 2016 |
Country/Territory | Japan |
City | Nara |
Period | 18/09/16 → 24/09/16 |
Internet address |
Keywords
- Metaprogramming
- Dependent types
- Elaboration
Fingerprint
Dive into the research topics of 'Elaborator reflection: extending Idris in Idris'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Type-Driven Verification of Communic: Type-driven verification of communicating systems
Brady, E. C. (PI)
1/05/16 → 30/04/17
Project: Standard