Elaborator reflection : extending Idris in Idris
- Submitting institution
-
University of St Andrews
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 252026640
- Type
- E - Conference contribution
- DOI
-
10.1145/2951913.2951932
- Title of conference / published proceedings
- Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)
- First page
- 284
- Volume
- 51
- Issue
- 9
- ISSN
- 0362-1340
- Open access status
- Compliant
- Month of publication
- September
- Year of publication
- 2016
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
1
- Research group(s)
-
D - Programming Languages
- Citation count
- 8
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Many modern programming languages build high level features on top of a small, verifiable core. This paper describes a general method, elaborator reflection, for allowing a programmer to access the core language and manipulate it, to extend the high level language. Reflection allows features such as proof automation, generic programming and reasoning about side-effects to be implemented as extensible libraries, rather than being built in to the language itself. The paper describes reflection for Idris, and since publication the same approach is now implemented in another language, Agda.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
