SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts. - Laila El-Beheiry; Giselle Reis; Ammar Karkour (LFMTP, 2021)