Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study. - Cyprien Mangin; Matthieu Sozeau (CoRR, 2015)

Equations reloaded: high-level dependently-typed functional programming and proving in Coq. - Matthieu Sozeau; Cyprien Mangin (Proc. ACM Program. Lang., 2019)