Buchumschlag

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Gross, Jason, Erbsen, Andres, Philipoom, Jade, Agrawal, Rajashree, Chlipala, Adam
Format:	Preprint
Veröffentlicht:	2023
Schlagworte:	Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Accelerating Verified-Compiler Development with a Verified Rewriting Engine
von: Gross, Jason, et al.
Veröffentlicht: (2022)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
von: Conoly, Owen, et al.
Veröffentlicht: (2025)

Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
von: Gross, Jason, et al.
Veröffentlicht: (2022)

Securing Cryptographic Software via Typed Assembly Language (Extended Version)
von: Song, Shixin, et al.
Veröffentlicht: (2025)

ViCAR: Visualizing Categories with Automated Rewriting in Coq
von: Shah, Bhakti, et al.
Veröffentlicht: (2024)

Pyrosome: Verified Compilation for Modular Metatheory
von: Jamner, Dustin, et al.
Veröffentlicht: (2025)

A Graphical Interface for Category Theory Proofs in Coq
von: Chabassier, Luc
Veröffentlicht: (2025)

Towards a Coq-verified Chain of Esterel Semantics
von: Berry, Gérard, et al.
Veröffentlicht: (2019)

A Coq implementation of a Theory of Tagged Objects
von: Gates, Matthew, et al.
Veröffentlicht: (2025)

Causality and Semantic Separation
von: Zhang, Anna, et al.
Veröffentlicht: (2026)

A Coq Mechanization of JavaScript Regular Expression Semantics
von: De Santo, Noé, et al.
Veröffentlicht: (2024)

A Coq Library of Sets for Teaching Denotational Semantics
von: Cao, Qinxiang, et al.
Veröffentlicht: (2024)

A beginner guide to Iris, Coq and separation logic
von: Dietrich, Elizabeth
Veröffentlicht: (2021)

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
von: Soldevila, Mallku, et al.
Veröffentlicht: (2024)

Verifying Peephole Rewriting In SSA Compiler IRs
von: Bhat, Siddharth, et al.
Veröffentlicht: (2024)

Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi
von: Tei, Kayo, et al.
Veröffentlicht: (2025)

Dias: Dynamic Rewriting of Pandas Code
von: Baziotis, Stefanos, et al.
Veröffentlicht: (2023)

eqsat: An Equality Saturation Dialect for Non-destructive Rewriting
von: Merckx, Jules, et al.
Veröffentlicht: (2025)

A Distribution Semantics for Probabilistic Term Rewriting
von: Vidal, Germán
Veröffentlicht: (2024)

Enhancing a Hierarchical Graph Rewriting Language based on MELL Cut Elimination
von: Takyu, Kento, et al.
Veröffentlicht: (2024)

Rewrite System Showdown: Stochastic Search vs. EqSat
von: Hong, Qiantan, et al.
Veröffentlicht: (2026)

Introducing Quantification into a Hierarchical Graph Rewriting Language
von: Mishina, Haruto, et al.
Veröffentlicht: (2024)

A Natural Formalized Proof Language
von: Xie, Lihan, et al.
Veröffentlicht: (2024)

Linearization via Rewriting (Long Version)
von: Lago, Ugo Dal, et al.
Veröffentlicht: (2025)

Agentic Proof Automation: A Case Study
von: Xu, Yichen, et al.
Veröffentlicht: (2026)

On Complexity Bounds and Confluence of Parallel Term Rewriting
von: Baudon, Thaïs, et al.
Veröffentlicht: (2023)

SkipFlow: Improving the Precision of Points-to Analysis using Primitive Values and Predicate Edges
von: Kozak, David, et al.
Veröffentlicht: (2025)

Confluence of Conditional Rewriting Modulo
von: Lucas, Salvador
Veröffentlicht: (2025)

Compact Proofs of Model Performance via Mechanistic Interpretability
von: Gross, Jason, et al.
Veröffentlicht: (2024)

Automating Equational Proofs in Dirac Notation
von: Xu, Yingte, et al.
Veröffentlicht: (2024)

LiveRec: Prototyping Probes by Framing Debug Protocols
von: Döderlein, Jean-Baptiste, et al.
Veröffentlicht: (2024)

SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
von: Nezhad, Sina Bagheri, et al.
Veröffentlicht: (2025)

Proof Repair across Quotient Type Equivalences
von: Viola, Cosmo, et al.
Veröffentlicht: (2023)

Adaptive Shielding via Parametric Safety Proofs
von: Feng, Yao, et al.
Veröffentlicht: (2025)

Asynchronous Global Protocols, Precisely: Full Proofs
von: Pischke, Kai, et al.
Veröffentlicht: (2025)

Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
von: Chakraborty, Saikat, et al.
Veröffentlicht: (2024)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
von: Enea, Constantin, et al.
Veröffentlicht: (2023)

Towards a Certified Proof Checker for Deep Neural Network Verification
von: Desmartin, Remi, et al.
Veröffentlicht: (2023)

Incremental Proof Development in Dafny with Module-Based Induction
von: Ho, Son, et al.
Veröffentlicht: (2024)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
von: Paraskevopoulou, Zoe
Veröffentlicht: (2026)