The Coq Workshop 2024

We present our experiences so far in bringing Coq-based hardware development to hardware engineers. More specifically, we chose Koika to re-implement the trusted communication unit (TCU), an essential kernel component in a micro-kernel-based operating system. We report on successes but also obstacles and derive future research directions.

The talk presents a development process for Coq projects that permits invalid proofs in the main development line while still keeping control over the project. I review the existing tool support and present new Proof General features that enable such a process. The described process has recently been introduced at Kernkonzept.

We present CoqPilot, a VS Code extension designed to help automate writing of Coq proofs. The plugin collects the parts of proofs marked with the admit tactic in a Coq file, i.e., proof holes, and combines LLMs along with non-machine-learning methods to generate proof candidates for the holes. Then, CoqPilot checks if each proof candidate solves the given subgoal and, if successful, replaces the hole with it. The focus of CoqPilot is twofold. Firstly, we want to allow users to seamlessly combine multiple Coq generation approaches and provide a zero-setup experience for our tool. Secondly, we want to deliver a platform for LLM-based experiments on Coq proof generation. We developed a benchmarking system for Coq generation methods, available in the plugin, and conducted an experiment using it, showcasing the framework's possibilities.

I will discuss the use and usefulness of “blueprints” in formalisation, and the design practices they promote; and I will present a port for Coq of the leanblueprint tool

Dear Coq users and developers, We would like to shed some light on our new project "Coq Platform Doc". Our goal is to provide an online compilation of short, practical and interactive tutorials and how-to guides about Coq and the Coq Platform. We wish this content to be part of the upcoming Rocq website. A detailed description of the project can be found in our Coq Enhancement Proposal (CEP) here: https://github.com/coq/ceps/pull/91.

The first few tutorials are available as well as a (very preliminary) online interface here: https://www.theozimmermann.net/platform-docs/. At this moment, it contains:

• a Search tutorial
• a Basic library file and module management tutorial
• 3 tutorials about the Equation plugin

More will follow, especially with your help!

There is a dedicated Zulip channel to discuss and participate: https://coq.zulipchat.com/#narrow/stream/437203-Coq-Platform-docs. The preliminary git repository is https://github.com/Zimmi48/platform-docs.

We have started a collaborative project to track which of a list of around 1200 theorems have been formalized in the major libraries of the main proof assistants for mathematics: Isabelle, HOL Light, Coq, Lean, Metamath and Mizar.

UniMath is a library of univalent mathematics written in Coq. In the past few years, it has seen growth mostly in the area of category theory and its applications to programming language semantics. We give an overview of the UniMath library, some of the challenges that we are facing in developing and maintaining it, and our solutions to these challenges.

Coq's consistency — and the consistency of constructive type theories in general — crucially depends on all recursive functions being terminating. Technically, in Coq, this is ensured by a so-called guard checker, which is part of Coq's kernel and ensures that fixpoints defined on inductive types are structurally recursive. Coq's guard checker has been first implemented in the 1990s by Christine Paulin-Mohring, but was subsequently extended, adapted, and fixed by several contributors. As a result, there is no exact, abstract specification of it, meaning for instance that formal proofs about it are out of reach. We propose a talk on our ongoing work-in-progress project to synthesise a specification of Coq's guard checker as a guard condition predicate defined in Coq itself on top of the MetaCoq project. We hope that our project will benefit the users of Coq by providing an accurate and transparent description, as well as lay the foundations for future improvements or even mechanised consistency proofs of Coq.

User interfaces for the Coq proof assistant focus on the ability to write and verify proofs, and mostly ignore Coq's ability to compute. This talk shows how the tactic-in-term feature and some adhoc vernacular commands can provide a user experience closer to the one found in computer algebra systems. This work has been implemented in the CoqInterval library.