Buchumschlag

Tachis: Higher-Order Separation Logic with Credits for Expected Costs

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Haselwarter, Philipp G., Li, Kwing Hei, de Medeiros, Markus, Gregersen, Simon Oddershede, Aguirre, Alejandro, Tassarotti, Joseph, Birkedal, Lars
Format:	Preprint
Veröffentlicht:	2024
Schlagworte:	Logic in Computer Science Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
von: Haselwarter, Philipp G., et al.
Veröffentlicht: (2026)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
von: Aguirre, Alejandro, et al.
Veröffentlicht: (2024)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
von: Haselwarter, Philipp G., et al.
Veröffentlicht: (2024)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
von: Li, Kwing Hei, et al.
Veröffentlicht: (2025)

Almost-Sure Termination by Guarded Refinement
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2024)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
von: Li, Kwing Hei, et al.
Veröffentlicht: (2025)

Logical Relations for Formally Verified Authenticated Data Structures
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2025)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
von: Timany, Amin, et al.
Veröffentlicht: (2021)

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
von: de Medeiros, Markus, et al.
Veröffentlicht: (2026)

Reasoning about Weak Isolation Levels in Separation Logic
von: Mathiasen, Anders Alnor, et al.
Veröffentlicht: (2025)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
von: Zilberstein, Noam, et al.
Veröffentlicht: (2024)

A Demonic Outcome Logic for Randomized Nondeterminism
von: Zilberstein, Noam, et al.
Veröffentlicht: (2024)

A denotationally-based program logic for higher-order store
von: Aagaard, Frederik Lerbjerg, et al.
Veröffentlicht: (2023)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory
von: Stassen, Philipp Jan Andries, et al.
Veröffentlicht: (2024)

Logical Predicates in Higher-Order Mathematical Operational Semantics
von: Goncharov, Sergey, et al.
Veröffentlicht: (2024)

Denotational Foundations for Expected Cost Analysis
von: de Amorim, Pedro H. Azevedo
Veröffentlicht: (2024)

Higher Order Automatic Differentiation of Higher Order Functions
von: Huot, Mathieu, et al.
Veröffentlicht: (2021)

Recursive Mutexes in Separation Logic
von: Du, Ke, et al.
Veröffentlicht: (2026)

Towards Concurrent Quantitative Separation Logic
von: Fesefeldt, Ira, et al.
Veröffentlicht: (2022)

A Nominal Approach to Probabilistic Separation Logic
von: Li, John M., et al.
Veröffentlicht: (2024)

Higher-Order Asynchronous Effects
von: Ahman, Danel, et al.
Veröffentlicht: (2023)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
von: Le, Quang Loc
Veröffentlicht: (2025)

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

Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
von: Leutgeb, Lorenz, et al.
Veröffentlicht: (2022)

Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
von: Accattoli, Beniamino
Veröffentlicht: (2022)

Bialgebraic Reasoning on Higher-Order Program Equivalence
von: Goncharov, Sergey, et al.
Veröffentlicht: (2024)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
von: Zilberstein, Noam, et al.
Veröffentlicht: (2023)

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
von: Bacci, Giorgio, et al.
Veröffentlicht: (2025)

Towards a Higher-Order Bialgebraic Denotational Semantics
von: Goncharov, Sergey, et al.
Veröffentlicht: (2026)

On Higher-Order Reachability Games vs May Reachability
von: Asada, Kazuyuki, et al.
Veröffentlicht: (2022)

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
von: Li, Runming, et al.
Veröffentlicht: (2025)

Inconsistent Ontology Handling by Translating Description Logics into Defeasible Logic Programming
von: Sergio Alejandro Gómez
Veröffentlicht: (2007)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
von: Grandury, Marcos, et al.
Veröffentlicht: (2025)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
von: Chirica, Ion, et al.
Veröffentlicht: (2025)

Kuroda's Translation for Higher-Order Logic
von: Traversié, Thomas
Veröffentlicht: (2024)

A Defeasible Logic Programming Approach to the Integration of Rules and Ontologies
von: Sergio Alejandro Gómez
Veröffentlicht: (2010)

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
von: Chen, Zhibo, et al.
Veröffentlicht: (2023)

Syntactic Effectful Realizability in Higher-Order Logic
von: Cohen, Liron, et al.
Veröffentlicht: (2025)

Bayesian Separation Logic
von: Ho, Shing Hin, et al.
Veröffentlicht: (2025)

Context-Dependent Effects and Concurrency in Guarded Interaction Trees
von: Stepanenko, Sergei, et al.
Veröffentlicht: (2025)