VERIFYING AN EFFECT-HANDLER-BASED DEFINE-BY-RUN REVERSE-MODE AD LIBRARY. - DE VILHENA, PAULO EMÍLIO; POTTIER, FRANÇOIS (Logical Methods in Computer Science (LMCS), 2023)