A POPL 2022 Retrospective

A few weeks ago, we physically attended POPL 2022 — the 49th ACM SIGPLAN Symposium on Principles of Programming Languages — which took place in Philadelphia, PA and also virtually everywhere on Earth via Airmeet.

POPL is a¹ premier annual conference event of the programming languages research community showcasing, together with several colocated events, the latest cutting edge results in programming languages, especially in functional programming and formal verification. The latter topics are very dear to the Tezos community, as they enable us to build safety-critical, complex-yet-beautiful software — such as the Tezos protocol and the Octez suite — on sound technical foundations. Moreover, research presented in conferences like POPL have immediate impact on our daily work at Nomadic Labs.

This affinity is reflected in our continuous involvement as sponsors:

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

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

After almost two years of virtual events, and debugging audio and video connections across different virtualization platforms, we were eager to return to in-person POPL-ing² and real-life hallway tracks. Our on-site team consisted of: Michel Mauny, Nomadic Labs’ CEO; Germán Delbianco, Research Engineer at Nomadic Labs; and Michael Holey, Blokhaus’ community manager³. They were present throughout the week at the Tezos booth, eager and ready to answer questions about Tezos. It was an amazing opportunity to promote our interest in these research fields, and also to advertise possible collaborations, openings in the Tezos ecosystem and at Nomadic Labs, as well as research funding opportunities.

We are happy to have had the chance to catch up with the PL community, and we hope that we have planted the seeds for fruitful collaborations which will benefit the Tezos community. There was also plenty of interesting, high-quality talks, and below we bring you a few (biased) highlights of this year’s program⁴.

The POPL Program and our Highlights

Each year, the ACM SIGPLAN Symposium on Programming Languages — POPL in short — features novel research contributions ranging from theoretical foundations of programming languages (e.g. semantics and type systems), to the development and application of formal tools for crafting, and verifying, reliable and correct systems.

Among the other colocated events on offer during the week (like VMCAI, or LAFI), we took time to attend CPP 2022 and CoqPL 2022.

The full program is available here, and several events, including the main conference, have made the talks available on SIGPLAN’s YouTube channel.

POPL 2022

This year the POPL program consisted of 60+ accepted papers, in addition to 3 keynotes, and a special session of TOPLAS articles. There was plenty of high-quality research catering to different tastes and appetites. An incomplete list of those we enjoyed⁵:

• Alfred Aho’s keynote, “Principles of Programming Language Translators” focused on the topic of computational thinking, and how it applies to compiler design. In particular, it revisited what an abstraction is, from a programming language perspective: we should define an abstraction as a model and a set of operations for manipulating data (the “programming language” of the data model). The talk focused on a taxonomy of four abstractions for computer science: fundamental abstractions, abstract implementation, and declarative and computational abstractions; and illustrated with examples from compiler design. Towards the end, and moving away from compilers, Professor Aho focused on quantum computing, and argued that the four postulates of quantum mechanics⁶ define new kinds of abstractions that extend the previously presented classical ones.

• “Concurrent Incorrectness Separation Logic”. Incorrectness separation logic has recently been introduced as a dual to separation logic, whose goal is not to establish the correctness of programs, but rather prove the presence of bugs, by catching them, based on under-approximated reasoning. This work extends the logic to a parametric framework to a concurrent, shared memory model, which can be instantiated to soundly assess whether races, deadlocks, and memory safety errors detected are true positives — where “sound” means that all results are true positives.

• “The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency”. This talk featured a retrospective of 20 years of research in memory models, looking into how to support sequential composition while targeting modern hardware architectures, following an event-based approach with preconditions and families of predicate transformers.

• Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations. This talks presents Simuliris, a simulation technique to establish termination preservation for a range of concurrent program transformations that exploit undefined behavior in the source language. The key idea is using ownership to reason modularly about compiler assumptions about well-defined behavior. Based on the Iris framework.

• “Pirouette: Higher Order Typed Functional Choreographies”. Pirouette is a programming language for typed higher-order functional distributed choreography. Pirouette offers programmers the ability to write a centralized functional program and compile it into programs for each node in a distributed system. The paper provides in particular a formalization in Coq, notably showing that the soundness of the type-system entails deadlock-freedom.

• Last, we want to highlight an effort on smart contract verification: “SolType: Refinement Types for Solidity”. This work presents a refinement type system for Solidity that can be used to prevent arithmetic over- and under-flows in Ethereum smart contracts.

This year, POPL also featured a virtual post-conference workshop event, across multiple time zones. In addition to a few select invited speakers, the novelty this year was a couple of speed-dating sessions where industrial sponsors (like us) could connect with potential candidates.

All presentations are available on a dedicated YouTube playlist.

CPP 2022

As mentioned above, Nomadic Labs were proud sponsors of CPP 2022, the 8th Conference on Certified Programs and Proofs. This conference covers a broad spectrum of mechanized verification efforts and tools, ranging from the formalization of mathematics and certified algorithms to new proof techniques, frameworks and tooling for interactive theorem proving.

This year, we highlight two very interesting keynotes that resonate with our own verification endeavors at Nomadic Labs:

• Professor Andrew Appel’s keynote, on “Coq’s vibrant ecosystem for verification engineering” addressed the engineering aspects of building vertical stacks consisting of verified software components, centered around the VST project, and how to scale up verification efforts by relying on community libraries and community-centric projects like the Coq platform. In particular he focused on how to address the verification gap across multiple layers of formalization efforts and mechanized software. The issue of the verification gap, that is the semantic distance between verification artifacts and real-world production code, is one of the big hurdles of industrial scale projects like ours — and it has for instance been at the center of different recent projects and internships in house.

• June Andronick’s keynote, “The seL4 verification: the art and craft of proof and the reality of commercial support”, consisted of two parts. The first one was a tour de force of the seL4 project, discussing in general the scalability of large verification stacks, and in particular the challenges of the project. The second part focused on the broader picture of carrying out large scale verification projects in industrial settings. She focused on both technical proof-engineering aspects; as well as non-technical ones, like how to properly explain the virtues of formal verification to non-technical audiences. That rings a bell!

Other talks we enjoyed were:

• “Specification and Verification of a Transient-Stack”, a very cool verification effort using CFML and time credits in Coq to certify concurrent and persistent data structures.

• “Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library”, presents the formal specification and verification in the Iris framework of a high-performance, fine-grained concurrent multi-producer multi-consumer queue from Meta’s folly library.

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

• “A verified algebraic representation of Cairo program execution”, which focuses on how to verify STARKs in the LEAN theorem prover. StarkNet’s STARKs constitute the core of a Zero Knowledge-based Layer 2 solution for Ethereum — but eventually scalable to other blockchains — whose aim is to translate EVM bytecode into simple, low level Cairo programs.

• “Formal Verification of a Distributed Dynamic Reconfiguration Protocol”, presenting the specification and formal verification using TLA+ of the core MongoRaftReconfig reconfiguration protocol, implemented in the MongoDB distributed database.

All CPP 2022 presentations are available on ACM SIGPLAN’s YouTube channel playlist.

CoqPL 2022

On the last day of the conference, we attended CoqPL 2022, the Eighth International Workshop on Coq for Programming Languages. The Coq proof assistant is one of Nomadic Labs’ favorite verification tools, as witnessed by the Mi-Cho-Coq framework, the coq-of-ocaml project — and also, various internship projects on offer. Moreover, the Tezos Foundation supports the development of Coq and of its ecosystem (see here how to apply for support), 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!

It was a great experience for us to be back at POPL, and the hybrid format allowed us to reach out and interact better with the community.

POPL turns 50 next year, and it will again be a hybrid event, with the physical event taking place somewhere in the United States’ West Coast⁷. We look forwards to seeing you there for this special occasion — both in person and online!