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: Calvin Beck <calvin AT disgruntledcode.com>
To: 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 09:08:11 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=calvin AT disgruntledcode.com; spf=Pass smtp.mailfrom=calvin AT disgruntledcode.com; spf=Pass smtp.helo=postmaster AT disgruntledcode.com
Domainkey-signature: a=rsa-sha1; c=nofws; d=disgruntledcode.com; h=date :in-reply-to:references:mime-version:content-type :content-transfer-encoding:subject:to:from:message-id; q=dns; s= disgruntled; b=TvnY0VbBhtjMXDtRIDHmFMaSXUy0ZcTc3fCP5IofhS7CN/hQj Obw9Cjq/pBATZzDT4m16kyUEcXS6hgo2i06w1FVzOkazCc8mGOcE5zQf+1eO0r77 P9w4gzfqLpIXhhCpDfKB0NliYPcQSSK+gPAOGafjKF9Jrk44sQuaFE37Co=
Ironport-phdr: 9a23:pIVIURzBYEsfG9HXCy+O+j09IxM/srCxBDY+r6Qd2+wRIJqq85mqBkHD//Il1AaPAd2Craocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HObwlSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CS2ROXMhRWCNdDY2zcoUBEeoPM+VDoobnpVYOqAGzCRWwCO7tzDJDm3/43bc90+QkCQzLwhYvH9YQsHTVqtX+KbofXv6pw6nL0D7OaO9Z1i356IjWcxAhp+qBUq9xccrKxkkvDR7FjlOMqYzhITyay/gCs2+G4OV+T+6gl2knqwRorzWp28wihI7JhocPxVDF8yV02J01JcGiR0FnYt6rDpRRuD2aN4RsRMMiTH9ntDwmxb0BvJ62ejUBxpc/xxPHdvCKcZaE7gjgWeqMOzt0mXFodK6lixuy/0Ws0vDwW8233VpQoSdIkcPAum0D2hHd8MSKTvhw80G80jiVzQ/T8PtLIUUsmKrbNZEhxrkwm4IOvkTCBS/2l1/2jLKQdkU4/uin9fnobanhppCBKYB4kB3xMqMrmsCnAOQ4NBYBX3SD9Oih1rDv41f1TbZXgvEsj6XUs4zWKd4bq6O3GwNV15ws6xe7DzeoytQYmnwHIUpZdx2di4jpJVDOIPbjAPiiglSsizhrx+rbPr3nHpXNKmbMn6r9crZ69kFT1hA/wsxY55JREr0BOu78WlfttNzECR80KxC7w+H+CNlkyoweXX+PDbSCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0gX83g19ONZWuiJAQcTWzGulsC0Sfe3vlxNkbVVcLtw0vUaTYiFqfGWpBZ3GvT7MU/TwmTo+qEMHIQNb+rqaG2XKQF5lIZ2YOIF2HEj+8fIyARfYKQC6TOcB7jzoYUbWtQIgt2FelswqsmOkvFfbd5iBN7cGr79Ny/eCG0EhqrTE=

As far as I am aware this doesn't exist yet (but I haven't looked very hard). If you're thinking that there must be ocaml semantics in Coq because of the extraction mechanism, then you're in for a bit of a surprise! The extraction mechanism is not (yet) verified for any language. It's just some ad hoc code.

There's a stack overflow question which may have some useful avenues to explore:

https://cstheory.stackexchange.com/questions/37659/formal-semantics-of-ocaml-in-coq

Depending on your needs something like CakeML may be interesting to you. For verified Coq (or gallina) extraction there is the CertiCoq project, but I believe it is not yet released.

On December 28, 2017 8:49:57 AM MST, Xiaoyu Zhou <zhouxy AT seu.edu.cn> wrote:

Hi all:
  As OCaml code can be extracted from Coq code, I thinks that a implementation of the syntax and semantics of OCaml (or its subset) is embedded in Coq. Where can I get an official documentation on this topic?

Best regards
Xiaoyu Zhou

[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