Elaborator reflection: extending Idris in Idris. - David R. Christiansen; Edwin C. Brady (ICFP, 2016)

Sequential decision problems, dependent types and generic solutions. - Nicola Botta; Patrik Jansson; Cezar Ionescu; David R. Christiansen; Edwin C. Brady (Log. Methods Comput. Sci., 2017)