Cover Image

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Kent, Zachary, Yavuz, Ugur Y., Jayanti, Siddhartha, Balzer, Stephanie, Blelloch, Guy
Format:	Preprint
Published:	2025
Subjects:	Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Pyrosome: Verified Compilation for Modular Metatheory
by: Jamner, Dustin, et al.
Published: (2025)

Big Atomics
by: Anderson, Daniel, et al.
Published: (2025)

Efficient Linearizability Monitoring
by: Abdulla, Parosh Aziz, et al.
Published: (2025)

Automatically Verifying Replication-aware Linearizability
by: Soundarapandian, Vimala, et al.
Published: (2025)

Fixed Parameter Tractable Linearizability Monitoring
by: Han, Lee Zheng, et al.
Published: (2025)

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
by: Zilberstein, Noam
Published: (2024)

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

Logical Relations for Session-Typed Concurrency
by: Balzer, Stephanie, et al.
Published: (2023)

On the First Computer Science Research Paper in an Indian Language and the Future of Science in Indian Languages
by: Jayanti, Siddhartha Visveswara
Published: (2026)

Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency
by: Derakhshan, Farzaneh, et al.
Published: (2024)

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
by: Frenkel, Eden, et al.
Published: (2026)

A Language-Agnostic Logical Relation for Message-Passing Protocols
by: Zhang, Tesla, et al.
Published: (2025)

Relax: Composable Abstractions for End-to-End Dynamic Machine Learning
by: Lai, Ruihang, et al.
Published: (2023)

StitchCUDA: An Automated Multi-Agents End-to-End GPU Programing Framework with Rubric-based Agentic Reinforcement Learning
by: Li, Shiyang, et al.
Published: (2026)

Semantic Logical Relations for Timed Message-Passing Protocols (Extended Version)
by: Yao, Yue, et al.
Published: (2024)

TPDE: A Fast Adaptable Compiler Back-End Framework
by: Schwarz, Tobias, et al.
Published: (2025)

Efficient Decrease-and-Conquer Linearizability Monitoring
by: Han, Lee Zheng, et al.
Published: (2024)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
by: Wu, Jinhua, et al.
Published: (2025)

Multi-Pass Targeted Dynamic Symbolic Execution
by: Yavuz, Tuba
Published: (2024)

Bench4HLS: End-to-End Evaluation of LLMs in High-Level Synthesis Code Generation
by: Khan, M Zafir Sadik, et al.
Published: (2026)

A Forward Simulation-Based Hierarchy of Linearizable Concurrent Objects
by: Wang, Chao, et al.
Published: (2026)

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
by: Thibault, Jérémy, et al.
Published: (2025)

End-to-End Chatbot Evaluation with Adaptive Reasoning and Uncertainty Filtering
by: Dang, Nhi, et al.
Published: (2026)

A Natural Formalized Proof Language
by: Xie, Lihan, et al.
Published: (2024)

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

Diamond: End-to-End Forward-secure and Compact Authenticated Encryption for Internet of Things
by: Nouma, Saif E., et al.
Published: (2026)

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

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

Proof Repair across Quotient Type Equivalences
by: Viola, Cosmo, et al.
Published: (2023)

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

Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion
by: Vákár, Matthijs
Published: (2020)

Towards a Certified Proof Checker for Deep Neural Network Verification
by: Desmartin, Remi, et al.
Published: (2023)

A Certified Proof Checker for Deep Neural Network Verification in Imandra
by: Desmartin, Remi, et al.
Published: (2024)

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

End-to-End Evaluation for Low-Latency Simultaneous Speech Translation
by: Huber, Christian, et al.
Published: (2023)

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

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

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

KG-Reasoner: A Reinforced Model for End-to-End Multi-Hop Knowledge Graph Reasoning
by: Wang, Shuai, et al.
Published: (2026)