HackerPapers

arXiv:1706.05271cs.PL

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

Youssef El Bakouny, Tristan Crolard, Dani Mezher

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

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.

arXiv 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
Journal reference
DOI
doi:10.1145/3103111.3104041
Subjects
cs.PLProgramming Languages cs.LOLogic in Computer Science

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Jun 2017 to Jun 2017. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.