[Caml-list] Attn: Development Editor, Latest OCaml Weekly News

[Alan Schmitt <alan.schmitt@polytechnique.org>]

[-- Attachment #1: Type: text/plain, Size: 9249 bytes --]

Hello

Here is the latest OCaml Weekly News, for the week of August 10 to 17,
2021.

Table of Contents
─────────────────

http-multipart-formdata v3.0.1 released
Call for participation: ML Family Workshop 2021
Coq-of-ocaml to translate OCaml to Coq
Old CWN


http-multipart-formdata v3.0.1 released
═══════════════════════════════════════

  Archive:
  <https://discuss.ocaml.org/t/ann-http-multipart-formdata-v3-0-1-released/8261/2>


Continuing the thread from last week, Hannes Mehnert asked
──────────────────────────────────────────────────────────

  Thanks for your work on that. I'm curious about the different
  "multipart" libraries now available for OCaml – anyone has a brief
  comparison of them?

  • [http-multipart-formdata] as announced above
  • [multipart_form] by @dinosaure
  • [multipart-form-data] by cryptosense

  Are there functional differences? Correctness? Performance? Or just a
  matter of style and co-development?


[http-multipart-formdata]
<https://github.com/lemaetech/http-multipart-formdata>

[multipart_form] <https://github.com/dinosaure/multipart_form/>

[multipart-form-data]
<https://github.com/cryptosense/multipart-form-data>


Bikal Lem replied
─────────────────

  One obvious difference among the three is `http-multipart-formdata'
  doesn't depend on any IO/Promise libraries, such as lwt or async. so
  you may find it easier to integrate in your project.

  `mulitpart-form-data' exposes a callback based streaming api, whereas
  http-multipart-formdata exposes a non-callback, non-blocking based API
  streaming api.

  The API surface of `http-multipart-formdata' is kept as low as
  possible, primarily 3 API calls - `boundary, reader' and `read' call.

  The dependency list of `http-multipart-formdata' is the thinnest. This
  may or may not be an issue depending on your aesthetics. However,
  relatively/comparatively the less your dependencies, the easier it is
  to integrate the lib with other OCaml libs and environments such as
  various OSes.


Bikal Lem added
───────────────

  I should also add `http-multipart-formdata' has been implemented with
  zero-copy streaming and minimal allocation in mind.


Call for participation: ML Family Workshop 2021
═══════════════════════════════════════════════

  Archive:
  <https://sympa.inria.fr/sympa/arc/caml-list/2021-08/msg00005.html>


Jonathan Protzenko announced
────────────────────────────

  We are happy to announce that the ML Family Workshop is back for its
  2021 edition, which we will be held online on Thursday August 26th, in
  conjunction with ICFP 2021. We invite you to subscribe to, and attend
  the workshop, in addition to the main ICFP conference.

  We are thrilled to announce that Don Syme will give this year's
  keynote: "Narratives and Lessons from The Early History of F#". Please
  join us!

  The program features 14 exciting submissions, including 4 short talks.
  The workshop will be held online in the 6pm-3am time band (Seoul
  Time).  Talks will be pre-recorded and uploaded online for those who
  cannot attend.

  • Program:
    <https://icfp21.sigplan.org/home/mlfamilyworkshop-2021#program>
  • Keynote:
    <https://icfp21.sigplan.org/details/mlfamilyworkshop-2021-papers/15/Keynote-Narratives-and-Lessons-from-The-Early-History-of-F>-
  • ICFP home: <http://icfp21.sigplan.org/home>


Program committee
╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌

  • Danel Ahman (University of Ljubljana)
  • Robert Atkey (University of Strathclyde)
  • Frédéric Bour (Tarides)
  • Ezgi Çiçek (Facebook London)
  • Youyou Cong (Tokyo Institute of Technology)
  • Richard A. Eisenberg (Tweag I/O)
  • Martin Elsman (University of Copenhagen, Denmark)
  • Ohad Kammar (University of Edinburgh)
  • Naoki Kobayashi (University of Tokyo, Japan)
  • Benoît Montagu (Inria)
  • Jonathan Protzenko (Microsoft Research) (Chair)
  • Kristina Sojakova (INRIA Paris)
  • Don Syme (Microsoft)
  • Matías Toro (University of Chile)
  • Katsuhiro Ueno (Tohoku University)


Coq-of-ocaml to translate OCaml to Coq
══════════════════════════════════════

  Archive:
  <https://discuss.ocaml.org/t/coq-of-ocaml-to-translate-ocaml-to-coq/8288/1>


Guillaume Claret announced
──────────────────────────

  I am pleased to present the [coq-of-ocaml] project, to translate a
  subset of OCaml to the [Coq] proof assistant. The aim is to do formal
  verification on OCaml programs. The idea is to generate a Coq
  translation as close as possible to the original code in terms of
  intent but using the Coq syntax. As a short example, if we take the
  following OCaml code and run `coq-of-ocaml':
  ┌────
  │ type 'a tree =
  │ | Leaf of 'a
  │ | Node of 'a tree * 'a tree
  │ 
  │ let rec sum tree =
  │   match tree with
  │   | Leaf n -> n
  │   | Node (tree1, tree2) -> sum tree1 + sum tree2
  └────
  we get the following Coq file:
  ┌────
  │ Require Import CoqOfOCaml.CoqOfOCaml.
  │ Require Import CoqOfOCaml.Settings.
  │ 
  │ Inductive tree (a : Set) : Set :=
  │ | Leaf : a -> tree a
  │ | Node : tree a -> tree a -> tree a.
  │ 
  │ Arguments Leaf {_}.
  │ Arguments Node {_}.
  │ 
  │ Fixpoint sum (tree : tree int) : int :=
  │   match tree with
  │   | Leaf n => n
  │   | Node tree1 tree2 => Z.add (sum tree1) (sum tree2)
  │   end.
  └────

  We support the following OCaml features:
  • the core of OCaml (functions, let bindings, pattern-matching,…)
  • type definitions (records, inductive types, synonyms, mutual types)
  • monadic programs
  • modules as namespaces
  • modules as polymorphic records (signatures, functors, first-class
    modules)
  • multiple-file projects (thanks to Merlin)
  • both `.ml' and `.mli' files
  • existential types (we use impredicative sets option in Coq)

  We also have some support for the GADTs, the polymorphic variants, and
  the extensible types.  We are in particular working on having an
  axiom-free translation of the GADTs to Coq. We do not support:
  • side-effects outside of a monad (references, exceptions, …);
  • object-oriented programming;
  • various combinations of OCaml features for which `coq-of-ocaml'
    should generate a warning.

  Our main example and use case is the [coq-tezos-of-ocaml]
  project. This contains a translation of most of the [economic
  protocol] of the [Tezos] blockchain (around 30.000 lines of OCaml
  translated to 40.000 lines of Coq). For example, we verify the
  comparison functions defined in
  [src/proto_alpha/lib_protocol/script_comparable.ml] with
  [src/Proto_alpha/Proofs/Script_comparable.v].

  We are looking for the application to other projects too.

  We think the best way to use `coq-of-ocaml' is to continue developing
  in OCaml and run `coq-of-ocaml' to keep a synchronized translation in
  Coq. Having a working Coq translation (as compiling in Coq) forces us
  to avoid some OCaml constructs. We believe these constructs would
  probably be hard to verify anyway. Then, on the Coq side, we can
  verify some important or easy to catch properties. If there is a
  regression in the OCaml code, re-running `coq-of-ocaml' should make
  the proofs break.


[coq-of-ocaml] <https://clarus.github.io/coq-of-ocaml/>

[Coq] <https://coq.inria.fr/>

[coq-tezos-of-ocaml]
<https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/>

[economic protocol]
<https://gitlab.com/tezos/tezos/-/tree/master/src/proto_alpha/lib_protocol>

[Tezos] <https://tezos.com/>

[src/proto_alpha/lib_protocol/script_comparable.ml]
<https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/script_comparable.ml>

[src/Proto_alpha/Proofs/Script_comparable.v]
<https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/script_comparable>


Old CWN
═══════

  If you happen to miss a CWN, you can [send me a message] and I'll mail
  it to you, or go take a look at [the archive] or the [RSS feed of the
  archives].

  If you also wish to receive it every week by mail, you may subscribe
  [online].

  [Alan Schmitt]


[send me a message] <mailto:alan.schmitt@polytechnique.org>

[the archive] <https://alan.petitepomme.net/cwn/>

[RSS feed of the archives] <https://alan.petitepomme.net/cwn/cwn.rss>

[online] <http://lists.idyll.org/listinfo/caml-news-weekly/>

[Alan Schmitt] <https://alan.petitepomme.net/>


[-- Attachment #2: Type: text/html, Size: 20527 bytes --]