Imagen de Portada

Teaching Divisibility and Binomials with Coq

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Boldo, Sylvie, Clément, François, Hamelin, David, Mayero, Micaela, Rousselin, Pierre
Formato:	Preprint
Publicado:	2024
Materias:	Logic in Computer Science
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

A Rocq Formalization of Monomial and Graded Orders
por: Boldo, Sylvie, et al.
Publicado: (2025)

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

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

A Coq Library of Sets for Teaching Denotational Semantics
por: Cao, Qinxiang, et al.
Publicado: (2024)

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
por: Affeldt, Reynald, et al.
Publicado: (2024)

A Coq Formalization of Unification Modulo Exclusive-Or
por: Xu, Yichi, et al.
Publicado: (2025)

A beginner guide to Iris, Coq and separation logic
por: Dietrich, Elizabeth
Publicado: (2021)

Algorithms for Markov Binomial Chains
por: Gonzalez, Alejandro Alarcón, et al.
Publicado: (2024)

Towards Automatic Transformations of Coq Proof Scripts
por: Magaud, Nicolas
Publicado: (2024)

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
por: Soldevila, Mallku, et al.
Publicado: (2024)

Assessing the Quality of Binomial Samplers: A Statistical Distance Framework
por: Sarkar, Uddalok, et al.
Publicado: (2025)

Taming Differentiable Logics with Coq Formalisation
por: Affeldt, Reynald, et al.
Publicado: (2024)

Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
por: Florath, Andreas
Publicado: (2024)

CoqPilot, a plugin for LLM-based generation of proofs
por: Kozyrev, Andrei, et al.
Publicado: (2024)

A Coq-based Axiomatization of Tarski's Mereogeometry
por: Barlatier, Patrick, et al.
Publicado: (2025)

Towards a Coq-verified Chain of Esterel Semantics
por: Berry, Gérard, et al.
Publicado: (2019)

Nonlinear Arithmetic with SMTLIB Division is Undecidable
por: Jovanovic, Dejan
Publicado: (2026)

Towards an Independent Version of Tarski's System of Geometry
por: Boutry, Pierre, et al.
Publicado: (2024)

A Graphical Interface for Category Theory Proofs in Coq
por: Chabassier, Luc
Publicado: (2025)

List types for resource aware languages: an implicit name approach
por: Ghilezan, Silvia, et al.
Publicado: (2021)

Verified and Optimized Implementation of Orthologic Proof Search
por: Guilloud, Simon, et al.
Publicado: (2025)

A dual characterisation of simple and subdirectly-irreducible temporal Heyting algebras
por: Alvarez, David Quinn
Publicado: (2025)

A Complete Equational Theory for Real-Clifford+CH Quantum Circuits
por: Clément, Alexandre
Publicado: (2026)

The Size-Change Principle for Mixed Inductive and Coinductive types
por: Hyvernat, Pierre
Publicado: (2024)

The Qualitative Collapse of Concurrent Games
por: Clairambault, Pierre
Publicado: (2024)

A Relational Theory of Grounding and a new Grounder for SMT
por: Carbonnelle, Pierre
Publicado: (2026)

Did Turing prove the undecidability of the halting problem?
por: Hamkins, Joel David, et al.
Publicado: (2024)

Base-extension Semantics for Modal Logic
por: Eckhardt, Timo, et al.
Publicado: (2024)

Base-extension Semantics for Intuitionistic Modal Logics
por: Buzoku, Yll, et al.
Publicado: (2025)

Dynamic Cantor Derivative Logic
por: Fernández-Duque, David, et al.
Publicado: (2021)

Semantic Foundations of Reductive Reasoning
por: Gheorghiu, Alexander V., et al.
Publicado: (2024)

Proof-theoretic Semantics for Second-order Logic
por: Gheorghiu, Alexander V., et al.
Publicado: (2025)

From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic
por: Gheorghiu, Alexander V., et al.
Publicado: (2022)

Syntax and semantics of multi-adjoint normal logic programming
por: Cornejo, M. Eugenia, et al.
Publicado: (2024)

Extended multi-adjoint logic programming
por: Cornejo, M. Eugenia, et al.
Publicado: (2024)

Multi-Environment MDPs with Prior and Universal Semantics
por: Bordais, Benjamin, et al.
Publicado: (2026)

Proof-theoretic Semantics for the Logic of Bunched Implications
por: Gu, Tao, et al.
Publicado: (2023)

Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic (Extended Abstract)
por: Gheorghiu, Alexander V., et al.
Publicado: (2023)

Tree Rewriting Calculi for Strictly Positive Logics
por: Santiago-Fernández, Sofía, et al.
Publicado: (2025)