Copertina

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Kappé, Tobias, Schmid, Todd, Silva, Alexandra
Natura:	Preprint
Pubblicazione:	2023
Soggetti:	Logic in Computer Science Programming Languages
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

A General Completeness Theorem for Skip-free Star Algebras
di: Kappé, Tobias, et al.
Pubblicazione: (2025)

An Elementary Proof of the FMP for Kleene Algebra
di: Kappé, Tobias
Pubblicazione: (2022)

A cyclic proof system for Guarded Kleene Algebra with Tests (full version)
di: Rooduijn, Jan, et al.
Pubblicazione: (2024)

Kleene Algebra
di: Kappé, Tobias, et al.
Pubblicazione: (2025)

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

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

Completeness of Finitely Weighted Kleene Algebra With Tests
di: Sedlár, Igor
Pubblicazione: (2024)

On Tools for Completeness of Kleene Algebra with Hypotheses
di: Pous, Damien, et al.
Pubblicazione: (2022)

Partial Reductions for Kleene Algebra with Linear Hypotheses
di: Chung, Liam, et al.
Pubblicazione: (2026)

Completions of Kleene's second model
di: Terwijn, Sebastiaan A.
Pubblicazione: (2023)

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

Almost-Sure Termination by Guarded Refinement
di: Gregersen, Simon Oddershede, et al.
Pubblicazione: (2024)

The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
di: Nakamura, Yoshiki
Pubblicazione: (2025)

Weighted GKAT: Completeness and Complexity
di: Van Koevering, Spencer, et al.
Pubblicazione: (2025)

Morita Rigidity for Kleene Algebras
di: Serafin, Luke
Pubblicazione: (2025)

Paraconsistent Relations as a Variant of Kleene Algebras
di: Cunha, Juliana, et al.
Pubblicazione: (2025)

An Introduction to Razborov's Flag Algebra as a Proof System for Extremal Graph Theory
di: Jeong, Gyeongwon, et al.
Pubblicazione: (2026)

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

Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog
di: Amato, Gianluca, et al.
Pubblicazione: (2024)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
di: Zilberstein, Noam, et al.
Pubblicazione: (2023)

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

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
di: Zilberstein, Noam, et al.
Pubblicazione: (2024)

Non-Cartesian Guarded Recursion with Daggers
di: Lemonnier, Louis
Pubblicazione: (2024)

FO-Complete Program Verification for Heap Logics
di: Murali, Adithya, et al.
Pubblicazione: (2026)

Complete first-order reasoning for functional programs
di: Murali, Adithya, et al.
Pubblicazione: (2026)

Complete Local Reasoning About Parameterized Programs Over Topologies
di: Cheng, Ruotong, et al.
Pubblicazione: (2026)

Expressivity of AuDaLa: Turing Completeness and Possible Extensions
di: Franken, Tom T. P., et al.
Pubblicazione: (2024)

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

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
di: Chatterjee, Krishnendu, et al.
Pubblicazione: (2024)

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

Verifying Lock-free Search Structure Templates
di: Patel, Nisarg, et al.
Pubblicazione: (2024)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
di: Elad, Neta, et al.
Pubblicazione: (2025)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
di: Zhang, Cheng, et al.
Pubblicazione: (2026)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
di: Klinkenberg, Lutz, et al.
Pubblicazione: (2023)

Words-to-Letters Valuations for Language Kleene Algebras with Variable and Constant Complements
di: Nakamura, Yoshiki, et al.
Pubblicazione: (2024)

Program Synthesis is $Σ_3^0$-Complete
di: Kim, Jinwoo
Pubblicazione: (2024)

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

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)
di: Batz, Kevin, et al.
Pubblicazione: (2024)

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

Verifying Peephole Rewriting In SSA Compiler IRs
di: Bhat, Siddharth, et al.
Pubblicazione: (2024)