Cover Image

Towards Automatic Transformations of Coq Proof Scripts

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Magaud, Nicolas
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science Symbolic Computation Software Engineering
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Practical Modelling with Bigraphs
by: Archibald, Blair, et al.
Published: (2024)

Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis
by: Kutsia, Temur, et al.
Published: (2024)

Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits
by: Orvalho, Pedro, et al.
Published: (2025)

On Automating Proofs of Multiplier Adder Trees using the RTL Books
by: Manjrekar, Mayank
Published: (2025)

Pseudo-Complex Quantifier Elimination
by: Faroß, Nicolas, et al.
Published: (2026)

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

Inferring Equivalence Classes from Legacy Undocumented Embedded Binaries for ISO 26262-Compliant Testing
by: De Luca, Marco, et al.
Published: (2026)

HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction
by: Jayasena, Aruna, et al.
Published: (2023)

Automatic Generation of Polynomial Symmetry Breaking Constraints
by: Erascu, Madalina, et al.
Published: (2026)

Solving unification in the description logic $\mathcal{FL}_\bot$
by: Morawska, Barbara, et al.
Published: (2024)

Rings with common division, common meadows and their conditional equational theories
by: Bergstra, Jan A, et al.
Published: (2024)

Improving NLSAT for Nonlinear Real Arithmetic
by: Wang, Zhonghan
Published: (2024)

Saturating Sorting without Sorts
by: Georgiou, Pamina, et al.
Published: (2024)

A Local Search Algorithm for MaxSMT(LIA)
by: He, Xiang, et al.
Published: (2024)

OSVAuto: automatic proofs about functional specifications in OS verification
by: Wu, Yulun, et al.
Published: (2024)

Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs
by: Kaufmann, Daniela, et al.
Published: (2024)

Exhaustive Symbolic Integration: Integration by Differentiation and the Landscape of Symbolic Integrability
by: Desmond, Harry
Published: (2026)

One-Parametric Presburger Arithmetic has Quantifier Elimination
by: Mansutti, Alessio, et al.
Published: (2025)

Proceedings of the 19th International Workshop on Logical and Semantic Frameworks, with Applications
by: Kop, Cynthia, et al.
Published: (2025)

Formal Verification of Parameterized Systems based on Induction
by: Xiu, Jiaqi, et al.
Published: (2025)

Nominal Equational Rewriting and Narrowing
by: Ayala-Rincón, Mauricio, et al.
Published: (2025)

Structuring Definitions in Mathematical Libraries
by: Gusakov, Alena, et al.
Published: (2025)

SCL(FOL) Revisited
by: Bromberger, Martin, et al.
Published: (2023)

From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries
by: Gorna, Karolina, et al.
Published: (2026)

PROMISE: Proof Automation as Structural Imitation of Human Reasoning
by: Ahn, Youngjoo, et al.
Published: (2026)

Names Don't Matter: Symbol-Invariant Transformer for Open-Vocabulary Learning
by: Işık, İlker, et al.
Published: (2026)

Formal Analysis of the Sigmoid Function and Formal Proof of the Universal Approximation Theorem
by: Bryant, Dustin, et al.
Published: (2025)

Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs
by: Brancas, Ricardo, et al.
Published: (2024)

modelSolver: A Symbolic Model-Driven Solver for Power Network Simulation and Monitoring
by: Dzafic, Izudin, et al.
Published: (2025)

SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks
by: Beyer, Dirk, et al.
Published: (2025)

Quantifier Elimination Meets Treewidth
by: Wu, Hao, et al.
Published: (2026)

Identity Testing for Radical Expressions
by: Balaji, Nikhil, et al.
Published: (2022)

On Ambiguity: The case of fraction, its meanings and roles
by: Bergstra, Jan A, et al.
Published: (2026)

The Scaling Properties of Implicit Deductive Reasoning in Transformers
by: Vompa, Enrico, et al.
Published: (2026)

Open Source Prover in the Attic
by: Kovács, Zoltán, et al.
Published: (2024)

From Proof to Program: Characterizing Tool-Induced Reasoning Hallucinations in Large Language Models
by: Bayat, Farima Fatahi, et al.
Published: (2025)

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

A Theoretical Review on Solving Algebra Problems
by: Yu, Xinguo, et al.
Published: (2024)

Boolean Matrix Logic Programming on the GPU
by: Ai, Lun
Published: (2024)

WebPie: A Tiny Slice of Dependent Typing
by: Scholliers, Christophe
Published: (2024)