Imagen de Portada

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

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Bernardi, Giovanni, Férée, Hugo, Lopez, Gaëtan
Formato:	Preprint
Publicado:	2026
Materias:	Logic in Computer Science Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Constructive characterisations of the must-preorder for asynchrony
por: Bernardi, Giovanni, et al.
Publicado: (2025)

Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
por: Férée, Hugo, et al.
Publicado: (2026)

Abstractions of Sequences, Functions and Operators
por: Rustenholz, Louis, et al.
Publicado: (2025)

An Order Theory Framework of Recurrence Equations for Static Cost Analysis $-$ Dynamic Inference of Non-Linear Inequality Invariants
por: Rustenholz, Louis, et al.
Publicado: (2024)

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

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

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
por: Verscht, Lena, et al.
Publicado: (2024)

Meaningfulness and Genericity in a Subsuming Framework
por: Kesner, Delia, et al.
Publicado: (2024)

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

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

A Program Logic for Abstract (Hyper)Properties
por: Baldan, Paolo, et al.
Publicado: (2026)

A Nominal Approach to Probabilistic Separation Logic
por: Li, John M., et al.
Publicado: (2024)

A feasible and unitary quantum programming language
por: Díaz-Caro, Alejandro, et al.
Publicado: (2023)

A Demonic Outcome Logic for Randomized Nondeterminism
por: Zilberstein, Noam, et al.
Publicado: (2024)

Towards a Higher-Order Bialgebraic Denotational Semantics
por: Goncharov, Sergey, et al.
Publicado: (2026)

A formalization of System I with type Top in Agda
por: Séttimo, Agustín, et al.
Publicado: (2026)

A Formally Verified Procedure for Width Inference in FIRRTL
por: Wang, Keyin, et al.
Publicado: (2026)

A programming language characterizing quantum polynomial time
por: Hainry, Emmanuel, et al.
Publicado: (2022)

PolyQEnt: A Polynomial Quantified Entailment Solver
por: Chatterjee, Krishnendu, et al.
Publicado: (2024)

A Formal Semantics of the GraalVM Intermediate Representation
por: Webb, Brae J., et al.
Publicado: (2021)

A Coq Library of Sets for Teaching Denotational Semantics
por: Cao, Qinxiang, et al.
Publicado: (2024)

A beginner guide to Iris, Coq and separation logic
por: Dietrich, Elizabeth
Publicado: (2021)

A Graded Modal Dependent Type Theory with Erasure, Formalized
por: Abel, Andreas, et al.
Publicado: (2026)

DateSAT: A Framework for Solving Date and Period Constraints
por: Cui, Leyi, et al.
Publicado: (2026)

A denotationally-based program logic for higher-order store
por: Aagaard, Frederik Lerbjerg, et al.
Publicado: (2023)

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics
por: Soldevila, Mallku, et al.
Publicado: (2024)

JAX Autodiff from a Linear Logic Perspective (Extended Version)
por: Giusti, Giulia, et al.
Publicado: (2025)

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

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
por: Chen, Zhibo, et al.
Publicado: (2023)

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

A Program Logic for Under-approximating Worst-case Resource Usage
por: Jin, Ziyue, et al.
Publicado: (2025)

A Type System for Data Flow and Alias Analysis in ReScript
por: Lund, Nicky Ask, et al.
Publicado: (2024)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
por: Vollmer, Victoria, et al.
Publicado: (2024)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
por: Castagna, Giuseppe, et al.
Publicado: (2024)

Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors
por: Congard, Sidney, et al.
Publicado: (2025)

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

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

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
por: Kappé, Tobias, et al.
Publicado: (2023)

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

An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
por: Elad, Neta, et al.
Publicado: (2023)