Imagen de Portada

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Viennot, Jules, Baudart, Guillaume, Arias, Emilio Jesùs Gallego, Lelarge, Marc
Formato:	Preprint
Publicado:	2025
Materias:	Logic in Computer Science Computation and Language Machine Learning Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

Verified Purely Functional Catenable Real-Time Deques
por: Viennot, Jules, et al.
Publicado: (2025)

Canonical bidirectional typechecking
por: Mihejevs, Zanzi, et al.
Publicado: (2025)

Symmetric Proofs of Parameterized Programs
por: Cheng, Ruotong, et al.
Publicado: (2026)

Coinductive Proofs for Temporal Hyperliveness
por: Correnson, Arthur, et al.
Publicado: (2025)

More Church-Rosser Proofs in BELUGA
por: Momigliano, Alberto, et al.
Publicado: (2024)

Can Proof Assistants Verify Multi-Agent Systems?
por: Mendez, Julian Alfredo, et al.
Publicado: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
por: Brotherston, James, et al.
Publicado: (2025)

Pleasant Imperative Program Proofs with GallinaC
por: Fort, Frédéric, et al.
Publicado: (2025)

Zippy -- Generic White-Box Proof Search with Zippers
por: Kappelmann, Kevin
Publicado: (2025)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
por: Gladshtein, Vladimir, et al.
Publicado: (2024)

CHAD: Combinatory Homomorphic Automatic Differentiation
por: Vákár, Matthijs, et al.
Publicado: (2021)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
por: Oda, Yukihiro
Publicado: (2025)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
por: Vollmer, Victoria, et al.
Publicado: (2024)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
por: Castagna, Giuseppe, et al.
Publicado: (2024)

Higher Order Automatic Differentiation of Higher Order Functions
por: Huot, Mathieu, et al.
Publicado: (2021)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
por: Elad, Neta, et al.
Publicado: (2025)

S4 modal sequent calculus as intermediate logic and intermediate language
por: Caspar, Jean, et al.
Publicado: (2026)

Kleene algebra with commutativity conditions is undecidable
por: de Amorim, Arthur Azevedo, et al.
Publicado: (2024)

Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors
por: Congard, Sidney, et al.
Publicado: (2025)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
por: de Vilhena, Paulo Emílio, et al.
Publicado: (2021)

Mini-Batch Robustness Verification of Deep Neural Networks
por: Tzour-Shaday, Saar, et al.
Publicado: (2025)

An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory
por: Jeong, Gyeongwon, et al.
Publicado: (2026)

A Deductive System for Contract Satisfaction Proofs
por: Correnson, Arthur, et al.
Publicado: (2026)

A Proof-Producing Compiler for Blockchain Applications
por: Avigad, Jeremy, et al.
Publicado: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
por: Grandury, Marcos, et al.
Publicado: (2025)

Cypher is Turing-Complete: A Formal Proof via 2-Counter Machine Simulation
por: Halftermeyer, Pierre
Publicado: (2026)

Frex: dependently-typed algebraic simplification
por: Allais, Guillaume, et al.
Publicado: (2023)

An Empirical Study of Rational Tree Unification for miniKanren
por: Domoratskiy, Eridan, et al.
Publicado: (2025)

Towards a Certified Proof Checker for Deep Neural Network Verification
por: Desmartin, Remi, et al.
Publicado: (2023)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
por: Desmartin, Remi, et al.
Publicado: (2024)

Deciding Serializability in Network Systems
por: Amir, Guy, et al.
Publicado: (2026)

Exploiting the Potential of Linearity in Automatic Differentiation and Computational Cryptography
por: Giusti, Giulia
Publicado: (2025)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
por: Thakur, Amitayush, et al.
Publicado: (2025)

Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)
por: Mangel, Éléonore, et al.
Publicado: (2025)

A Probabilistic Choreography Language for PRISM
por: Carbone, Marco, et al.
Publicado: (2025)

Internalizing Representation Independence with Univalence
por: Angiuli, Carlo, et al.
Publicado: (2020)

Denotational Semantics for Probabilistic and Concurrent Programs
por: Zilberstein, Noam, et al.
Publicado: (2025)

Crash-Stop Failures in Asynchronous Multiparty Session Types
por: Barwell, Adam D., et al.
Publicado: (2023)