173 views
A Nomad's notes from POPL 2022 ============================ :mega: :octopus: Your friendly [POPL 2022](https://popl22.sigplan.org/) correspondent here, broadcasting live from the [city of brotherly love](https://philadelphiaencyclopedia.org/archive/city-of-brotherly-love/). I'll be keeping notes and highlights here from the conferences here throughout the week. My path will start with [CPP](https://popl22.sigplan.org/home/CPP-2022), continue with a linearization of POPL parallel sessions and finalize with [CoqPL](https://popl22.sigplan.org/home/CoqPL-2022) on Saturday. :pray: If you are attending _remotely_ this _hybrid_ event, fill free to chip in reading notes and reading suggestions from other parallel events. ## CPP 2022 The [Certified Programs and Proofs (CPP)](https://popl22.sigplan.org/home/CPP-2022) is an international conference focusing on practical and theoretical works on formal verification, notably on mechanization efforts. Proudly sponsored by Nomadic Labs, for the 3rd consecutive year. Open Access proceedings [are available here](https://dl.acm.org/doi/proceedings/10.1145/3497775), The remote talks are already available on the conference site, as they were pre-recorded. Everything ~~will be eventually made~~ **edit:is** freely available on [YouTube here](https://www.youtube.com/playlist?list=PLyrlk8Xaylp7peYx_GED0Ny3q-gf3fZYC). ### Monday Morning Several very interesting talks on the first morning of CPP -- heavy use of separation logic, so this correspondent is particularly happy. #### Keynote - [Coq's vibrant ecosystem for-verification engineering:](https://popl22.sigplan.org/details/CPP-2022-papers/25/Coq-s-vibrant-ecosystem-for-verification-engineering) starting out with a bang, with an invited keynote by Andrew Appel, speaking about addressing multiple verification gaps in vertical mechanization stacks. Also discussed where the Coq platform and how to scale up verification efforts by relying on community libraries -- centered around VST. The organizers promised it will be soon on YouTube for everybody to enjoy. Make sure you catch it up later! In the meantime, here is the [EA](https://dl.acm.org/doi/10.1145/3497775.3503951). #### Semantics and Program Verification - [Specification and Verification of a Transient-Stack:](https://popl22.sigplan.org/details/CPP-2022-papers/22/Specification-and-Verification-of-a-Transient-Stack) a very cool verification effort by well known usual suspects, using CFML and Time Credits in Coq to certify transient memory data structures. - [Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library:](https://popl22.sigplan.org/details/CPP-2022-papers/16/Mechanized-Verification-of-a-Fine-Grained-Concurrent-Queue-from-Meta-s-Folly-Library) Reloc/Iris proof for a fancy concurrent queue from Meta. - [Applying Formal Verification to Microkernel IPC at Meta:](https://popl22.sigplan.org/details/CPP-2022-papers/8/Applying-Formal-Verification-to-Microkernel-IPC-at-Meta) tl;dr Meta (the ~~artist~~ company formerly known as Facebook) actually uses Iris in house for some verification projects. - [Certified Abstract Machines for Skeletal Semantics:](https://popl22.sigplan.org/details/CPP-2022-papers/9/Certified-Abstract-Machines-for-Skeletal-Semantics) for the abstract machine geeks out there, certified skeletal semantics extracted from Coq to OCaml. ## Mon Afternoon Two blocks of talks on a long afternoon, finalizing with another keynote by [June Andronick](https://proofcraft.systems/#june) broadcast live from Down Under. ### Semantics and Program Verification - [A Compositional Proof Framework for FRETish Requirements:](https://popl22.sigplan.org/details/CPP-2022-papers/3/A-Compositional-Proof-Framework-for-FRETish-Requirements) this paper presents a rigorous formalization of the [Fretish](https://fretish.com/) language, in the Prototype Verification System (PVS) theorem prover. - [Verbatim++ Verified Optimized and Semantically Rich Lexing with Derivatives:](https://popl22.sigplan.org/details/CPP-2022-papers/24/Verbatim-Verified-Optimized-and-Semantically-Rich-Lexing-with-Derivatives) this works presents a Coq formalization of extensions to the [Verbatim](https://ieeexplore.ieee.org/document/9474322) optimizing lexers. - [Formally Verified Superblock Scheduling.](https://popl22.sigplan.org/details/CPP-2022-papers/13/Formally-Verified-Superblock-Scheduling) This work presents a certified scheduling compiler that operates over [_superblocks_](https://www.hpl.hp.com/techreports/92/HPL 92 78.pdf), integrated within the [CompCert](https://compcert.org/) C compiler, providing a complete machine checked proof of semantic preservation from C to assembly. - [Overcoming Restraint: Composing Verification of Foreign Functions with Cogent.](https://popl22.sigplan.org/details/CPP-2022-papers/18/Overcoming-Restraint-Composing-Verification-of-Foreign-Functions-with-Cogent) Cogent is a purposed built functional language aimed at building verified systems, with interesting features, e.g., a type system based on _strict_ uniqueness types. To interface with the wild world of system plumbing, Cogent provides a foreign function interface (FFI) to C code. This work presents advances in formally asserting that the proven invariants in Cogent, are preserved in the presence of the unsafe FFI code. ### Security and Distributed Systems - [Reflection Rewinding and Coin Toss in EasyCrypt](https://popl22.sigplan.org/details/CPP-2022-papers/19/Reflection-Rewinding-and-Coin-Toss-in-EasyCrypt) - [A verified algebraic representation of Cairo program execution](https://popl22.sigplan.org/details/CPP-2022-papers/6/A-verified-algebraic-representation-of-Cairo-program-execution) verifiable cryptographic STARKs in LEAN. Layer 2 solution for Ethereum but eventually scalable to other blockchains. Aim: make EVM translate into simple Cairo programs. This project targets the formalization of Cairo program executions, encoded as traces. - [Formal Verification of a Distributed Dynamic Reconfiguration Protocol](https://popl22.sigplan.org/details/CPP-2022-papers/11/Formal-Verification-of-a-Distributed-Dynamic-Reconfiguration-Protocol) TLA+ spec of MongoRaft distributed systems + some safety properties (3 invariants and several aux theorems) - [Forward build systems formally](https://popl22.sigplan.org/details/CPP-2022-papers/14/Forward-build-systems-formally) Formally verified forward build systems in Agda. Defining what is the correctness, identifying hazards, building a model in Agda, to target both [Rattle](https://hackage.haskell.org/package/rattle), a Haskell DSL for forward builds, and [Fabricate](https://github.com/brushtechnology/fabricate), which inspired the former. Partial correctness of speculative Rattle. Based on reasoning on execution traces. #### Remote Keynote - [The seL4 verification: the art and craft of proof and the reality of commercial support](https://popl22.sigplan.org/details/CPP-2022-papers/27/The-seL4-verification-the-art-and-craft-of-proof-and-the-reality-of-commercial-suppo) The day ended how it started, discussing scalability of large vertical verification stacks. This time the focus was on the formalization of the [SeL4](https://sel4.systems/) micro-kernel. June's keynote was split on two parts. The first one was a _tour de force_ through the formalization, discussing the moving pieces of such large mechanization efforts, and discussing the interesting properties when modeling the correctness of a micro-kernel, such as _availability_, and _integrity_ for kernel calls. The second part though, focused on the challenges of doing large scale mechanization in an industrial settings. She focused both on both technical _proof-engineering_ aspects, as well as _non-technical_ ones like how to leverage with customer demands and expectations. Also, and perhaps more importantly, how to _properly_ explain the virtues of formal verification to non-technical folks. ## Tuesday Morning The morning session started with on a keynote presentation by Cesar Muñoz (AWS, formerly at NASA), and a session dedicated to _proof engineering_ and tooling. ### Keynote - [Structural Embeddings Revisited:](https://popl22.sigplan.org/details/CPP-2022-papers/26/Structural-Embeddings-Revisited) Cesar Muñoz's keynote presented an overview on his long experience with _applied_ verification projects at NASA, highlighting different PVS formalization efforts -- mostly targeting algorithm written in FORTRAN, NASA likes FORTRAN a lot. Moreover, his presentation discussed the pragmatic of engineering formalization stacks via structural embeddings. For example, the choice between _hybrid_ and _foundational_, or bottom-up, approaches to formal verification. ### Proof Infrastructure, Rewriting and Automated Reasoning - [CertiStr A Certified String Solver.](https://popl22.sigplan.org/details/CPP-2022-papers/10/CertiStr-A-Certified-String-Solver) - [Safe Fast Concurrent Proof Checking for the lambda Pi Calculus Modulo Rewriting:](https://popl22.sigplan.org/details/CPP-2022-papers/20/Safe-Fast-Concurrent-Proof-Checking-for-the-lambda-Pi-Calculus-Modulo-Rewriting) this works presents Kontroli, a memory- and thread-safe, concurrent, proof checker for the lambda-Pi calculus modulo rewriting, written in Rust, and inspired by Dedukti. - [An Extension of the Framework Types To Sets for Isabelle HOL](https://popl22.sigplan.org/details/CPP-2022-papers/7/An-Extension-of-the-Framework-Types-To-Sets-for-Isabelle-HOL) - [A Drag and Drop Proof Tactic](https://popl22.sigplan.org/details/CPP-2022-papers/4/A-Drag-and-Drop-Proof-Tactic) ## Tuesday Afternoon ### Formalization of Logic, Algebra and Geometry The first block of the afternoon presents theoretical results in the formalization of different logics in proof assistant. - [Semantic cut elimination for the logic of bunched implications formalized in Coq:](https://popl22.sigplan.org/details/CPP-2022-papers/21/Semantic-cut-elimination-for-the-logic-of-bunched-implications-formalized-in-Coq) this *distinguished article* presents a Coq formalization of the _cut elimination_ rule for the logic of Bunched Implication -- which lies at the foundation of (Concurrent) Separation Logics. - [Undecidability Incompleteness and Completeness of Second Order Logic in Coq:](https://popl22.sigplan.org/details/CPP-2022-papers/23/Undecidability-Incompleteness-and-Completeness-of-Second-Order-Logic-in-Coq) a really interesting work focusing on the mechanization of known properties of [Second Order Logic (SOL)](https://plato.stanford.edu/entries/logic-higher-order), notably _Undecidability_ and _completeness_, and connecting back to the early beginnings of the formalization of mathematics and [ Hbert's work](https://en.wikipedia.org/wiki/Hilbert%27s_tenth_problem). It builds upon earlier mechanization works, e.g., for [first-order logic (FOL)](https://en.wikipedia.org/wiki/First-order_logic). Real question that actually happened during Q&A, coming from a serious, respected pillar of the community: _Have you cited anybody who's actual still alive?_ Banter question I didn't dare to ask: Would Hilbert be a Coq guy or Lean guy? This correspondent says he'd be leading the Coq dev team. - [Formalising Lie algebras:](https://popl22.sigplan.org/details/CPP-2022-papers/12/Formalising-Lie-algebras) speaking of Lean - this talk presents a formalization of Lie algebras in Mathlib, and some examples on where these arise in math and physics. - [A Machine Checked Direct Proof of the Steiner-Lehmus Theorem](https://popl22.sigplan.org/details/CPP-2022-papers/5/A-Machine-Checked-Direct-Proof-of-the-Steiner-Lehmus-Theorem): or, how to build on the mechanization of _classical_ results in [NuPRL](http://www.nuprl.org/) back [Euclid's Element of Geometry](https://en.wikipedia.org/wiki/Euclid%27s_Elements), to derive a first direct, _constructive_ proof of the [Steiner-Lehmus Theorem](https://en.wikipedia.org/wiki/Steiner%E2%80%93Lehmus_theorem), a result in geometry which was eluding geometry folks since 1844! #### Category Theory, HoTT, Number Theory The last session of CPP continued on a similar theme, presenting more formalization results in Category Theory and Homotopy Type Theory. - [Implementing a category theoretic framework for typed abstract syntax:](https://popl22.sigplan.org/details/CPP-2022-papers/15/Implementing-a-category-theoretic-framework-for-typed-abstract-syntax) a deep formalization effort on the algebraic structure behind (typed) abstract syntax based on the UniMath Coq framework. Building on several thousand lines of Coq proofs formalizing results on _bi-categories_, _endofunctors_ on them, initial algebras, and what not... the end result is the _generic_ -- the technical term is universal -- derivation of certified monadic substitution operations _for free_ from the signature of a simply-typed language. - [Deep Induction Rules for GADTs:](https://popl22.sigplan.org/details/CPP-2022-papers/2/-Deep-Induction-Rules-for-GADTs) _deep_ induction is a technique used to prove properties of _truly_ -- i.e., very -- nested algebraic data types which don't support standard structural recursion rules. This talk presents an extension to cope with certain nested GADTs, and how to automate the generation of induction rules in proof assistants. Regrettably, their technique doesn't scale to _truly_ nested GADTs, but it sets the field for getting closer to being able to derive inductive relations for all GADTs. - [On homotopy of walks and spherical maps in homotopy type theory](https://popl22.sigplan.org/details/CPP-2022-papers/17/On-homotopy-of-walks-and-spherical-maps-in-homotopy-type-theory) An HoTT/Agda formalization using _spherical maps_, combinatorial maps to represent embeddings from graphs into spheres and other higher-inductive types. - [Windmills of the minds: an algorithm for Fermat's Two Squares Theorem.](https://popl22.sigplan.org/details/CPP-2022-papers/1/Windmills-of-the-minds-an-algorithm-for-Fermat-s-Two-Squares-Theorem) a _proof pearl_ from number theory -- the two squares theorem of Fermat -- formalized in HOl4. ## POPL :film_projector: :red_circle: Past and Live YouTube feeds are available, for those without access to the _private_ fun on airmeet: - [Wed Salon I](https://www.youtube.com/watch?v=83D2k5pgFlM) - [Wed Salon III](https://www.youtube.com/watch?v=mMYR_4Ij0AY) - [Thu Salon I](https://www.youtube.com/watch?v=g-spitYZmg0) - [Thu Salon III](https://www.youtube.com/watch?v=KEkK3KJYdSg) - [Fri Salon I](https://www.youtube.com/watch?v=HCmk7FxGnog) - [Fri Salon III](https://www.youtube.com/watch?v=XD89VDxcrpE) ### Wednesday morning POPL started with a Keynote by [Professor Alfred Aho](http://www.cs.columbia.edu/~aho/) -- you must be familiar with [Dragon book series](https://en.wikipedia.org/wiki/Dragon_Book), right? Then path forked, and I went for the Separation Logic track. If you attended the other session and want to recommend something -- please go ahead and start your own thread! #### Alfred V. Aho's Keynote - [Principles of Programming Language Translators:](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/66/Principles-of-Programming-Language-Translators) this very interesting keynote actually focused on _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 operations for manipulating data (the "programming language" of the data model). The talk focused on a taxonomy of 4 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 4 postulates of quantum computing define new kinds of abstractions that extend the previously presented _classical_ ones. #### Separation Logic Separation Logic is a foundational theory for reasoning about _stateful_ programs (i.e. that write, read, consume, and eventually share memory). It's a very active fields of research in the last 20+ years, specially concerning the correctness of concurrent programs. - [A Separation Logic for Heap Space under Garbage Collection](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/15/A-Separation-Logic-for-Heap-Space-under-Garbage-Collection)_reachability_ is a non-local property in Separation Logics, so it's hard to establish. Moreover, it is a fundamental and desirable property for Garbage Collectors as it is required for _logical deallocation_. In this talk the authors present a Separation Logic that allows controlling the heap space consumption of a program in the presence of dynamic memory allocation and garbage collection. - [Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/28/Simuliris-A-Separation-Logic-Framework-for-Verifying-Concurrent-Program-Optimization) This talks presents _Simuliris_, a simulation technique to establish termination preservation for a range of concurrent program transformations that exploit _undefined behaviour_ in the source language. The key idea is using _ownership_ to reason modularly about compiler assumptions about well-defined behavior. Based on the [Iris](https://iris-project.org/) framework. - [Concurrent Incorrectness Separation Logic](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/34/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 asses whether _races_, _deadlocks_, and memory safety errors detected are true positives -- where sound means that all results are _true positives_. - [On Incorrectness Logic and Kleene Algebra With Top and Tests:](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/29/On-Incorrectness-Logic-and-Kleene-Algebra-With-Top-and-Tests) Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, with many fields of applications. Following the common theme from the previous talk, this work aims at utilising KAT provides for reasoning about incorrectness. In particular the resulting framework is expressive enough to model incorrectness triples, and to prove the soundness of sequential Incorrectenss Separation logic. ### Wednesday Afternoon My path through the afternoon led me to navigate through the dark forests of weak memory, and finished with some concurrency and parallelism -- that's the naive SC spec, but you known, terms and ~~conditions~~ reorderings apply. #### Weak Memory models. Multicore architectures screw up the natural sequential understanding of how computer memory works, and how a sequence of instructions is _actually_ implemented. On the bright side, it gave rise to a really rich and active research field , with the aim of getting this right. - [The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory Concurrency.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/54/The-Leaky-Semicolon-Compositional-Semantic-Dependencies-for-Relaxed-Memory-Concurren) This ~~talk~~ live performance, featuring a retrospective of 20 years of research in memory models, looks at how to support sequential composition while targeting modern hardware, via enriching the event-based approach with preconditions and families of predicate transformers. **I'm sorry for those that missed this talk, or even those who were in remote, because the fun was indeed in person. Thanks to Alan et al. for the first weak memory model stand-up show! Soon on Netflix!** - [Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-Temporal Stores:](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/22/Extending-Intel-x86-Consistency-and-Persistency-Formalising-the-Semantics-of-Intel-x) The work extends the existing formalization of the semantics of persistent memory for the Intel-x86 family of architectures to cover: _non-temporal_ writes; mix-model reads and writes, i.e. to uncacheable/write-combined/write-through Intel-x86 memory types;and their interactions. - [Truly Stateless Optimal Dynamic Partial Order Reduction.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/49/Truly-Stateless-Optimal-Dynamic-Partial-Order-Reduction) Dynamic partial order reduction (DPOR) is an automated verification technique, based on equivalence of traces, and it used to reason about concurrent programs by exploring all (modulo some up-to isos) of their interleavings. Here, the focus is on weak memory models like TSO, PSO, and RC11. #### Concurrency and Parallelism - [https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/33/Visibility-Reasoning-for-Concurrent-Snapshot-Algorithms:](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/33/Visibility-Reasoning-for-Concurrent-Snapshot-Algorithms) Visibility relations is an abstraction for proving linearizability of concurrent algorithms, with connections to the relational toolkit used to reason about memory models and distributed consistency. This presentation applies this framework to [reason about 3 concurrent snapshot algorithms by Jayanti](https://dl.acm.org/doi/10.1145/1060590.1060697). **Also, personally, I'm glad that Joaquim stayed away of our previous [hackish proof](https://drops.dagstuhl.de/opus/volltexte/2017/7255/pdf/LIPIcs-ECOOP-2017-8.pdf) for the first Jayanti principle, and instead of ~~building upon~~ suffering with it, decided instead to build a cleaner, more principled framework that can reason about such algorithms. Moreover, I would like too see more works like this one, tackling LL/SC atomics.** - [Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/1/Connectivity-Graphs-A-Method-for-Proving-Deadlock-Freedom-Based-on-Separation-Logic) Connectivity graphs provide an abstract representation of the topology of interacting _entities_ (think threads), and enable reasoning about properties like _deadlock_ and _memory leak_ freedom. This properties are proven out of of Separation Logic rules for graph transformations -- all this formalized in Coq. - [Static Prediction of Parallel Computation Graphs.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/46/Static-Prediction-of-Parallel-Computation-Graphs) Another approach to analyzing computation graphs, this time the focus being parallel programs. This talk introduces _graph types_, encoding all of the graphs that could arise from a program execution. The target is an OCaml, extended with parallelism primitives. #### Reasoning about Probabilistic Programs and Algorithms ... that is, program logics and proof technics which enable verification of probabilistic programming langauges. - [A Separation Logic for Negative Dependence.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/57/A-Separation-Logic-for-Negative-Dependence) This works presents advances in probailistic separation logics -- in particular a logic called LINA -- which enables reasoning about proabilistic data structures relying on hasing, like hash tables and Bloom filters. - [Reasoning about _“Reasoning about Reasoning”_: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/16/Reasoning-about-Reasoning-about-Reasoning-Semantics-and-Contextual-Equivalence-for) The work presents a probabilistic programming language enabling relational reasoning principles for programs making nested queries, hence enabling _meta-reasoning_. The work builds upon a step-indexed, biorthogonal logical-relations model. ### Thursday Morning My Thursday morning menu, took me away from my comfort zone and into the realms of ML -- machine learning, not the one with the :camel: -- and even some quantum computing. #### Keynote - [Better Learning through Programming Languages.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/67/Better-Learning-through-Programming-Languages) [Armando Solana](https://people.csail.mit.edu/asolar/)'s keynote described how different programming language techniques, like _program synthesis_, have transcended this community into domains that have been traditionally associated with machine learning and artificial intelligence. He also went into what's next, and how the PL community can help expand the frontiers of the latter fields. #### Quantum Computing Quantum computers are not a staple of your house yet -- so your kitten is safe. Still, there is a bunch of interesting work going on how the PL techniques apply in this new frontier. - [Quantum Information Effects:](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/2/Quantum-Information-Effects) this work leverages type and effect systems to reason about two specific _quantum_ effects: hiding and allocation. - [Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/30/Twist-Sound-Reasoning-for-Purity-and-Entanglement-in-Quantum-Programs) Twist is a programming language enabling automatic reason about _entanglement_ in quantum programs. It leverages static analysis, runtime verification, and a dedicated type system. The latter supports a notion of _pure_ computations -- i.e., independent of _measurement effects_ -- enabling the detection of entangled states. - [Quantum Separation Logic A Framework for Local Reasoning of Quantum Programs.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/36/Quantum-Separation-Logic-A-Framework-for-Local-Reasoning-of-Quantum-Programs) this work aims at verifying quantum algorithm (including several _classics_ like [Deutsch-Jozsa](https://en.wikipedia.org/wiki/Deutsch%E2%80%93Jozsa_algorithm)), by extending separation logic with a notion of quantum frames. - [Semantics for Variational Quantum Programming.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/26/Semantics-for-Variational-Quantum-Programming) A typed-safe programming language for _variational_ quantum programming, a hybrid classical-quantum paradigm. ### Thursday Afternoon Thursday is usually the heaviest day for me of POPL week -- where you start to feel the physical and mental fatigue of being overwhelmed by too many good talks, and interesting conversations. So, the quality of the reporting might suffer a bit. Still, we soldier through. #### Types and Sessions - [On Type Cases Union Elimination and Occurrence Typing.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/12/On-Type-Cases-Union-Elimination-and-Occurrence-Typing) This work extends classic union and intersection type systems with a type-case construction, and show this suffices to support _occurrence typing_ -- a typing technique that takes into account the result of type tests to assign different types to the same expression when it occurs in different branches of the test. - [Oblivious Algebraic Data Types](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/51/Oblivious-Algebraic-Data-Types) enable to compute functions over _private data_ without leaking sensitive information. This work combines dependent types with constructs for oblivious computation, and in order to enforce in the type system that adversaries can learn nothing more than the result of a computation - [SolType: Refinement Types for Solidity.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/4/SolType-Refinement-Types-for-Solidity) SolType is a refinement type system for Solidity that can be used to prevent arithmetic over- and under-flows in ETH smart contracts. #### Metaprogramming - [Staging with Class.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/61/Staging-with-Class) This work introduces staged type class constraints, which enable typed code quotation in a principled and sound way. - [Moebius: Metaprogramming using Contextual Types.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/39/Moebius-Metaprogramming-using-Contextual-Types) The Moebious meta-programming language leverages contextual modal types to enable the generation of polymorphic code, and its analysis via pattern matching. - [Type Level Programming with Match Types.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/37/Type-Level-Programming-with-Match-Types) This paper presents match types, a type-level equivalent of pattern matching which moreover enables subtyping. ### Friday Morning Friday morning featured an interesting keynote by [Alexandra Silva](https://alexandrasilva.org/#/main.html), and my first time joining the POPL version of musical chairs this year, that is the switching rooms in between sessions to attend talks on different tracks -- I have avoided that in so far. I reckon it is easier to switch browser tabs on remote. #### Keynote - [Coalgebra for the working programming languages researcher](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/68/Coalgebra-for-the-working-programming-languages-researcher) A history of coalgebra and coinduction, from foundations to POPL results. _Coalgebra_ is a mathematical framework to study different types of state-based systems in a uniform way, rooted in category theory. At first results were purely theoretical, but eventually application areas became evident -- including ~~getting papers in POPL~~ the field of programming languages. An example is the foundation of typed languages with fixpoint operators. Towards the end, Alexandra presented a few interesting directions for future research in the field. #### Distributed or Network Programs - [Pirouette: Higher Order Typed Functional Choreographies.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/23/Pirouette-Higher-Order-Typed-Functional-Choreographies) Pirouette, is a programming language for typed higher-order functional choreographs. Pirouette offers programmers the ability to write a centralised functional program and compile it via endpoint projection into programs for each node in a distributed system. Moreover, the paper provides a formalization in Coq, notably showing that the soundness entails deadlock-freedom. #### Semantics **Caveat Emptor!** some heavy-duty theoretical talks on the semantics of programming language, and commutative diagrams galore. - [A Fine Grained Computational Interpretation of Girard's Intuitionistic Proof Nets.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/8/A-Fine-Grained-Computational-Interpretation-of-Girard-s-Intuitionistic-Proof-Nets) This single authored paper by Delia Kesner -- a rare avis these days at conferences like POPL --, introduces a term calculus and a fine-grained operational semantics for proof nets in MELL, a fragment of Intitutionistic Linear Logic. The latter is a powerful framework to reason about resources and effects, and proof-nets enable compositional reasoning using diagrams -- which I reckon is more intituive, amenable, and fun!... than complex and verbose derivation trees. - [Fully abstract models for effectful calculi via category theoretic logical relation.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/44/Fully-abstract-models-for-effectful-calculi-via-category-theoretic-logical-relation) Following Moggi's seminal work on models for _computational_ effects -- read _monads_--, a lot of research effort has been thrown into looking for the most effect generic semantic model, which at the same time has the desirable properties. Here the goal is [_full abstraction_](https://en.wikipedia.org/wiki/Denotational_semantics#Abstraction), that is if the semantic model preserves that any two observationally equivalent terms have equivalent interpretations. - [Layered and Object Based Game Semantics](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/42/Layered-and-Object-Based-Game-Semantics) _Certified Abstraction Layers_ is a framework rooted in linear logic to reason modularly about computational objects. This work extends this framework to provide state encapsulation and shared object concurrency. ### Friday Afternoon It's coming home! The last 10 yards -- or whatever sport metaphor for doing the last bit of effort you are fond of. I thank the PC members for reserving a last treat of memory models, separation logics, and proofs for the big finale. How thoughtful of you to think of me. #### TOPLAS Session - [Armed cats: formal concurrency modelling at Arm.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/69/Armed-cats-formal-concurrency-modelling-at-Arm) This article presents a comprehensive review of work done at Arm on the ARM consistency model, and also shows that the tooling and semantcic models presented can also be applied to other architecture families, like x86. ### Friday Afternoon It's coming home! The last 10 yards -- or whatever sport metaphor for doing the last bit of effort you are fond of. I thank the PC members for reserving a last treat of memory models, separation logics, and proofs for the big finale. How thoughtful of you to think of me. #### TOPLAS Session This session gathered journal papers from the [TOPLAS latest volume](https://dl.acm.org/journal/toplas) -- which where submitted with an option to present the work at the POPL conference. - [Armed cats: formal concurrency modelling at Arm.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/69/Armed-cats-formal-concurrency-modelling-at-Arm) This article presents a comprehensive review of work done at Arm on formalizing memory consistency models for their architectures, and also shows that the tooling and semantic models presented can also be applied to other architecture families, like x86. - [TaDA Live: Compositional Reasoning for Termination of Fine grained Concurrent Programs.](ttps://popl22.sigplan.org/details/POPL-2022-popl-research-papers/70/TaDA-Live-Compositional-Reasoning-for-Termination-of-Fine-grained-Concurrent-Program) TaDa is a concurrent separation logic, which leverages rely guarantee features. This talk introduces _Tada Live!_, a novel version of the framework enabling compositional reasoning about termination of concurrent programs. Notably, they use subjective assertions, in the style of [FCSL](https://software.imdea.org/fcsl/), to model liveness assumptions about the environment. - [Gradualizing the Calculus of Inductive Constructions.](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/71/Gradualizing-the-Calculus-of-Inductive-Constructions) This talks explores variations of CIC calculi to enable _gradual_ features to prototype imprecise types and terms, and explores possible avenues towards the development of "malleable" proof assistants and dependently-typed programming languages with gradual typing support. #### Verification This session highlighted efforts towards verifying lower-level system code: - [Certifying Derivation of State Machines from Coroutines](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/24/Certifying-Derivation-of-State-Machines-from-Coroutines). This talk presented a compiler-based technique (built on coroutines), that enables certifying network protocols implemented in higher level DSL in Coq, and extract certified lower-level, efficient, state machine implementations. - [VIP: Verifying Real World C Idioms with Integer Pointer Casts](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/20/VIP-Verifying-Real-World-C-Idioms-with-Integer-Pointer-Casts). This talk presents VIP, a new memory object model targeting the verification of C programs via an embedding into the Coq proof assistant. The goal is to be able to express rich properties about memory layout and lower-level pointer manipulations -- e.g., those expressed via bit-wise operations on pointer values. - [Verified Compilation of C Programs with a Nominal Memory Model](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/25/Verified-Compilation-of-C-Programs-with-a-Nominal-Memory-Model). This article presents an extension of the [CompCert's](https://compcert.org/) block-based memory model, based on _nominal techniques_, which enables verified compilation of C programs, and enable reasoning about compiler transformation on partial memory. #### Program Synthesis - [Learning Formulas in Finite Variable Logics](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/10/Learning-Formulas-in-Finite-Variable-Logics). This talk presented decidability and realizability results for learning formulas on finite variable logics that classify a set of positive and negative labels, and extensions to FOL and other logics. - [Bottom up Synthesis of Recursive Functional Programs using Angelic Execution](https://popl22.sigplan.org/details/POPL-2022-popl-research-papers/21/Bottom-up-Synthesis-of-Recursive-Functional-Programs-using-Angelic-Execution). This talk presented a novel approach to synthesis of functional recursive programs which outperforms exiting techniques. The synthesized programs are derived from a specification using _angelic_ interleaving semantics based on version space learning. ## CoqPL Among the post-conference workshops on a more quiet Saturday, I attended [CoqPL](https://popl22.sigplan.org/home/CoqPL-2022) -- the Eighth International Workshop on Coq for Programming Languages. This workshop provides an opportunity for the PL research community to meet and interact with members from the core Coq development team. It's a good chance to get a sneak peek upcoming new features of the Coq proof assistants, and see talks about, and demonstrations, of exciting current projects. Also on offer on the menu was [PriSC](https://popl22.sigplan.org/home/prisc-2022), a satellite conference on _secure compilation_, and two new events [ProLaLa](https://popl22.sigplan.org/home/prolala-2022) and [WitS](https://popl22.sigplan.org/home/wits-2022) respectively focusing on the intersection of programming languages and the law, and on the implementation of type systems. ### Morning Session The morning session consisted on an invited talk by [Clement Pit-Claudel](http://pit-claudel.fr/clement/), and a few contributed ones: - [Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofs.](https://popl22.sigplan.org/details/CoqPL-2022-papers/7/Coq-meets-literate-programming-tools-for-documenting-preserving-and-sharing-mechan) Clement has been building library and tooling for the Coq community for a long time -- for e.g., [company-coq](https://github.com/cpitclaudel/company-coq). Today, the issue at hand is _proof presentation_: specifically Alectryon, a framework for literate proving in Coq. The talk focused as well on deeper subjects, like the social process of building proofs, and the trade offs between writing _beautiful proof pearls_ (in equational style) and heavy duty automation -- all I want is the [_gorram_](https://screenrant.com/firefly-swear-word-guide-gorram) QED! - [A Visual Ltac Debugger in CoqIDE.](https://popl22.sigplan.org/details/CoqPL-2022-papers/1/A-Visual-Ltac-Debugger-in-CoqIDE) The existing command-line Ltac debugger in coqtop provides very limited functionality. A visual debugger is much easier to use and more appropriate for the larger projects undertaken today. This paper describes a visual [Ltac](https://coq.inria.fr/refman/proof-engine/ltac.html) debugger added to CoqIDE in Coq 8.15. Most of the Coq changes made to implement the debugger should be readily reusable by other IDEs. - [Scrap your boilerplate definitions in 10 lines of Ltac](https://popl22.sigplan.org/details/CoqPL-2022-papers/2/Scrap-your-boilerplate-definitions-in-10-lines-of-Ltac-). This talk presents IDT, a Coq library for automatically generating the sorts of boilerplate definitions often pestering mechanized meta-theory developers. It's powered by [Template-Coq](https://github.com/gmalecha/template-coq) and uses Ltac to do all the heavy lifting. - [Tealeaves-Categorical-structures-for-syntax](https://popl22.sigplan.org/details/CoqPL-2022-papers/3/Tealeaves-Categorical-structures-for-syntax). This talk introduces Teleaves, a Coq library whose purpose is to formalize abstract syntax theories on top of a concrete one. The interface involves a novel theory of strong monads with extra structure, called _decorated-traversable_ which are monads equipped with additional compatible operations. - [Towards a Formalization of Nominal Sets in Coq](https://popl22.sigplan.org/details/CoqPL-2022-papers/4/Towards-a-Formalization-of-Nominal-Sets-in-Coq). This talk presented a first step towards unified library support for _nominal techniques_ in Coq, based on a formalization of nominal sets. - [A Case for Lightweight Interfaces in Coq](https://popl22.sigplan.org/details/CoqPL-2022-papers/6/A-Case-for-Lightweight-Interfaces-in-Coq). This presentation by the [Bedrock Systems](https://bedrocksystems.com/) team focused on the issue of proof modularity for large industrial projects, in particular those addressing separate compilation, and discussed ideas to mitigate the issue. ### Afternoon Session The shorter afternoon session consisted by one invited talk by [Joseph Tassarotti](http://www.cs.bc.edu/~tassarot/), a contributed talk, and finally, the customary open-mic session with the Coq development team. - [Verifying Concurrent Crash Safe Systems with Perennial](https://popl22.sigplan.org/details/CoqPL-2022-papers/8/Verifying-Concurrent-Crash-Safe-Systems-with-Perennial). This invited talk described efforts towards verifying the heavily-concurrent implementations of file (and other storage) systems, and in particular how to prove _crash-safety_, that is that the systems are able to recover after complete, hard, failures -- like a power cutting off. In particular, the talks describes the principles behind the _Perennial_ framework for formally verifying (in Coq) crash safety of concurrent systems. - [A Verified Pipeline from a Specification Language to Optimized Safe Rust]( https://popl22.sigplan.org/details/CoqPL-2022-papers/5/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust). This talk presents a Coq back-end to leverage the [Fiat crypto](https://github.com/mit-plv/fiat-crypto) and [hacspec](https://github.com/hacspec/hacspec) projects together, in order to provide a mechanized pipeline to extract optimized, safe Rust implementations of cryptographic primitives, notably, BLS elliptic curves. #### Session with the Coq-Dev Team As customary, the CoqPL ended with an open round-table with the members of the core Coq development team, discussing the current and future releases of the Coq proof assistant -- notably [8.14](https://coq.inria.fr/refman/changes.html#version-8-14) and [8.15](https://coq.inria.fr/refman/changes.html#version-8-15), the status of the Coq platform, and the plans for the future.