|
 
|
[BCM17] A Coq-based synthesis of Scala programs which are correct-by-construction
Conférence Internationale avec comité de lecture : FTfJP'17:19th Workshop on Formal Techniques for Java-like Programs Proceedings, June 2017, pp.2, Barcelona, Spain, (DOI: 10.1145/3103111.3104041)Mots clés: Formal methods, Functional programming, Coq, Scala, Compilation
Résumé:
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.
BibTeX
| @inproceedings { | |||
| BCM17, | |||
| title | = | "{A Coq-based synthesis of Scala programs which are correct-by-construction}", | |
| author | = | " Y. Bakouny and T. Crolard and D. Mezher ", | |
| booktitle | = | "{FTfJP'17:19th Workshop on Formal Techniques for Java-like Programs Proceedings}", | |
| year | = | 2017, | |
| month | = | "June", | |
| pages | = | "2", | |
| address | = | "Barcelona, Spain", | |
| doi | = | "10.1145/3103111.3104041", | |
| } | |||
