A Coq-based synthesis of Scala programs which are correct-by-construction.
Proceedings of the 19th Workshop on Formal Techniques for Java-like Programs(2017)
摘要
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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要