:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Séttimo, Agustín, Sottile, Cristian, Manzino, Cecilia
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Programming Languages
Online Access:	https://arxiv.org/abs/2603.23652
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Domain Reasoning in TopKAT
by: Zhang, Cheng, et al.
Published: (2024)

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)

A formal specification of the jq language
by: Färber, Michael
Published: (2024)

Strong normalization through idempotent intersection types: a new syntactical approach
by: Barenbaum, Pablo, et al.
Published: (2025)

Multi types and reasonable space
by: Accattoli, Beniamino, et al.
Published: (2022)

Simply typed convertibility is TOWER-complete even for safe lambda-terms
by: Nguyên, Lê Thành Dũng
Published: (2023)

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

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

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

Frex: dependently-typed algebraic simplification
by: Allais, Guillaume, et al.
Published: (2023)

Nominal techniques as an Agda library
by: Gabbay, Murdoch J., et al.
Published: (2026)

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

Multi-paradigm Logic Programming in the ${\cal E}$rgoAI System
by: Kifer, Michael, et al.
Published: (2026)

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

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
by: Matsuoka, Satoshi
Published: (2026)

When Agda met Vampire
by: Šinkarovs, Artjoms, et al.
Published: (2026)

A Practical Quantum Hoare Logic with Classical Variables, I
by: Ying, Mingsheng
Published: (2024)

A Formalization of Abstract Rewriting in Agda
by: Arkle, Sam, 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)

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)

Semantic Properties of Computations Defined by Elementary Inference Systems
by: Lucas, Salvador
Published: (2025)

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

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

An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory
by: Jeong, Gyeongwon, 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)

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)