Dependent type systems as macros. - Stephen Chang 001; Michael Ballantyne; Milo Turner; William J. Bowman (Proc. ACM Program. Lang., 2020)