基于 Coq 的构造正确 Scala 程序综合
编程语言
2017-06-19 v1 计算机科学中的逻辑
摘要
本文介绍了 Scala-of-Coq，这是一种新型编译器，允许基于 Coq 综合出“构造正确”的 Scala 程序。典型的工作流程是：用户实现一个 Coq 函数式程序，证明该程序相对于其规范的正确性，并利用 Scala-of-Coq 综合出一个可以无缝集成到现有工业级 Scala 或 Java 应用程序中的 Scala 程序。
引用
@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}
}
备注
2 pages, accepted version of the paper as submitted to FTfJP 2017 (Formal Techniques for Java-like Programs), June 18-23, 2017, Barcelona , Spain