A Coq-based synthesis of Scala programs which are correct-by-construction
Programming Languages
2017-06-19 v1 Logic in Computer Science
Abstract
The present paper introduces Scala-of-Coq, a new compiler that allows a Coq-based synthesis of Scala programs which are "correct-by-construction". A typical workflow features a user implementing a Coq functional program, proving this program's correctness with regards to its specification and making use of Scala-of-Coq to synthesize a Scala program that can seamlessly be integrated into an existing industrial Scala or Java application.
Keywords
Cite
@article{arxiv.1706.05271,
title = {A Coq-based synthesis of Scala programs which are correct-by-construction},
author = {Youssef El Bakouny and Tristan Crolard and Dani Mezher},
journal= {arXiv preprint arXiv:1706.05271},
year = {2017}
}
Comments
2 pages, accepted version of the paper as submitted to FTfJP 2017 (Formal Techniques for Java-like Programs), June 18-23, 2017, Barcelona , Spain