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: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?
Date: Mon, 1 Jan 2018 21:29:09 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb0-f170.google.com
Ironport-phdr: 9a23:RlcNUBeyW8lkvPzwfFVN+DqvlGMj4u6mDksu8pMizoh2WeGdxcS+ZR7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM28m/XhMx+gqxYvRyvuQBwzpXOb42JLvdzZL/Rcc8YSGdHQ81fVzZBAoS5b4YXE+cOJuZYr4jmp1sOsxS+BhSnCf/pyjBSgH/5wLAx3uM7Hg7d3AwgHskOsHTKo9X2LqsdS+a1w7POzTredf9W2Db96JTHch06rvGMWKh/ccvVyUU1CwzFiVCQpJXjMjiI2OoNtG2b4PBhVeKpk2MotwZxoiKpxsgyjonJgpgZxU7Z+iVk2Io6Odq4SFR9YdG6FJtQszuWO5FoTcw/XmFkoDo1yrgbuZKhYicF1YknyhjCYPKEa4iF+gzvWPqVLDtih39oeKiziwiv/UWu0OHwS8u53EpMoyFYiNfDrGoN2AbW6sWfSvty4EOh2TGX2gDW8O5EIEQ0mbPbKpE63rI8j5QTvVnBEyPqgkn2g6iWdkIr+uis9evreKnpppiZN4NsiwH+NLohmtCnDOgmLgQDW3KX9Oe82bH540H1XbtHgucrnqTbrJzWPcEbqbS4Aw9R3IYj8RG/DzK+3dsChnYHLFNFeAmHj4f3OFHCOur3DfGljFSqjThn3fHGPrz9ApXCNXXDn7Lhcqx8605Y0gY80ddf55dMBrEbPP3zQlPxtMDfDhIhLwO0xP/nBMxh2YMaRGKAGbSUMLjSsF+N/uIgOfOAZI4TuDbnKvgq/eTijXEjmQxVQa781pwOLXu8A/4ud06eeD/nhsoLOWYMpAs3CuLw3g6sSzlWMl+4X6Mn5jw4QKugBIHPDtSkiryAxye2HdtfYGlABhaNEGvnX4qBUvYILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/Iw==

The following paper seems to be about a Coq formalization of parametricity results for OCaml.

https://www.cs.cmu.edu/~crary/papers/2017/mapp.pdf

The fragment (of OCaml) considered in the paper certainly seemed larger than what is needed to translate Coq to OCaml.

I guess to formalize parametricity, it would be necessary to formalize the syntax, operational semantics, and various theorems about the semantics.

Thus, I suspect the code released with the paper may contain what you are looking for.

The paper contains the following link for Coq sources:

http://www.cs.cmu.edu/~crary/papers/2016/mapp.tgz

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Dec 28, 2017 at 10:49 AM, 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

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