SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts

Laila El-Beheiry
(Carnegie Mellon University)
Giselle Reis
(Carnegie Mellon University)
Ammar Karkour
(Carnegie Mellon University)

Formally reasoning about functional programs is supposed to be straightforward and elegant, however, it is not typically done as a matter of course. Reasoning in a proof assistant requires "reimplementing" the code in those tools, which is far from trivial. SMLtoCoq provides an automatic translation of SML programs and function contracts into Coq. Programs are translated into Coq specifications, and function contracts into theorems, which can then be formally proved. Using the Equations plugin and other well established Coq libraries, SMLtoCoq is able to translate SML programs without side-effects containing partial functions, structures, functors, records, among others. Additionally, we provide a Coq version of many parts of SML's basis library, so that calls to these libraries are kept almost as is.

In Elaine Pimentel and Enrico Tassi: Proceedings Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2021), Pittsburgh, USA, 16th July 2021, Electronic Proceedings in Theoretical Computer Science 337, pp. 71–87.
Published: 16th July 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: