From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id AA5F38239C; Mon, 25 Dec 2017 14:28:20 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vietlq85@gmail.com; spf=Pass smtp.mailfrom=vietlq85@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f182.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of vietlq85@gmail.com) identity=pra; client-ip=209.85.220.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="vietlq85@gmail.com"; x-sender="vietlq85@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of vietlq85@gmail.com designates 209.85.220.182 as permitted sender) identity=mailfrom; client-ip=209.85.220.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="vietlq85@gmail.com"; x-sender="vietlq85@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-qk0-f182.google.com) identity=helo; client-ip=209.85.220.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="vietlq85@gmail.com"; x-sender="postmaster@mail-qk0-f182.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AJdu9rhWWNTV0dkGxCxomQcRDBMTV8LGtZVwlr6E/?= =?us-ascii?q?grcLSJyIuqrYbRWAt8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjc?= =?us-ascii?q?hE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRo?= =?us-ascii?q?LerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf?= =?us-ascii?q?5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXM?= =?us-ascii?q?TRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlD?= =?us-ascii?q?kIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAIy8?= =?us-ascii?q?YYsBAeQCM+hFsYfyu0ADogGiCQS2Hu7j1iNEi33w0KYn0+ohCwbG3Ak4Et0BsX?= =?us-ascii?q?Tbssn1P7oUX++r0aLFyivDb/JI1jfh7IjIaxMsrPGXULJ/dMre00gvFwffglqM?= =?us-ascii?q?rozlOiqY2+IQuGaV6OpgUPigi28hqwxppjivx94sipTIho0Iy1DE6SV4zJ8xJd?= =?us-ascii?q?KiTk57bsSoEJxKtyGVL4d2TcIiQ31ouCYn0bIKo4K0fC8PyJg/wx7fauWHc5WJ?= =?us-ascii?q?4h3+VeaRPTd5iGtheL2lgRay/lKsxvf7Vsmu31ZHqDdOnNrUtn0VyRDf9syKRu?= =?us-ascii?q?F+80qhwzqDyR7f5v1eLUwplqfXNZgsyaMqmJUJq0TMBCr2lV32jKCIckUk/fCl?= =?us-ascii?q?6+H9bbXnop+QLpZ0igLiPqg3lMyzHOc1PhYUU2iU/uS807Lj/UnnT7lQkvI2la?= =?us-ascii?q?zZvIjbJcQduKG5HxdY3pg/5xu7FTur09QVkWMZIF5bZB6LlZXlNlLQLPzgCPew?= =?us-ascii?q?mVWskDNlx/DcOb3hB43ALmbCkLj/YbZ971dcxQkzwN1E6JJUD6sOIPP3WkPrqN?= =?us-ascii?q?PYCRo5PxSuw+n7ENV9yp8eWWWXD6CFKqzStFuI6vsrI+mNf48VpC3wK+Ml5v7r?= =?us-ascii?q?lX82g0URfaiv3ZsNaXC3BO5qI0uDYXD0mNcODX8KvhYiTOztkFCCViJcaGy3X6?= =?us-ascii?q?I4/z07CoWmApzYRo22m7yA3CK7HoVMaWxcC1CMF23od4SeVPsWZiKSOJwprjtR?= =?us-ascii?q?a7GnA6Qh3BfmkgD9g+5sLuPSvCsXssi5jINd6OjalBV0/jtxWZezyWaIGl91k3?= =?us-ascii?q?9AYzJ+iL5+rFB50wfe+ad9iv1cU9dU4qUaAU8BKZfAwrkiWJjJUQXbc4LMEQ7+?= =?us-ascii?q?Tw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A/AQDB+0BahrbcVdFdGgEBAQEBAgEBA?= =?us-ascii?q?QEIAQEBAYJKgVp0FBMHg39jJDJQlyyCAYh/hVSKawojgzqBXgKESwdDFAEBAQE?= =?us-ascii?q?BAQEBAQESAQEBCAsLCCgvgjgkAYJGAQEBAQIBIx0BGx0BAwELBgULDSoCAiEBA?= =?us-ascii?q?REBBQEcBhOKFQEDDQgQmhNAjBCCBQUBHIMLBYNXChknDVlRgWQBAQEBAQUBAQE?= =?us-ascii?q?BAQEBAQEXAgYSg3qCEoZtgmtEAYF+HYJqgmUFgS0BAaFgMwgBAYFkCoYViDSEf?= =?us-ascii?q?oIXhhaLUI0kPoVygxsUBSCBFzaBcW9SMlKBJQmCPB+Bc0E3iwUBAQE?= X-IPAS-Result: =?us-ascii?q?A0A/AQDB+0BahrbcVdFdGgEBAQEBAgEBAQEIAQEBAYJKgVp?= =?us-ascii?q?0FBMHg39jJDJQlyyCAYh/hVSKawojgzqBXgKESwdDFAEBAQEBAQEBAQESAQEBC?= =?us-ascii?q?AsLCCgvgjgkAYJGAQEBAQIBIx0BGx0BAwELBgULDSoCAiEBAREBBQEcBhOKFQE?= =?us-ascii?q?DDQgQmhNAjBCCBQUBHIMLBYNXChknDVlRgWQBAQEBAQUBAQEBAQEBAQEXAgYSg?= =?us-ascii?q?3qCEoZtgmtEAYF+HYJqgmUFgS0BAaFgMwgBAYFkCoYViDSEfoIXhhaLUI0kPoV?= =?us-ascii?q?ygxsUBSCBFzaBcW9SMlKBJQmCPB+Bc0E3iwUBAQE?= X-IronPort-AV: E=Sophos;i="5.45,455,1508796000"; d="scan'208,217";a="306853428" Received: from mail-qk0-f182.google.com ([209.85.220.182]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 25 Dec 2017 14:28:19 +0100 Received: by mail-qk0-f182.google.com with SMTP id 143so26703930qki.2; Mon, 25 Dec 2017 05:28:19 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=OXSMlc0zwo0TsGFaYNeqwOqeubjQqU77W138XrQN3z8=; b=jBJHx711Y7bg8GQGoIJfERrGOkgLUMa8KermchoBMisUzyoV7BAo6HyCMtCP/hZuCp jQxOvZIGuJAzhPGHOc/zI75vmtnhEen12zi7UJYvXDdB5ubDu744xwl0/FfJKTdRmVGv +MJt1O+h5c0wel2rEy4tyFvR6uWpm1z9ebdIxhuTqXiJIcq1IGwSxLPF2KtOXE/Scj/Y ta1uhnBife0aEKUK3W9QkMzxj5K1P9rCtJrOUHlpsK1lc/CCUSNx6Zo1zkM9vU066pJl qlkVXrz1DIpQuygANZEttJmP74fLnzvUK7L0JF8kcv5E3ia7jBU9gsMppdcGkPYCjIqP 1m9g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=OXSMlc0zwo0TsGFaYNeqwOqeubjQqU77W138XrQN3z8=; b=Q7S7iqdCfek/2lAdxKCi16Voffl0qogu3uZy7yF5V/nq1ptsBftTcM10VLKEive0j3 +pD6jzAIqtYiiBfDXuf5I9xHdt1RYTDwmA9ekvH5YkjWHwOW5ar7JApFMXPthgOGTc8Q s06mSSFrdxT+fBRL7Efeq0YPw1nP3aCwvqqasv60jftgFg9lkYLX4eXnhXcW19fpVsEX FM8OIzkg97b8Y9AxLhoh9x/pXpAC39/6WhKbPjpCcasIOO8486HfC4QbWxZVz11vycoH lfhz3jejUWNGDpHSJT4yK2hE35e7ZP289J+2vAxuNreFJLkI1rDKDKbVGZWkaEinwtUn 94pw== X-Gm-Message-State: AKGB3mKTyftEyIlbabR+LV2j0SODMuI+sehIDAy7tg7oLvJLiotR7dOI eHmO2CmGIFoGc0xzAdT0EHrh3/kAzQVgK1ydFV8= X-Google-Smtp-Source: ACJfBovROH6WigvPTyyjdxWcFqV96y3f3rq3/DeOWogWuuZ47aeksF8cYoi/y28KxAvzEhxgXhmPWdtNeW2/bOCL8EA= X-Received: by 10.55.185.132 with SMTP id j126mr29831607qkf.275.1514208497876; Mon, 25 Dec 2017 05:28:17 -0800 (PST) MIME-Version: 1.0 Received: by 10.140.84.148 with HTTP; Mon, 25 Dec 2017 05:28:17 -0800 (PST) In-Reply-To: References: From: Viet Le Date: Mon, 25 Dec 2017 13:28:17 +0000 Message-ID: To: Van Chan Ngo Cc: Arthur Breitman , OCaml Mailing List , ocaml-jobs@inria.fr Content-Type: multipart/alternative; boundary="94eb2c04309aa1c45005612a23b8" Subject: Re: [Caml-list] Blockchains in OCaml --94eb2c04309aa1c45005612a23b8 Content-Type: text/plain; charset="UTF-8" Hi all, Only one year after this message, I found interest in building a blockchain and smart contracts in OCaml. May I know how far is the EVM formalisation in Coq? There aren't many materials / blockchain implementations in OCaml but I found some interesting links: https://github.com/LaurentMazare/btc-ocaml http://www.liquidity-lang.org/ https://github.com/tezos/tezos https://github.com/pirapira/eth-isabelle https://github.com/pirapira/ethereum-formal-verification-overview I would like to know more if anyone has more information. Thanks, Viet On 10 October 2016 at 15:00, Van Chan Ngo wrote: > Hi Arthur, > > It is interesting to implement blockchains in functional language like > OCaml. I am happy to hear more about this project. > > FYI, a related work, we are in progress to formalize the Ethereum Virtual > Machine (EVM, the running environment of smart contracts) in Coq. > > Best, > -Chan > > > On Oct 5, 2016, at 11:59 PM, Arthur Breitman wrote: > > If you find this intriguing and enjoy working in OCaml, please reach out: > we're hiring! If you lean on the academic side and have experience with > formal verification, reach out as well! We'd be interested in proving the > correctness of some aspects of the protocol or sponsoring research in the > field in general (within our modest means). > > > -- Kind regards, Viet --94eb2c04309aa1c45005612a23b8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi all,

Only one year after this messag= e, I found interest in building a blockchain and smart contracts in OCaml. = May I know how far is the EVM formalisation in Coq?

There aren't many materials / blockchain implementations in OCaml but= I found some interesting links:





=



On 10 October 2016 at 15:= 00, Van Chan Ngo <chan.ngo2203@gmail.com> wrote:
Hi Arthur,<= div>
It is interesting to implement blockchains in functional= language like OCaml. I am happy to hear more about this project.

FYI, a related work, we are in progress to formalize the Et= hereum Virtual Machine (EVM, the running environment of smart contracts) in= Coq.

Best,
-Chan
=


On Oct 5,= 2016, at 11:59 PM, Arthur Breitman <arthurb@tezos.com> wrote:


=



--
Kind regards,
Viet
--94eb2c04309aa1c45005612a23b8--