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
Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf (PDF)
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