A Coq-based synthesis of Scala programs which are correct-by-construction
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.
Tue 20 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30
|A Coq-based synthesis of Scala programs which are correct-by-construction|
Youssef El Bakouny CIMTI - ESIB - Saint-Joseph University - Beirut, Lebanon, Tristan Crolard CEDRIC - CNAM - Paris, France, Dani Mezher CIMTI - ESIB - Saint-Joseph University - Beirut, LebanonPre-print
|Iris: A Modular Foundation for Higher-Order Concurrent Separation Logic (KEYNOTE)|
Derek Dreyer MPI-SWS