In response to the challenges associated with a Coq-based extraction of readable and traceable Scala code, the Scallina project defines a grammar delimiting a common subset of Gallina and Scala along with an optimized translation strategy for programs conforming to the aforementioned grammar. The Scallina translator shows how these contributions can be transferred into a working prototype. A typical application features a user implementing a functional program in Gallina, the core language of Coq, proving this program's correctness with regards to its specification and making use of Scallina to synthesize readable Scala components.
展开▼
