Image de couverture de livre

A uniform characterisation of the (a)synchronous must-preorder

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Bernardi, Giovanni, Férée, Hugo, Lopez, Gaëtan
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science Programming Languages
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Constructive characterisations of the must-preorder for asynchrony
par: Bernardi, Giovanni, et autres
Publié: (2025)

Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
par: Férée, Hugo, et autres
Publié: (2026)

Abstractions of Sequences, Functions and Operators
par: Rustenholz, Louis, et autres
Publié: (2025)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
par: Rustenholz, Louis, et autres
Publié: (2024)

Kleene algebra with commutativity conditions is undecidable
par: de Amorim, Arthur Azevedo, et autres
Publié: (2024)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
par: Ukhanov, Evgeny
Publié: (2025)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
par: Verscht, Lena, et autres
Publié: (2024)

Meaningfulness and Genericity in a Subsuming Framework
par: Kesner, Delia, et autres
Publié: (2024)

A Probabilistic Choreography Language for PRISM
par: Carbone, Marco, et autres
Publié: (2025)

A Lazy, Concurrent Convertibility Checker
par: Courant, Nathanaëlle, et autres
Publié: (2025)

A Program Logic for Abstract (Hyper)Properties
par: Baldan, Paolo, et autres
Publié: (2026)

A Nominal Approach to Probabilistic Separation Logic
par: Li, John M., et autres
Publié: (2024)

A feasible and unitary quantum programming language
par: Díaz-Caro, Alejandro, et autres
Publié: (2023)

A Demonic Outcome Logic for Randomized Nondeterminism
par: Zilberstein, Noam, et autres
Publié: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
par: Goncharov, Sergey, et autres
Publié: (2026)

A formalization of System I with type Top in Agda
par: Séttimo, Agustín, et autres
Publié: (2026)

A Formally Verified Procedure for Width Inference in FIRRTL
par: Wang, Keyin, et autres
Publié: (2026)

A programming language characterizing quantum polynomial time
par: Hainry, Emmanuel, et autres
Publié: (2022)

PolyQEnt: A Polynomial Quantified Entailment Solver
par: Chatterjee, Krishnendu, et autres
Publié: (2024)

A Formal Semantics of the GraalVM Intermediate Representation
par: Webb, Brae J., et autres
Publié: (2021)

A Coq Library of Sets for Teaching Denotational Semantics
par: Cao, Qinxiang, et autres
Publié: (2024)

A beginner guide to Iris, Coq and separation logic
par: Dietrich, Elizabeth
Publié: (2021)

A Graded Modal Dependent Type Theory with Erasure, Formalized
par: Abel, Andreas, et autres
Publié: (2026)

DateSAT: A Framework for Solving Date and Period Constraints
par: Cui, Leyi, et autres
Publié: (2026)

A denotationally-based program logic for higher-order store
par: Aagaard, Frederik Lerbjerg, et autres
Publié: (2023)

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
par: Soldevila, Mallku, et autres
Publié: (2024)

JAX Autodiff from a Linear Logic Perspective (Extended Version)
par: Giusti, Giulia, et autres
Publié: (2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
par: Tsukada, Takeshi, et autres
Publié: (2025)

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
par: Chen, Zhibo, et autres
Publié: (2023)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
par: Coglio, Alessandro, et autres
Publié: (2025)

A Program Logic for Under-approximating Worst-case Resource Usage
par: Jin, Ziyue, et autres
Publié: (2025)

A Type System for Data Flow and Alias Analysis in ReScript
par: Lund, Nicky Ask, et autres
Publié: (2024)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
par: Vollmer, Victoria, et autres
Publié: (2024)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
par: Castagna, Giuseppe, et autres
Publié: (2024)

Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors
par: Congard, Sidney, et autres
Publié: (2025)

Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
par: Sulzmann, Martin
Publié: (2026)

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

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
par: Kappé, Tobias, et autres
Publié: (2023)

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

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
par: Elad, Neta, et autres
Publié: (2023)