POPL 2021 retrospective

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:

• On Monday 18 Jan, Arvid Jakobsson, one of our experts in formal verification of smart contracts, presented the formalisation of the Dexter decentralised exchange contract in the Mi-Cho-Coq framework. at CPP’s 2021 Lightning Talks session³.

• On Wednesday 20 Jan, Michel Mauny, Nomadic Labs’ CEO, made a short presentation of our company at POPL’s Sponsor Reception, which also featured a contributed video presenting a general overview of Tezos by Arthur Breitman.

• On Friday 22 Jan, Germán Delbianco, one of our software verification experts, together with our collaborators from IMDEA Software Institute and UCM, presented an article presenting new developments on the algebraic foundations of Concurrent Separation logics. at POPL⁴.

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) grant¹.

Sponsorship

• The Tezos Foundation was a platinum sponsor of POPL 2021, for the third consecutive year.

• We at Nomadic Labs are pleased and proud to have sponsored the colocated CPP 2021 (Conference on Certified Programs and Proofs), for the second consecutive year.

Highlights

Here are our selected highlights²:

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:

• formalised optimisations for quantum circuits;
• programming with and reasoning about algebraic effects;
• formal verification of shared memory concurrency and probabilistic programs; and
• how to make cryptographic primitives secure under speculative executions.

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

• Rachid Guerraoui (EPFL) on The road to a Universal Internet Machine (Demystifying Blockchain Protocols) and
• Joe Hellerstein (UC Berkeley) on Toward a Programmable Cloud: CALM Foundations and Open Challenges.

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.