Elaborator reflection: extending Idris in Idris

DOI10.1145/2951913.2951932MaRDI QIDQ2985777zbMATH OpenOpenAlexFDO

Authors David R. Christiansen, Edwin Brady

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 typeselaborationmetaprogramming

Mathematics Subject Classification ID

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

Recommendations

• Idris, a general-purpose dependently typed programming language: Design and implementation
• Hindley-Milner elaboration in applicative style (functional pearl)
• Typed syntactic meta-programming
• Auto in Agda. Programming proof search using reflection
• scientific article; zbMATH DE number 2185723

Cited in

(5)

• Incorporating quotation and evaluation into Church's type theory
• The \textsc{MetaCoq} project
• Structure-preserving diagram operators
• scientific article; zbMATH DE number 1231541 (Why is no real title available?)
• Rapid prototyping formal systems in MMT: 5 case studies

Describes a project that uses

Uses Software

• Mtac
• Idris
• Haskell
• Proof General
• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2985777)