Cover Image

Constructive characterisations of the must-preorder for asynchrony

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Bernardi, Giovanni, Castellani, Ilaria, Laforgue, Paul, Stefanesco, Léo
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

A uniform characterisation of the (a)synchronous must-preorder
by: Bernardi, Giovanni, et al.
Published: (2026)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
by: Timany, Amin, et al.
Published: (2021)

Towards a Semantic Characterisation of Global Type Well-formedness
by: Castellani, Ilaria, et al.
Published: (2024)

Flexible Correct-by-Construction Programming
by: Runge, Tobias, et al.
Published: (2022)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

A 2-adjunction between representations and preorder morphisms
by: Brunet, Paul
Published: (2026)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

Denotational Semantics for Probabilistic and Concurrent Programs
by: Zilberstein, Noam, et al.
Published: (2025)

Positive Sharing and Abstract Machines
by: Accattoli, Beniamino, et al.
Published: (2025)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Expressive Power of One-Shot Control Operators and Coroutines
by: Kobayashi, Kentaro, et al.
Published: (2025)

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)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

The Functional Machine Calculus III: Control
by: Heijltjes, Willem
Published: (2025)

Orthologic Type Systems
by: Guilloud, Simon, et al.
Published: (2025)

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report)
by: Rowicki, Radosław Jan, et al.
Published: (2025)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Proceedings Twelfth Workshop on Fixed Points in Computer Science
by: Saurin, Alexis
Published: (2025)

A Lazy, Concurrent Convertibility Checker
by: Courant, Nathanaëlle, et al.
Published: (2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
by: Tsukada, Takeshi, et al.
Published: (2025)

Coinductive Proofs for Temporal Hyperliveness
by: Correnson, Arthur, et al.
Published: (2025)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Extended Abstract: Mutable Objects with Several Implementations
by: Kaufmann, Matt, et al.
Published: (2025)

Cyclic Proofs in Hoare Logic and its Reverse
by: Brotherston, James, et al.
Published: (2025)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
by: Teuber, Samuel, et al.
Published: (2025)

Intrinsically Correct Algorithms and Recursive Coalgebras
by: Alexandru, Cass, et al.
Published: (2025)

Dependent Multiplicities in Dependent Linear Type Theory
by: Doré, Maximilian
Published: (2025)

Quantum Programming in Polylogarithmic Time
by: Ferrari, Florent, et al.
Published: (2025)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
by: Le, Quang Loc
Published: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
by: Batz, Kevin, et al.
Published: (2025)

Partial Incorrectness Logic
by: Verscht, Lena, et al.
Published: (2025)

Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers
by: Endo, Ryunosuke, et al.
Published: (2025)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
by: Tang, Xichen
Published: (2025)

Semantically Reflected Programs
by: Kamburjan, Eduard, et al.
Published: (2025)

Handling the Selection Monad (Full Version)
by: Plotkin, Gordon, et al.
Published: (2025)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
by: Oda, Yukihiro
Published: (2025)