Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman. 2020. Dependent Type Systems as
Macros. Proc. ACM Program. Lang. 4, POPL, Article 3 (January 2020) - https://dl.acm.org/ft_gateway.cfm?id=3371071 (Redirects to download PDF)
> We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages