New paper submission: “Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection”

I just finished a submission to IFL 2014. It’s a paper about Idris’s quasiquotations mechanism, which allow the use of high-level Idris syntax to describe low-level reflected terms, with the ability to escape from quotation in chosen areas and intentionally control the details of the representation. This is very much inspired by Lisp quasiquotation.

You can find the paper on my academic page. Because of the IFL submission process, I have ample time to make changes, so if I’ve made a mistake or failed to explain something clearly, I’d love to hear about it!