Calculating dependently-typed compilers (functional pearl). - Mitchell Pickard; Graham Hutton (Proc. ACM Program. Lang., 2021)