Tadjouddine, E. M.; Lv, W. Foundational Certification of Code Transformations Using Automatic Differentiation. csci 2014, 15, 215.