Defunctionalization with Dependent Types. - Yulong Huang 002; Jeremy Yallop (Proc. ACM Program. Lang., 2023)