Showing 1–1 of 1 results for author: Mezher, D

A Coq-based synthesis of Scala programs which are correct-by-construction

Authors: Youssef El Bakouny, Tristan Crolard, Dani Mezher

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 existin… ▽ More 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. △ Less

Submitted 16 June, 2017; originally announced June 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