*** Call for Participation ***
*** Certified Programs and Proofs (CPP 2022) ***
- Early registration deadline: 3 January 2022
- Getting a visa: https://popl22.sigplan.org/attending/visa-information
- Registration: https://popl22.sigplan.org/attending/registration
- Further reduced student participation fee: see below
- Accommodation: https://popl22.sigplan.org/venue/POPL-2022-venue
Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education.
CPP 2022 (https://popl22.sigplan.org/home/CPP-2022) will be held on 17-18 January 2022 and will be co-located with POPL 2022. CPP 2022 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG, and supported by a diverse set of industrial sponsors.
Similarly to other events collocated with POPL 2022, CPP will take place as an in-person event at the Westin Philadelphia (99 South 17th Street at Liberty Place, 19103 Philadelphia), and will require attendees to provide proof of vaccination (details will be available soon). Authors who are unable to attend CPP in person will be able to present remotely. All talks will be recorded, and all recordings will be available either as a livestream or soon afterwards.
For more information about this edition and the CPP series, please visit https://popl22.sigplan.org/home/CPP-2022
### Invited talks
* June Andronick (UNSW Sydney). The seL4 verification: the art and craft of proof and the reality of commercial support
* Andrew W. Appel (Princeton). Coq's vibrant ecosystem for verification engineering
* Cesar Munoz (Currently at AWS, Formerly at NASA, USA). Structural Embeddings Revisited
### Accepted papers
The list of accepted papers is available at
https://popl22.sigplan.org/home/CPP-2022#event-overview
### Subsidized student registration
To facilitate in-person participation of undergraduate and graduate students who require financial assistance, CPP 2022 offers the opportunity to register at a special reduced rate, determined on a case-by-case basis, and implemented using a special-purpose registration code on POPL's registration website. Students wishing to apply for such support may do so by sending mail to the CPP conference co-chairs (Beringer and Krebbers, see below for their email) preferably by December 24, 2021, with a brief description of their situation. Notifications will be sent out at most one week later; hence, students who cannot be supported will still have the opportunity to register at the publicly available reduced rate, which is available until January 3rd. Applications arriving after December 24th will be considered only in exceptional cases. Students who already receive registration support for PLMW or are supported by SIGPLAN PAC are not eligible.
CPP's student support is made possible by to our generous industrial supporters:
https://popl22.sigplan.org/home/CPP-2022
### Contact
For any questions please contact the chairs:
Andrei Popescu <a.popescu@sheffield.ac.uk> (PC co-chair)
Steve Zdancewic <stevez@seas.upenn.edu> (PC co-chair)
Lennart Beringer <eberinge@cs.princeton.edu> (conference co-chair)
Robbert Krebbers <mail@robbertkrebbers.nl> (conference co-chair)
OCaml Weekly News
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
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?
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
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 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
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
.mland.mlifiles - 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-ocamlshould 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.
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.