Buchumschlag

Proof Repair across Quotient Type Equivalences

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Viola, Cosmo, Fan, Max, Ringer, Talia
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

Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs
von: Britton, Matthew, et al.
Veröffentlicht: (2026)

Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion
von: Zhang, Dylan, et al.
Veröffentlicht: (2024)

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
von: Hu, Jilin, et al.
Veröffentlicht: (2025)

QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
von: Sanchez-Stern, Alex, et al.
Veröffentlicht: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
von: Kasibatla, Saketh Ram, et al.
Veröffentlicht: (2024)

We've Got You Covered: Type-Guided Repair of Incomplete Input Generators
von: LaFontaine, Patrick, et al.
Veröffentlicht: (2025)

ExVerus: Verus Proof Repair via Counterexample Reasoning
von: Yang, Jun, et al.
Veröffentlicht: (2026)

Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version)
von: Giovannini, Eric, et al.
Veröffentlicht: (2024)

Compilation Quotient (CQ): A Metric for the Compilation Hardness of Programming Languages
von: Szabo, Violet, et al.
Veröffentlicht: (2024)

On Propositional Program Equivalence (extended abstract)
von: Kappé, Tobias
Veröffentlicht: (2025)

Equivalence Checking of ML GPU Kernels
von: Dubey, Kshitij, et al.
Veröffentlicht: (2025)

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

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

Refuting Equivalence in Probabilistic Programs with Conditioning
von: Chatterjee, Krishnendu, et al.
Veröffentlicht: (2025)

Equivalence and Similarity Refutation for Probabilistic Programs
von: Chatterjee, Krishnendu, et al.
Veröffentlicht: (2024)

Modernizing SMT-Based Type Error Localization
von: Kopinsky, Max, et al.
Veröffentlicht: (2024)

Interaction Equivalence
von: Accattoli, Beniamino, et al.
Veröffentlicht: (2024)

Proving Functional Program Equivalence via Directed Lemma Synthesis
von: Sun, Yican, et al.
Veröffentlicht: (2024)

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

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

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

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

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

Syntax Repair as Language Intersection
von: Considine, Breandan
Veröffentlicht: (2025)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
von: Kent, Zachary, et al.
Veröffentlicht: (2025)

Generating Equivalent Representations of Code By A Self-Reflection Approach
von: Li, Jia, et al.
Veröffentlicht: (2024)

Grammar Repair with Examples and Tree Automata: Extended Version
von: Lee, Yunjeong, et al.
Veröffentlicht: (2026)

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

TypePro: Boosting LLM-Based Type Inference via Inter-Procedural Slicing
von: Lin, Teyu, et al.
Veröffentlicht: (2026)

Sheaf-Cohomological Program Analysis: Unifying Bug Finding, Equivalence, and Verification via Čech Cohomology
von: Young, Halley
Veröffentlicht: (2026)

TypeDis: A Type System for Disentanglement
von: Moine, Alexandre, et al.
Veröffentlicht: (2025)

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

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
von: Schüssele, Frank, et al.
Veröffentlicht: (2025)

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
von: Xu, Qiyuan, et al.
Veröffentlicht: (2025)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
von: Nagy, Shaan, et al.
Veröffentlicht: (2024)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
von: Zhang, Tesla, et al.
Veröffentlicht: (2025)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
von: Ravi, Nikil, et al.
Veröffentlicht: (2026)

Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
von: Yu, Nengkun, et al.
Veröffentlicht: (2025)

Local Type Inference for Context-Free Session Types
von: Almeida, Bernardo, et al.
Veröffentlicht: (2025)

Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types
von: Amorim, Arthur, et al.
Veröffentlicht: (2025)