Scala extraction for Coq and Scala-like calculi in Coq

The latest Coq Working Group discussed the possibility of support for extraction of Coq programs to Scala, and also formalizations of Scala-like calculi in Coq. This is an attempt to quickly document resources on this topic.

  • Scallina is a subset of Scala designed to capture (be the translation target of) a significant fragment of Coq’s Gallina language. A prototype Scala implementation of the Gallina-to-Scallina translation is available.
  • DOT (dependent object types) is a calculus aimed at capturing a core fragment of Scala, which has been formalized in Coq along with its metatheory.
  • pDOT is a generalization of the DOT calculus which is closer to Scala, and also has corresponding Coq metatheory.

@Blaisorblade made the following comment on Coq’s gitter chat:

elaborating Scala to DOT is not trivial, even for the output of Scallina, especially because it sometimes uses Scala abstract types (when translating Coq ones). [On the other hand], the work on pDOT should [address] the main obstacle found in the last attempt

The existing Scala extraction for Isabelle/HOL is documented as part of Isabelle’s codegen facilities.

3 Likes