Imagen de Portada

Proof Repair across Quotient Type Equivalences

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Viola, Cosmo, Fan, Max, Ringer, Talia
Formato:	Preprint
Publicado:	2023
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement
por: Hu, Jilin, et al.
Publicado: (2025)

QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning
por: Sanchez-Stern, Alex, et al.
Publicado: (2024)

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
por: Kasibatla, Saketh Ram, et al.
Publicado: (2024)

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

ExVerus: Verus Proof Repair via Counterexample Reasoning
por: Yang, Jun, et al.
Publicado: (2026)

Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version)
por: Giovannini, Eric, et al.
Publicado: (2024)

Compilation Quotient (CQ): A Metric for the Compilation Hardness of Programming Languages
por: Szabo, Violet, et al.
Publicado: (2024)

On Propositional Program Equivalence (extended abstract)
por: Kappé, Tobias
Publicado: (2025)

Equivalence Checking of ML GPU Kernels
por: Dubey, Kshitij, et al.
Publicado: (2025)

A Natural Formalized Proof Language
por: Xie, Lihan, et al.
Publicado: (2024)

Automating Equational Proofs in Dirac Notation
por: Xu, Yingte, et al.
Publicado: (2024)

Refuting Equivalence in Probabilistic Programs with Conditioning
por: Chatterjee, Krishnendu, et al.
Publicado: (2025)

Equivalence and Similarity Refutation for Probabilistic Programs
por: Chatterjee, Krishnendu, et al.
Publicado: (2024)

Modernizing SMT-Based Type Error Localization
por: Kopinsky, Max, et al.
Publicado: (2024)

Interaction Equivalence
por: Accattoli, Beniamino, et al.
Publicado: (2024)

Proving Functional Program Equivalence via Directed Lemma Synthesis
por: Sun, Yican, et al.
Publicado: (2024)

Adaptive Shielding via Parametric Safety Proofs
por: Feng, Yao, et al.
Publicado: (2025)

Agentic Proof Automation: A Case Study
por: Xu, Yichen, et al.
Publicado: (2026)

Asynchronous Global Protocols, Precisely: Full Proofs
por: Pischke, Kai, et al.
Publicado: (2025)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
por: Enea, Constantin, et al.
Publicado: (2023)

Incremental Proof Development in Dafny with Module-Based Induction
por: Ho, Son, et al.
Publicado: (2024)

Syntax Repair as Language Intersection
por: Considine, Breandan
Publicado: (2025)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
por: Kent, Zachary, et al.
Publicado: (2025)

Generating Equivalent Representations of Code By A Self-Reflection Approach
por: Li, Jia, et al.
Publicado: (2024)

Grammar Repair with Examples and Tree Automata: Extended Version
por: Lee, Yunjeong, et al.
Publicado: (2026)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
por: Conoly, Owen, et al.
Publicado: (2025)

TypePro: Boosting LLM-Based Type Inference via Inter-Procedural Slicing
por: Lin, Teyu, et al.
Publicado: (2026)

Sheaf-Cohomological Program Analysis: Unifying Bug Finding, Equivalence, and Verification via Čech Cohomology
por: Young, Halley
Publicado: (2026)

TypeDis: A Type System for Disentanglement
por: Moine, Alexandre, et al.
Publicado: (2025)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
por: Paraskevopoulou, Zoe
Publicado: (2026)

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

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
por: Xu, Qiyuan, et al.
Publicado: (2025)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
por: Nagy, Shaan, et al.
Publicado: (2024)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
por: Zhang, Tesla, et al.
Publicado: (2025)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
por: Ravi, Nikil, et al.
Publicado: (2026)

Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
por: Yu, Nengkun, et al.
Publicado: (2025)

Local Type Inference for Context-Free Session Types
por: Almeida, Bernardo, et al.
Publicado: (2025)

Enforcing MAVLink Safety & Security Properties Via Refined Multiparty Session Types
por: Amorim, Arthur, et al.
Publicado: (2025)