Yves Daaboul (May 18 2022 at 05:30): Yves Daaboul (May 18 2022 at 05:30):Hey everyone
I am an incoming software engineer.
I've been working in the past 4 months during my Final Year Project with @Bruno Barras and @Joseph Bakouny on an eventual Scala extraction. In fact we began the preliminary steps more than a year ago.
So I wanted to check if there is someone still active on the Extraction project (and who can also accept PRs) because we were able to come up with great results regarding the renaming of identifiers. It turned out also that our results have direct consequences on the code of Scheme extraction.
Please if anyone know someone, let me know. Thank you.
Maxime Dénès (May 18 2022 at 07:01):Hi Yves and welcome! Extraction is not very active in terms of new contributions, but we can certainly organize to review and merge a set of PRs.
Maxime Dénès (May 18 2022 at 07:05):So feel free to open PRs. If you have a short documentation which gives an overview of the changes you worked on and maybe how they fit with Scala extraction, it can also be useful. But if you don't, it should not be a blocker.
Karl Palmskog (May 18 2022 at 07:51):is there some theory of Scala behind the Scala extraction effort? For example, dot-iris comes to mind?
Joseph Bakouny (May 25 2022 at 09:38):Hi,
Thank you for your messages and sorry for the late reply as it has been a very busy week finalizing the grades of the semester at Saint-Joseph University (USJ).
Indeed, the implementation done by Yves, which was closely supervised by @Bruno Barras , is available under https://github.com/JBakouny/coq. Thanks for the suggestion @Maxime Dénès , we'll be soon opening a PR regarding the Scala extraction development.
This development follows the work done previously done on Scallina and backed by two publications which explain the translation of Gallina to Scala at a syntactic level and demonstrate the Scallina Proof of Concept (POC) implemented in Scala (and available under https://github.com/JBakouny/Scallina) :
El Bakouny, Y., Mezher, D. (2018). The Scallina Grammar. In: Massoni, T., Mousavi, M. (eds) Formal Methods: Foundations and Applications. SBMF 2018. Lecture Notes in Computer Science(), vol 11254. Springer, Cham. https://doi.org/10.1007/978-3-030-03044-5_7
El Bakouny, Y., Mezher, D. (2018). Scallina: Translating Verified Programs from Coq to Scala. In: Ryu, S. (eds) Programming Languages and Systems. APLAS 2018. Lecture Notes in Computer Science(), vol 11275. Springer, Cham. https://doi.org/10.1007/978-3-030-02768-1_7
In the aforementioned development the translation from miniml to the currently supported Hindley-Milner-based subset of Scala can be considered somewhat trivial and would therefore not required more verification than the currently implemented miniml to OCaml translation. However, in the future, we are aiming to support the extraction (without type casts) of a larger subset of Gallina to a subset of Scala incorporating path-dependent types and GADTs. In this case, we plan to delve into a type theoretic study based on the Calculus of Inductive Constructions (Cic) and the Dependent Object Type (DOT) calculus. In this regards, the dot-iris project could prove quite interesting. Thanks @Karl Palmskog for pointing it out.
We remain at your disposal for any further information and are eager to open the PR and merge this Scala extraction development into Coq's main codeline.
Last updated: Apr 20 2024 at 12:02 UTC