Nomadic Labs
Nomadic Labs

POPL 2021 retrospective

A short summary of our experience at POPL, CPP and CoqPL this year.

About POPL (Symposium on Principles of Programming Languages)

POPL 2021 — the 48th ACM SIGPLAN Symposium on Principles of Programming Languages — is a premier annual conference event of the Programming Languages research community. POPL consists of a main conference, and many colocated events, which together present the latest and greatest research in (amongst other topics):

  • programming languages theory,
  • formal verification,
  • type systems, and
  • functional programming

— all subjects which are dear to Tezos community, and which are the bread-and-butter of the daily work at Nomadic Labs of writing some of the most complex and safety-critical code in commercial practice.

POPL took place from 17th to 22nd January 2021. It was supposed to be in Copenhagen Denmark, but due to the pandemic it was virtualised with a semi-synchronous program catering for multiple time zones. See the full symposium events page online and the schedule.

Our contributions

Nomadic Labs was actively involved throughout the week:

We were also pleased to find further research works backed by Tezos Foundation grants in the programs: Xuanrui Qi and Jacques Garrigue from Nagoya University, in Japan, presented advances towards specifying OCaml GADTs in Coq, a work funded through the Certifiable OCaml Type Inference (COCTI) grant1.

Sponsorship

Highlights

Here are our selected highlights2:

POPL 2021

The POPL program ranges from theoretical foundations of programming languages (e.g. semantics and type systems), to the development and application of formal tools and techniques for creating and verifying reliable and correct systems.

Selected examples include:

Reliable blockchains and other distributed systems were the focus for two POPL21 invited keynotes:

CPP 2021 (Conference on Certified Programs and Proofs)

As mentioned above, we sponsored CPP 2021 (Conference on Certified Programs and Proofs). This covers mechanised verification efforts and tools, including:

  • the formalisation of mathematics,
  • certified algorithms, and
  • the development of new proof techniques and frameworks for certified programming.

A highlight of this year’s program was the keynote talk by Peter Sewell (University of Cambridge) accounting past, present, and future formalisation efforts towards formally specified, mechanised hardware architectures in the context of the CHERI project, and their impact on the development of existing and future hardware architectures.

Blockchain-related topics like certified frameworks for programming correct smart contracts, or mechanised proofs of consensus algorithms, frequently appear in the program. This year, presentations included:

  • advances in the ConCert framework to verify, test, and extract certified smart contracts in Coq (including extraction to Liquidity and plans to target CameLIGO in the future);
  • ongoing efforts to certify Tendermint using TLA+;
  • and our own lightning-talk presentation on the verification of the Dexter contract.

CoqPL 2021 (Seventh International Workshop on Coq for Programming Languages)

Amongst the other colocated events on offer during the week (like VMCAI, or LAFI), we took time to attend CoqPL 2021, the Seventh International Workshop on Coq for Programming Languages.

The Coq proof assistant is one of Nomadic Labs’ most-used verification tools, as witnessed by the Mi-Cho-Coq framework, the coq-of-ocaml project, and its use on this contributions to this year’s CPP and on this contributions to this year’s POPL.

The Tezos Foundation supports the development of Coq and of its ecosystem, and the CoqPL workshop provides an opportunity to interact with the Coq development team, learn about the recently released features and what’s coming next in the pipeline, and other recent library developments.

See you next year!

POPL 2022 is planned for Philadelphia, PA. We look forward to catching up with you all again there — hopefully, in person.


  1. You can find the COCTI code here

  2. At time of writing, the entire program is publicly available on Clowdr and should soon be uploaded to SIGPLAN’s YouTube channel

  3. Arvid Jakobsson, Colin González, Bruno Bernardo, and Raphaël Cauderlier. Formally Verified Decentralized Exchange with Mi-Cho-Coq. Contributed Lightning Talk to CPP 2021. Thanks also to Kristina Sojakova (INRIA) for her contributions to the formalisation effort. 

  4. František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas. On Algebraic Abstractions for Concurrent Separation Logics. Proc. ACM Program. Lang. 5, POPL, Article 5 (January 2021), 32 pages. https://doi.org/10.1145/3434286