:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Boldo, Sylvie, Clément, François, Martin, Vincent, Mayero, Micaela
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science
Online Access:	https://arxiv.org/abs/2512.04573
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A Rocq Formalization of Simplicial Lagrange Finite Elements
by: Boldo, Sylvie, et al.
Published: (2026)

Teaching Divisibility and Binomials with Coq
by: Boldo, Sylvie, et al.
Published: (2024)

Maths with Coq in L1, a pedagogical experiment
by: Kerjean, Marie, et al.
Published: (2025)

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
by: Rosain, Johann, et al.
Published: (2026)

TensorRocq: Enabling diagrammatic reasoning in Rocq
by: Caldwell, Benjamin, et al.
Published: (2026)

Revisiting the Fast Fourier Transform in Rocq
by: Théry, Laurent
Published: (2022)

String Diagrams for Monoidal Categories, in Rocq
by: Pous, Damien
Published: (2026)

Finite element method. Detailed proofs to be formalized in Coq
by: Clément, François, et al.
Published: (2024)

Adhesive category theory for graph rewriting in Rocq
by: Arsac, Samuel, et al.
Published: (2025)

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
by: Baudart, Guillaume, et al.
Published: (2026)

Nominal Sets in Rocq
by: Paranhos, Fabrício Sanches, et al.
Published: (2025)

RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
by: Kozyrev, Andrei, et al.
Published: (2025)

A Graded Modal Dependent Type Theory with Erasure, Formalized
by: Abel, Andreas, et al.
Published: (2026)

Formal P-Category Theory and Normalization by Evaluation in Rocq
by: Berry, David G., et al.
Published: (2025)

RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
by: Kozyrev, Andrei, et al.
Published: (2026)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
by: Viennot, Jules, et al.
Published: (2025)

FSLI: An Interpretable Formal Semantic System for One-Dimensional Ordering Inference
by: Alkhairy, Maha, et al.
Published: (2025)

Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
by: Mannucci, Mirco A., et al.
Published: (2025)

Unravelling Cyclic First-Order Arithmetic
by: Leigh, Graham E., et al.
Published: (2025)

Graded Quantitative Narrowing
by: Ayala-Rincón, Mauricio, et al.
Published: (2025)

Graded Courrent PDL
by: Lin, Chun-Yu
Published: (2025)

Abstract Scene Graphs: Formalizing and Monitoring Spatial Properties of Automated Driving Functions
by: Saxena, Ishan, et al.
Published: (2025)

A Theory of Formal Choreographic Languages
by: Barbanera, Franco, et al.
Published: (2022)

Meta-Modelling in Formal Concept Analysis
by: Wang, Yingjian
Published: (2024)

The Complexity of Fragments of Second-Order HyperLTL
by: Regaud, Gaëtan, et al.
Published: (2025)

Formalizing two-level type theory with cofibrant exo-nat
by: Uskuplu, Elif
Published: (2023)

Monadic Second-Order Logic of Permutations
by: Jelínek, Vít, et al.
Published: (2025)

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
by: Bacci, Giorgio, et al.
Published: (2025)

Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
by: Lyon, Tim S., et al.
Published: (2024)

On the ABK Conjecture, alpha-well Quasi Orders and Dress-Schiffels product
by: Abraham, Uri, et al.
Published: (2023)

Formalizing equivalences without tears
by: de Jong, Tom
Published: (2024)

Formalization of Amicable Numbers Theory
by: Chen, Zhipeng, et al.
Published: (2026)

Decidability in First-Order Modal Logic with Non-Rigid Constants and Definite Descriptions
by: Artale, Alessandro, et al.
Published: (2025)

Hammering Higher Order Set Theory
by: Brown, Chad E., et al.
Published: (2025)

Graded Monads and Behavioural Equivalence Games
by: Ford, Chase, et al.
Published: (2022)

A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga
by: Cecilia, Gabriele
Published: (2025)

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
by: Moreira, Walter, et al.
Published: (2026)

A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
by: Cecilia, Gabriele, et al.
Published: (2024)

A Two-Watched Literal Scheme for First-Order Logic
by: Briefs, Yasmine, et al.
Published: (2026)

The Parameterized Complexity of Learning Monadic Second-Order Logic
by: van Bergerem, Steffen, et al.
Published: (2023)