Elaborator reflection: extending Idris in Idris

DOI10.1145/2951913.2951932zbMath1361.68035OpenAlexW2507856242MaRDI QIDQ2985777

Edwin Brady, David R. Christiansen

Publication date: 10 May 2017

Published in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2951913.2951932

zbMATH Keywords

dependent typesmetaprogrammingelaboration

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Related Items (3)

The \textsc{MetaCoq} project ⋮ Structure-preserving diagram operators ⋮ Incorporating quotation and evaluation into Church's type theory

Uses Software

• Coq
• Haskell
• Proof General
• Mtac
• Idris

This page was built for publication: Elaborator reflection: extending Idris in Idris