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.



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. 

A review of Nomadic Labs in 2020

Nomadic Labs’ activities in 2020

2020 is over and in spite of the difficulties which the year presented, we at Nomadic Labs got a lot done. So here’s who we are, and what we accomplished in 2020: Nomadic Labs in a nutshell Nomadic Labs is an international technical company dedicated to evolving the Tezos ecosystem. Tezos is a community-driven proof-of-stake self-evolving blockchain platform that adapts and adopts new features and enables borderless global cooperation. Let’s unpack that: Community-driven: The Tezos community is a...

Read More
Introducing mockup mode for tezos-client

Presenting tezos-client’s new mockup mode feature

We are pleased to announce that the tezos-client binary has a new feature aimed at contract and tool developers alike: the mockup mode. Mockup mode allows easy prototyping of Tezos applications and smart contracts locally. By local we mean: The relevant data files sit in a directory on your computer’s local filesystem. These files are a lightweight emulation of the internal state of a Tezos single-node network. Thus, networking communications infrastructure that a node would be wrapped...

Read More
Announcing the Edo Release!

This is a joint announcement from Nomadic Labs, Marigold, and Metastate. A couple of weeks ago, we were proud to see the “Delphi” upgrade to the Tezos protocol go live. This week, we are proud to announce our latest protocol upgrade proposal, “Edo”. As usual, Edo’s true name is its hash, which is PtEdoTezd3RHSC31mpxxo1npxFjoWWcFgQtxapi51Z8TLu6v6Uq. Why is Edo being proposed when Delphi has only been in place for a short while? Although Delphi went live on November 12th,...

Read More
Announcing Ebetanet, the Edo Preview Network!

We have just spawned a test network for a beta version of the Edo protocol, which we plan to propose as the next (008) Tezos protocol upgrade. The code running on the test network is our release candidate for Edo. We anticipate that the beta period will last only one to two weeks before our proposal is final. Please participate by testing it now! We plan to replace this test network with Edonet, the successor of Delphinet, once we...

Read More
Cortez End of Support

In a context where Nomadic Labs aims to concentrate on its high value activities, we plan to refocus our efforts on projects and tools that are directly related to the heart of Tezos and its economic protocol. As a result, Nomadic Labs decided to discontinue its support and maintenance of both the Android and iOS versions of the Tezos mobile wallet, Cortez. After a grace period running from now to 15 February 2021, Nomadic Labs will no longer...

Read More
Smarter contracts thanks to Delphi (part 1/2)

Delphi is the successor to the Carthage protocol. Delphi’s main difference from Carthage is that gas costs are lower, so that smart contracts can compute more before hitting the Delphi/Carthage per-operation gas limit of 1,040,000 gas units (gu). In this post we quantify the difference that Delphi’s lower gas costs will make: We start with a description and justification of the Michelson gas model; and then we showcase the expected gains for some smart contracts chosen to illustrate the...

Read More
Delphi, the Latest Tezos upgrade, is live!

This is a joint post from Nomadic Labs, Metastate and Marigold. We’re very happy to announce that the vote on the “Delphi” upgrade to the Tezos network passed a few hours ago (around 13:00 GMT on 12 November 2020.) The upgrade went live immediately afterwards at block 1,212,417. An informal blog post describing Delphi is here, and a changelog of everything that went into Delphi is here. Most prominently, Delphi makes substantial improvements to the...

Read More
The case of mixed forks in Emmy+

Note: This analysis was done with the help of Bruno Blanchet (Inria). The interested reader can experiment with our code used in the analysis. As in the previous analysis, we do not present any security proofs. This is the fourth in a series of posts on Emmy+: After our initial analysis, recently revisited and extended to the partial synchronous network model, we now consider so-called “mixed forks”. So far, we assumed that malicious bakers wanted to undo a transaction. In this post, we consider instead...

Read More
Regular Scheduling For Our Tezos Proposals

The teams at Nomadic Labs, Metastate, Marigold, and DaiLambda have participated in a number of joint protocol proposals for Tezos; some of us have been working on the code since the original launch of the Tezos network, and have been involved with updates from Athens through the recent Delphi proposal. Over time, we have gained more and more experience and have learned what practices seem to work best for updates to the...

Read More