Formalizing Program Equivalences in Dependent Type Theory. - Giorgio Marabelli; Alberto Momigliano (ICTCS, 2019)