# Scala extraction for Coq and Scala-like calculi in Coq

**URL:** <https://discourse.rocq-prover.org/t/scala-extraction-for-coq-and-scala-like-calculi-in-coq/531>\
**Category:** Developing the Rocq Prover\
**Created:** [December 18, 2019, 11:31am UTC](https://discourse.rocq-prover.org/t/scala-extraction-for-coq-and-scala-like-calculi-in-coq/531 "2019-12-18T11:31:07Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [December 18, 2019, 11:31am UTC](https://discourse.rocq-prover.org/t/scala-extraction-for-coq-and-scala-like-calculi-in-coq/531/1 "2019-12-18T11:31:07Z")

</div>

The latest Coq Working Group [discussed](https://github.com/coq/coq/wiki/Next-Coq-Working-Group#2pm-330pm) 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](https://link.springer.com/chapter/10.1007%2F978-3-030-03044-5_7) is a subset of Scala designed to capture (be the translation target of) a significant fragment of Coq’s Gallina language. A [prototype](https://github.com/JBakouny/Scallina) Scala implementation of the Gallina-to-Scallina translation is available.
- [DOT](https://infoscience.epfl.ch/record/215280) (dependent object types) is a calculus aimed at capturing a core fragment of Scala, which has been [formalized](https://plg.uwaterloo.ca/~olhotak/pubs/oopsla17.pdf) in Coq along with its [metatheory](https://github.com/amaurremi/dot-calculus/tree/master/src/simple-proof).
- [pDOT](https://arxiv.org/abs/1904.07298v1) is a generalization of the DOT calculus which is closer to Scala, and also has corresponding Coq [metatheory](https://github.com/amaurremi/dot-calculus/tree/master/src/extensions/paths).

@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](https://isabelle.in.tum.de/doc/codegen.pdf) facilities.