Copertina

Proof Repair across Quotient Type Equivalences

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Viola, Cosmo, Fan, Max, Ringer, Talia
Natura:	Preprint
Pubblicazione:	2023
Soggetti:	Programming Languages
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

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

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

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

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

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

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

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

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

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

On Propositional Program Equivalence (extended abstract)
di: Kappé, Tobias
Pubblicazione: (2025)

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

A Natural Formalized Proof Language
di: Xie, Lihan, et al.
Pubblicazione: (2024)

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

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

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

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

Interaction Equivalence
di: Accattoli, Beniamino, et al.
Pubblicazione: (2024)

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

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

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

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

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

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

Syntax Repair as Language Intersection
di: Considine, Breandan
Pubblicazione: (2025)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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