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.