Buchumschlag

A Rocq Formalization of Monomial and Graded Orders

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Boldo, Sylvie, Clément, François, Martin, Vincent, Mayero, Micaela
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Logic in Computer Science
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

A Rocq Formalization of Simplicial Lagrange Finite Elements
von: Boldo, Sylvie, et al.
Veröffentlicht: (2026)

Teaching Divisibility and Binomials with Coq
von: Boldo, Sylvie, et al.
Veröffentlicht: (2024)

Maths with Coq in L1, a pedagogical experiment
von: Kerjean, Marie, et al.
Veröffentlicht: (2025)

TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
von: Rosain, Johann, et al.
Veröffentlicht: (2026)

TensorRocq: Enabling diagrammatic reasoning in Rocq
von: Caldwell, Benjamin, et al.
Veröffentlicht: (2026)

Revisiting the Fast Fourier Transform in Rocq
von: Théry, Laurent
Veröffentlicht: (2022)

String Diagrams for Monoidal Categories, in Rocq
von: Pous, Damien
Veröffentlicht: (2026)

Adhesive category theory for graph rewriting in Rocq
von: Arsac, Samuel, et al.
Veröffentlicht: (2025)

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

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
von: Baudart, Guillaume, et al.
Veröffentlicht: (2026)

Nominal Sets in Rocq
von: Paranhos, Fabrício Sanches, et al.
Veröffentlicht: (2025)

RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
von: Kozyrev, Andrei, et al.
Veröffentlicht: (2025)

A Graded Modal Dependent Type Theory with Erasure, Formalized
von: Abel, Andreas, et al.
Veröffentlicht: (2026)

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

FSLI: An Interpretable Formal Semantic System for One-Dimensional Ordering Inference
von: Alkhairy, Maha, et al.
Veröffentlicht: (2025)

RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
von: Kozyrev, Andrei, et al.
Veröffentlicht: (2026)

Unravelling Cyclic First-Order Arithmetic
von: Leigh, Graham E., et al.
Veröffentlicht: (2025)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
von: Viennot, Jules, et al.
Veröffentlicht: (2025)

Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
von: Mannucci, Mirco A., et al.
Veröffentlicht: (2025)

Graded Quantitative Narrowing
von: Ayala-Rincón, Mauricio, et al.
Veröffentlicht: (2025)

Graded Courrent PDL
von: Lin, Chun-Yu
Veröffentlicht: (2025)

Abstract Scene Graphs: Formalizing and Monitoring Spatial Properties of Automated Driving Functions
von: Saxena, Ishan, et al.
Veröffentlicht: (2025)

A Theory of Formal Choreographic Languages
von: Barbanera, Franco, et al.
Veröffentlicht: (2022)

The Complexity of Fragments of Second-Order HyperLTL
von: Regaud, Gaëtan, et al.
Veröffentlicht: (2025)

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

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
von: Bacci, Giorgio, et al.
Veröffentlicht: (2025)

On the ABK Conjecture, alpha-well Quasi Orders and Dress-Schiffels product
von: Abraham, Uri, et al.
Veröffentlicht: (2023)

Monadic Second-Order Logic of Permutations
von: Jelínek, Vít, et al.
Veröffentlicht: (2025)

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

Formalizing equivalences without tears
von: de Jong, Tom
Veröffentlicht: (2024)

Formalization of Amicable Numbers Theory
von: Chen, Zhipeng, et al.
Veröffentlicht: (2026)

Hammering Higher Order Set Theory
von: Brown, Chad E., et al.
Veröffentlicht: (2025)

Formalizing two-level type theory with cofibrant exo-nat
von: Uskuplu, Elif
Veröffentlicht: (2023)

Graded Monads and Behavioural Equivalence Games
von: Ford, Chase, et al.
Veröffentlicht: (2022)

Meta-Modelling in Formal Concept Analysis
von: Wang, Yingjian
Veröffentlicht: (2024)

A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga
von: Cecilia, Gabriele
Veröffentlicht: (2025)

Sequencelib: A Computational Platform for Formalizing the OEIS in Lean
von: Moreira, Walter, et al.
Veröffentlicht: (2026)

A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
von: Cecilia, Gabriele, et al.
Veröffentlicht: (2024)

A Two-Watched Literal Scheme for First-Order Logic
von: Briefs, Yasmine, et al.
Veröffentlicht: (2026)

The Parameterized Complexity of Learning Monadic Second-Order Logic
von: van Bergerem, Steffen, et al.
Veröffentlicht: (2023)