一种基于Coq的结构正确的Scala程序综合
A Coq-based synthesis of Scala programs which are correct-by-construction
摘要：
本文介绍了一个新的编译器，允许一个基于Coq的合成的Scala程序是“正确的建设”。一个典型的工作流程的特点是用户实现一个Coq函数程序，证明这个程序的正确性，并利用Scala-of-Coq来合成一个可以无缝集成到现有工业Scala或Java应用程序中的Scala程序。
英文摘要：
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分析而来，可能存在错误，请以论文正文为准。
