:: Library Catalog

Image de couverture de livre

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Feng, Yao, Zhu, Jun, Platzer, André, Laurent, Jonathan
Format:	Preprint
Publié:	2025
Sujets:	Programming Languages
Accès en ligne:	https://arxiv.org/abs/2502.18879
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Oracular Programming: A Modular Foundation for Building LLM-Enabled Software
par: Laurent, Jonathan, et autres
Publié: (2025)

Hybrid Game Control Envelope Synthesis
par: Kabra, Aditi, et autres
Publié: (2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
par: Teuber, Samuel, et autres
Publié: (2025)

ExVerus: Verus Proof Repair via Counterexample Reasoning
par: Yang, Jun, et autres
Publié: (2026)

A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
par: Bayazıt, Barış, et autres
Publié: (2025)

Parametricity via Cohesion
par: Aberlé, C. B.
Publié: (2024)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
par: Zhang, Tesla, et autres
Publié: (2025)

Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
par: He, Siyuan, et autres
Publié: (2026)

Language-Parametric Reference Synthesis (Extended)
par: Pelsmaeker, Daniel A. A., et autres
Publié: (2025)

Axiomatization of Compact Initial Value Problems: Open Properties
par: Platzer, André, et autres
Publié: (2024)

A Natural Formalized Proof Language
par: Xie, Lihan, et autres
Publié: (2024)

Automating Equational Proofs in Dirac Notation
par: Xu, Yingte, et autres
Publié: (2024)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
par: Frenkel, Eden, et autres
Publié: (2026)

Substructural Parametricity
par: Aberlé, C. B., et autres
Publié: (2025)

Asynchronous Global Protocols, Precisely: Full Proofs
par: Pischke, Kai, et autres
Publié: (2025)

Proof Repair across Quotient Type Equivalences
par: Viola, Cosmo, et autres
Publié: (2023)

Agentic Proof Automation: A Case Study
par: Xu, Yichen, et autres
Publié: (2026)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
par: Enea, Constantin, et autres
Publié: (2023)

Incremental Proof Development in Dafny with Module-Based Induction
par: Ho, Son, et autres
Publié: (2024)

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
par: Ravi, Nikil, et autres
Publié: (2026)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
par: Kent, Zachary, et autres
Publié: (2025)

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
par: Conoly, Owen, et autres
Publié: (2025)

Coinductive Proofs for Temporal Hyperliveness
par: Correnson, Arthur, et autres
Publié: (2025)

Symmetric Proofs of Parameterized Programs
par: Cheng, Ruotong, et autres
Publié: (2026)

A Usage-Aware Sequent Calculus for Differential Dynamic Logic
par: Dotzel, Myra, et autres
Publié: (2023)

The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version)
par: Schüssele, Frank, et autres
Publié: (2025)

A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
par: Xu, Qiyuan, et autres
Publié: (2025)

Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
par: Paraskevopoulou, Zoe
Publié: (2026)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
par: Nagy, Shaan, et autres
Publié: (2024)

ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
par: Gu, Alex, et autres
Publié: (2025)

Parametrizing Reads-From Equivalence for Predictive Monitoring
par: Farzan, Azadeh, et autres
Publié: (2026)

Unlocking the Power of Environment Assumptions for Unit Proofs
par: Priya, Siddharth, et autres
Publié: (2024)

Towards a Scalable Proof Engine: A Performant Prototype Rewriting Primitive for Coq
par: Gross, Jason, et autres
Publié: (2023)

More Church-Rosser Proofs in BELUGA
par: Momigliano, Alberto, et autres
Publié: (2024)

Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
par: Ho, Son, et autres
Publié: (2024)

SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
par: Nezhad, Sina Bagheri, et autres
Publié: (2025)

Cypher is Turing-Complete: A Formal Proof via 2-Counter Machine Simulation
par: Halftermeyer, Pierre
Publié: (2026)

Refactoring and Equivalence in Rust: Expanding the REM Toolchain with a Novel Approach to Automated Equivalence Proofs
par: Britton, Matthew, et autres
Publié: (2026)

Cyclic Proofs in Hoare Logic and its Reverse
par: Brotherston, James, et autres
Publié: (2025)

Pleasant Imperative Program Proofs with GallinaC
par: Fort, Frédéric, et autres
Publié: (2025)