ABSTRACT. In an attempt to study how the Rocq prover can help teaching mathematics, we propose to exploit the ring and field tactics extensively to let students justify elementary steps in calculational proofs. These tactics manipulate formulas where they recognize a restricted set of operations and handle every value involving other functions as variables. As a result, they only work at the surface of formulas and their behavior can be puzzling, especially for beginners. We designed an extension where arguments of non-ring or non-field functions are simplified progressively. We will show how this extension makes declarative proof scripts closer to usual mathematical text. This extension is based on companion tactics, ring_simplify and field_simplify. It appears that field_simplify only performs half the simplification we expect. To improve on this, we propose implementing an extension where an external program is called to compute greatest common divisors of polynomials as an oracle and the result is checked in a traditional manner. This talk should interest any user of the Rocq prover interested in developing their own tactics combining some amount of reflexive computation, some amount of external untrusted computation, and some amount of meta-programming, in this case using Ltac and Rocq-Elpi. This is joint work with Thomas Portet, with contributions by Davide Fissore, Laurent Théry, and Enrico Tassi.

ABSTRACT. We present a new iteration of Sulfur, a Rocq library and plugin to deal with substitution automatically for languages with binders. Compared with previous work, out tool supports the definition of various judgments such as typing, in a compositional way, and derives a substitution lemma for them.

ABSTRACT. This paper presents a formalization in Rocq of an extension of our category theory library with a category with computable pushouts and pullbacks. This library already contains several instances of categories with pullbacks and pushouts, but computation is not possible in any of them. We implement a category of finite ordinals and functions and detail how computation was made possible and (relatively) efficient.

ABSTRACT. The Rocq-prover is a functional programming language and logical system based on fixpoints and pattern-matching. To be consistent, Rocq only accepts functions that terminate. This is enforced by a syntactic check named the “guard con- dition”, that ensures that every recursive call is performed on a smaller term than the original one. Despite its critical role, the guard condition is little understood: there is no mathematical justification for it, nor formal specification of it. Moreover, its implementation consist in about 2000 lines of intricate OCaml code, that even experts struggle to under- stand. This lack of understanding has led to inconsistency bugs due to both implementation and theoretical issues, and prevents any further modifications. With this work, we provide the first formal specification of the guard condition as it should be implemented. We fur- ther build knowledge on guard conditions by introducing its different features one by one, and discussing their motiva- tions, limitations and related historical bugs. Based on this specification, we provide a reimplementation of the guard condition in MetaRocq.

ABSTRACT. We present Camltac, a Rocq plugin that allows OCaml to be written directly within Rocq scripts. Camltac blurs the line between Rocq plugins and tactics, letting users leverage the expressivity, performance, and rich ecosystem of OCaml to write tactics and meta-programs, without compromising on simplicity and convenience.

ABSTRACT. For an ongoing mechanisation attempt, I needed some domain theory. A number of libraries on this topic have been developed since the early days of Rocq, but all of them are currently outdated – the most recent has been in maintenance mode since 2014. I propose an experience report on my attempt at porting this library to modern Rocq, both from a technical point of view (use of quotients, automation, hierarchy of structures, etc.) and on “softer” aspects.

ABSTRACT. Verified Rocq components often communicate through ordinary formats after extraction. When two verified components exchange a value through ad hoc JSON encoders and decoders, the components can be correct while the pipeline fails because the boundary code changes, drops, or misreads the value. This paper presents \texttt{rocq-json}, an ELPI-based deriver that generates JSON encoders, decoders, and Rocq-checked round-trip proofs for ordinary inductive and record types. We present the concrete contract the tool provides and the performance profile of the generated serializers.