coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Xiaoyu Zhou" <zhouxy AT seu.edu.cn>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Is there an official documentation of formal semantics of Ocaml in Coq?
Date: Thu, 28 Dec 2017 23:49:57 +0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=zhouxy AT seu.edu.cn; spf=SoftFail smtp.mailfrom=zhouxy AT seu.edu.cn; spf=None smtp.helo=postmaster AT hwp1.icoremail.net
Ironport-phdr: 9a23:r/evHxBFc3D/j6Ff68CbUyQJP3N1i/DPJgcQr6AfoPdwSPv7osbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzZhMJzg61UvB2vqRtjw4PPfIGVLfV+cr/Dcd8GR2dMWNtaWSxbAoO7aosCF+QNMudZr4bnoFsPrQa+DhSvC+PvzT9Im3H61rA93uUgEQHG2xEgHt0OsXnPt9X6KroSXfqrw6bV0DXPde9Z2THk5YXObxsvoumMUKptfcffzUQjDR7Jg1SOpYD/Pz6Zyv4BvmyU4uZ4SO6jlXMrpxtvrjWhxMogkJfFi4wLxlze6yl13IA4LsCiRkFhe96rCp5QujmaN4RoRsMiRHlluCY0y70epJK3ZikKx4ggxx7FdfOHdpKH4hPnVOqLJzd3mm5ldKq+hxa070eg1vXxWtS63VtOtCZJj9jBum4X2xHT9sSLUP9w80i51TaKzQ/T6+VEIU4ularcLp4s2r8xlpoUsUTeES73mF77jLSIeUU54OSn9fnoYqj8qpCAMY94khv+Pbg2msyjHeQ4NRADUHSc+eSlzbHs4Un5QKhRgfAtianYsJXaJdwBqaKjAg9V1Jwj6xelADu83tQYhypPEFUQLBmAls3iP0zECPH+F/a2xVq2xmRF3ffDa/fRA5zKP2WLorfmYPw1v1xczxcj3PhE6o8SB70cZvn1DByi/OfEBwM0ZlTni93sD89wg9sT

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