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: "John Wiegley" <johnw AT newartisans.com>
To: Calvin Beck <calvin AT disgruntledcode.com>
Cc: coq-club AT inria.fr, Xiaoyu Zhou <zhouxy AT seu.edu.cn>
Subject: Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?
Date: Thu, 28 Dec 2017 11:47:06 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=johnw AT newartisans.com; spf=Pass smtp.mailfrom=johnw AT newartisans.com; spf=None smtp.helo=postmaster AT out2-smtp.messagingengine.com
Ironport-phdr: 9a23:tt08KhEib9RqecHONHM+1J1GYnF86YWxBRYc798ds5kLTJ7zos6wAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95RWSJfH42zbYUBD+0CM+ZWoYbyqEcBoACiBQWwHu7j1iNEi2Xq0aA8zu8vERvG3AslH98WvnjaqNL1NKcUUeuozKbIzCvMb/xS2Tjj6InEfA0qrPaOXbJ3ccrRz0cuGhjDjlqOp43qJSmV1vgMs2iA9eVgU/mvh3Q7pAF2pzii38EhgZTHiIISz1DL7yR5wIAtKN2+VkF6b8SrEIFMtyGbLIt5WMUiQ3pytCkmzb0GvJi2dzUJxpQ/3xPSav2Kf5KV7h7+SeqdOzh1iGh7dL++nxq/80mtxvfiWsS631tGtCtIn93WunwQ2BHe7s6KQeZn8Ei7wzaAzQXT5/lEIU8qkarbLIYswrktlpoPr0jPBzT2mEDqjK+ObEkk//an6//8Yrr8qZ+cNol0ig7gPaQolcy/AOI4PRYUU2eH/uS80aXv/Uz/QLpUkv07iqjUvZHAKcgGu6K1HhVZ34k55xqhDjqqyNEYkmMGLFJBdhKHlY/pO1TWLfD6Cve/g1KskTlwyvDAILLgDI/CLmLfkLfgZrZy8UhcyBEpwd9D4JJUD6kNIOjvVU/pqNzYEhg5PhSozObgEdVxz58RWWaSAqCCK67Sql+J5uc3I+aWfoMVuTD9K+Ik5/H0l3M5l0UdLuGV2s48YXSmH/IuCUiSYjK4id4FD2YMlgY/V+PwlVueVTNfbHG+UuQ34TRtW6y8CoKWDKKqgLrJ4ya2EZlbdyoOXlKLEXH3X4OJRP4WdCOJK8l61DcDUO7yGMcayRiyuVqimPJcJe3O93hd7Mq72Q==
Organization: New Artisans LLC

>>>>> "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

[Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?, Xiaoyu Zhou, 12/28/2017
- Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?, Calvin Beck, 12/28/2017
  - Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?, John Wiegley, 12/28/2017