coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>, Calvin Beck <calvin AT disgruntledcode.com>, Xiaoyu Zhou <zhouxy AT seu.edu.cn>
Subject: Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?
Date: Mon, 1 Jan 2018 21:21:00 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
Ironport-phdr: 9a23:9FsMgBPgIQDBlBj1Ad8l6mtUPXoX/o7sNwtQ0KIMzox0I//5rarrMEGX3/hxlliBBdydt6odzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlViDanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZXMlRWSxPDI2/YYUSEeQOIf1Vr5Xhq1YUsReyGRWgCeHpxzRVhnH2x6o60+E5HAzbxgMgBM8FvmnMrNX0KKcSTf66zLPTzT7eaP5Zwi3x55LSfhEvu/2MRqpwccvNyUkzCQzFlE6QpJfqPzOQzOsNsmyb4/B8WuKojm4qsgd8qSWhyMcrj4nGnIMVylbc+CV/3ok0K8e3SFRnYd6lC5tfrSeaN5BsTsw+RGFovT42yqYHuZ60ZCgKzI4oxxjFZ/yAaYiI7QrvVOeLITd5inJpYry/hwy0/EO9yeP8TtG53EhWoidBiNXBtXAA2wbN5sSZVvdx5Fqt1DeL2g3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLunUX5lq6WdkE99uix6OTrfqzqppGBO4J1jgzyKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqkqTBrpzWOcAWqrS6DgJVyIov9QizAyu83NgFnHQKKEpJeBedgIjoP1HOLur4DfC6g1m0izhn3erJMqfvA5nXNXjDiLbhfaph60FC0goz1stS551RCr4bIfLzXlX9u8DfDh88KwC02froCM1h1oMCXmKCGrOWMKTLsVOR+u0vJ/SMa5QOtTbmK/kl4ubugmUjlV8ce6mpx5oXZ2qiEvRoOUXKKUbr1/wGCC8huhc0BLjhj0THWjpObV6zWbg973c1EtTiRazKQp6shvSr0Sy4Vsldb2RYC1akHXbzeJ+ZXesIZS6ZJcNs1DcDUO7lA78g3Ba/qUfIy716Zr7G+ioFpYPLz9VooeDfiFc582onId6a1jSnRno8pXsJWyM7xrs39UY7wxGcl7NgguBEGMZIz/xMWwY+c5XbyropWJjJRgvdc4LRGx6dSdK8DGR0F4ppzg==

The documentation is in Pierre Letouzey's PhD thesis and later articles.
https://www.irif.fr/en/users/letouzey/science

This is also a recent formalization:
https://popl18.sigplan.org/event/cpp-2018-uf-minimizing-the-coq-extraction-tcb

Matthieu Sozeau's work on Program/Equations is a partial converse, it
takes functional programs and embeds them into Coq's type theory.

On Thu, Dec 28, 2017 at 8:47 PM, John Wiegley
<johnw AT newartisans.com>
wrote:
>>>>>> "CB" == Calvin Beck
>>>>>> <calvin AT disgruntledcode.com>
>>>>>> writes:
>
> CB> As far as I am aware this doesn't exist yet (but I haven't looked very
> CB> hard). If you're thinking that there must be ocaml semantics in Coq
> CB> because of the extraction mechanism, then you're in for a bit of a
> CB> surprise! The extraction mechanism is not (yet) verified for any
> language.
> CB> It's just some ad hoc code.
>
> I think a nice first step would be to establish the semantics of MiniML,
> which
> Coq appears to "extract" to first, before translating MiniML into the target
> language.
>
> --
> John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
> http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?, Bas Spitters, 01/01/2018
- <Possible follow-up(s)>
- Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?, Abhishek Anand, 01/02/2018