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 AF72780023; Mon, 10 Oct 2016 16:00:35 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chan.ngo2203@gmail.com; spf=Pass smtp.mailfrom=chan.ngo2203@gmail.com; spf=None smtp.helo=postmaster@mail-qk0-f170.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of chan.ngo2203@gmail.com) identity=pra; client-ip=209.85.220.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="chan.ngo2203@gmail.com"; x-sender="chan.ngo2203@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of chan.ngo2203@gmail.com designates 209.85.220.170 as permitted sender) identity=mailfrom; client-ip=209.85.220.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="chan.ngo2203@gmail.com"; x-sender="chan.ngo2203@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-f170.google.com) identity=helo; client-ip=209.85.220.170; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="chan.ngo2203@gmail.com"; x-sender="postmaster@mail-qk0-f170.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AaX1ONxx0Cpc0a2TXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?0esVIJqq85mqBkHD//Il1AaPBtSBrakUwLSJ++C4ACpbvsbH6ChDOLV3FDY7yu?= =?us-ascii?q?wu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9?= =?us-ascii?q?Dq3PF4XTl8W60fyps92WOl0QxWn1XbQnBQ+qrRjL/uMMjIp+L683gk/AuGdIZv?= =?us-ascii?q?5c7X9lN1WI2R3745Hj0oRk9nFusvRp3M5JV+3ccKNwGbdYBTJgNW8yvpez7jHM?= =?us-ascii?q?SAKO4j0XVWBAwUkAOBTM8ByvBsS5iSD9rOconXDCZcA=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AJAgDlnftXhqrcVdFbGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFwEBBAEBCgEBglw1AQEBAQGBcKQ2iEaGV4UUgguGIAKCDzoSAQEBAQE?= =?us-ascii?q?BAQEBAQESAQEBCAsLCRkvQRKBXwQBFQEEghABAQEDARIuARsdAQMBCwYFBAcNL?= =?us-ascii?q?iMRAQUBHAYTIogTAQMPCKdIgTI+Mo0tgl8Fg2QKGScNU4J9AQEBAQEBBAEBAQE?= =?us-ascii?q?BAQEBAQEBFAMGEIgqgliHd4IvAQSBIQGYUwgBAYEmjleBboRngwaGGYxkE4I9M?= =?us-ascii?q?YERJQaDUCCBelaFR4EHgUEBAQE?= X-IPAS-Result: =?us-ascii?q?A0AJAgDlnftXhqrcVdFbGgEBAQECAQEBAQgBAQEBFwEBBAE?= =?us-ascii?q?BCgEBglw1AQEBAQGBcKQ2iEaGV4UUgguGIAKCDzoSAQEBAQEBAQEBAQESAQEBC?= =?us-ascii?q?AsLCRkvQRKBXwQBFQEEghABAQEDARIuARsdAQMBCwYFBAcNLiMRAQUBHAYTIog?= =?us-ascii?q?TAQMPCKdIgTI+Mo0tgl8Fg2QKGScNU4J9AQEBAQEBBAEBAQEBAQEBAQEBFAMGE?= =?us-ascii?q?IgqgliHd4IvAQSBIQGYUwgBAYEmjleBboRngwaGGYxkE4I9MYERJQaDUCCBela?= =?us-ascii?q?FR4EHgUEBAQE?= X-IronPort-AV: E=Sophos;i="5.31,324,1473112800"; d="scan'208,217";a="240140333" Received: from mail-qk0-f170.google.com ([209.85.220.170]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 10 Oct 2016 16:00:34 +0200 Received: by mail-qk0-f170.google.com with SMTP id z190so99711508qkc.2; Mon, 10 Oct 2016 07:00:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:subject:from:in-reply-to:date:cc:message-id:references :to; bh=oyRLw8Nffqnf9xIA6+jpu+ezZLrE3tsE0WNg5Tg/DCQ=; b=ws/cmuM7uB7VK0tchjWV4NAHtQcY32M13yQI2vRm3of/Jex6GFfCdB7Yf7noYmzdSi LqHJW8H4IOwIL71+KDO3FZ9TcyplXTpYYcc4u8sLpZjP6IAnDbFKjTd+86b3t9SvfNXP OJuXqALEKOtvLDnJ+1jI4pHtl2JwYFY8YFYXOmWV5xsu/CFySua/IHbHr3Hp5zN6invi hlOJfTe78OEf/t4MoVqhKuLRw3a0MENDAXrv15MX2K6f3ZC472cFdJyic6ObadTN/xG2 3HJSkx9Dk8AppCx/npEFT3gnXLNbWDKZpqEnc2WiUQPvCY+TvlZ1NDxXvTpAg8Kx5x19 ivAA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:subject:from:in-reply-to:date:cc :message-id:references:to; bh=oyRLw8Nffqnf9xIA6+jpu+ezZLrE3tsE0WNg5Tg/DCQ=; b=jfYShMN5QyXeexrYE1Uuf9mefnR38h//yjRReX0/8SqzdZg91D7Logytss7oAU70/h z+cy3MAESibX4jstuTLzjNwPz/GLQe35qiwOe4xvnsElbrpohjbyjtd+V22vm+/UhVF1 gzgpMnNmf2cB7XTvKvrixoMZ61q5j4ksaUnr7rU7bB0Mj9RCidvK+fqhZRnJq7ets+bE sv3rdhCh6B2mMK7GXmU3BlZPjiTFRxXUSKM/Rr4ZvaR0ijKd4d5nlo7iZYtzsCUg6U+c KaPV/DOsLLT5zESInr5MgDtuYVJ4Pie+OTFXNOgOTtOt1DDnwMeJ/66ckGJe9oOJ7RAY 6/GA== X-Gm-Message-State: AA6/9Rlnx3ayE4mSPfyrgtS1+tc5LY0J1BImIJp15d3bA/nKcWKM9JmPTj6C2yaw+WasNQ== X-Received: by 10.55.167.149 with SMTP id q143mr29957525qke.97.1476108033732; Mon, 10 Oct 2016 07:00:33 -0700 (PDT) Received: from chans-imac.wv.cc.cmu.edu (Chans-iMac.wv.cc.cmu.edu. [128.237.221.111]) by smtp.gmail.com with ESMTPSA id s23sm11667875qka.10.2016.10.10.07.00.32 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Mon, 10 Oct 2016 07:00:32 -0700 (PDT) Content-Type: multipart/alternative; boundary="Apple-Mail=_5B9ABE83-BF29-4661-BC0F-5EA4E15F29D7" Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) From: Van Chan Ngo In-Reply-To: Date: Mon, 10 Oct 2016 10:00:24 -0400 Cc: caml-list@inria.fr, ocaml-jobs@inria.fr Message-Id: References: To: Arthur Breitman X-Mailer: Apple Mail (2.3124) Subject: Re: [Caml-list] Blockchains in OCaml --Apple-Mail=_5B9ABE83-BF29-4661-BC0F-5EA4E15F29D7 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii Hi Arthur, It is interesting to implement blockchains in functional language like OCam= l. I am happy to hear more about this project. FYI, a related work, we are in progress to formalize the Ethereum Virtual M= achine (EVM, the running environment of smart contracts) in Coq. Best, -Chan > On Oct 5, 2016, at 11:59 PM, Arthur Breitman wrote: >=20 > 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 fo= rmal verification, reach out as well! We'd be interested in proving the cor= rectness of some aspects of the protocol or sponsoring research in the fiel= d in general (within our modest means). >=20 --Apple-Mail=_5B9ABE83-BF29-4661-BC0F-5EA4E15F29D7 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=us-ascii Hi Arthur,

It is interesting to implem= ent 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 Virtua= l Machine (EVM, the running environment of smart contracts) in Coq.

Best,
-Chan


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

If you find this intrigu= ing 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 o= ut as well! We'd be interested in proving the correctness of some aspects o= f the protocol or sponsoring research in the field in general (within our m= odest means).


= --Apple-Mail=_5B9ABE83-BF29-4661-BC0F-5EA4E15F29D7--