Thursday 13 June 2019, 14:00, LSV library: Scallina: on the Intersection of Scala and Gallina, Youssef El Bakouny (PhD student at CNAM Paris and École Supérieure d'Ingénieurs de Beyrouth).

The Coq proof assistant allows the implementation of functional programs in the Gallina specification language while providing an environment for the semi-interactive development of machine-checked proofs. Once a Gallina program has been developed, Coq can extract from it an implementation in a Hindley-Milner based functional programming language such as OCaml or Haskell. The Scala programming language, interoperable with Java, fuses the functional and object-oriented paradigms; providing a type system, based on the calculus of Dependent Object Types (DOT), which significantly differs from that of Hindley-Milner based languages such as OCaml and Haskell. On the one hand, Scala’s type system requires the generation of significantly more type information but, on the other hand, can type-check some constructs that are not typable in OCaml and Haskell. Moreover, Scala diverges significantly from Gallina; a functional specification language based on the Calculus of Inductive Constructions (Cic). Therefore, an adequate extraction of Gallina programs to readable Scala code challenges us to reconcile the differences between these two languages. In response to these challenges, the Scallina project defines a grammar delimiting a common subset of Gallina and Scala along with a translation strategy for programs conforming to the aforementioned grammar. The Scallina translator shows how these contributions can be transferred into a working prototype; enabling the practical Coq-based synthesis of Scala components. A typical application features a user implementing a functional program in Gallina, proving this program's correctness with regards to its specification and making use of Scallina to synthesize readable, traceable and idiomatic Scala code similar to what a programmer would usually write. This synthesis of readable, traceable and idiomatic Scala components eases their integration into larger Scala and Java applications; opening the door for a wider community of programmers to benefit from the Coq proof assistant. In this context, the formalization of the Scallina grammar facilitates the reasoning about the fragment of Gallina that is translatable to Scala and the corresponding translation strategy paves the way for an adequate support of the Scala programming language in Coq's native extraction mechanism. A notable contribution of our strategy regards its mapping of Gallina records to Scala; leveraging the path-dependent types of this new target output language. In this context, we have translated a list queue example which was adapted from the test suite of Coq’s Parametricity Plugin.