:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Bernardi, Giovanni, Férée, Hugo, Lopez, Gaëtan
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Programming Languages
Online Access:	https://arxiv.org/abs/2605.02362
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

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

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

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

Mechanised uniform interpolation for modal logics K, GL, and iSL
by: Férée, Hugo, et al.
Published: (2024)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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