Pickard, M., & Hutton, G. (2021). Calculating dependently-typed compilers (functional pearl). Proceedings of the ACM on Programming Languages, 5(ICFP), 1-27. https://doi.org/10.1145/3473587