Cover Image

A denotationally-based program logic for higher-order store

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Aagaard, Frederik Lerbjerg, Sterling, Jonathan, Birkedal, Lars
Format:	Preprint
Published:	2023
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Unifying cubical and multimodal type theory
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2022)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

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

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
by: Haselwarter, Philipp G., et al.
Published: (2024)

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

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
by: Timany, Amin, et al.
Published: (2021)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
by: Stübinger, Terru, et al.
Published: (2023)

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

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
by: Aguirre, Alejandro, et al.
Published: (2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
by: Haselwarter, Philipp G., et al.
Published: (2024)

When is the partial map classifier a Sierpiński cone?
by: Pugh, Leoni, et al.
Published: (2025)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
by: Oda, Yukihiro
Published: (2025)

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

Controlling unfolding in type theory
by: Gratzer, Daniel, et al.
Published: (2022)

Checkpoint-based rollback recovery in session programming
by: Mezzina, Claudio Antares, et al.
Published: (2023)

Semantics out of context: nominal absolute denotations for first-order logic and computation
by: Gabbay, Murdoch J.
Published: (2013)

S4 modal sequent calculus as intermediate logic and intermediate language
by: Caspar, Jean, et al.
Published: (2026)

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

Making first order linear logic a generating grammar
by: Slavnov, Sergey
Published: (2022)

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

An Intermediate Program Representation for Optimizing Stream-Based Languages
by: Baumeister, Jan, et al.
Published: (2025)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
by: Hu, Jason Z. S., et al.
Published: (2024)

Higher-order bialgebraic semantics
by: Goncharov, Sergey, et al.
Published: (2024)

Context-Dependent Effects and Concurrency in Guarded Interaction Trees
by: Stepanenko, Sergei, et al.
Published: (2025)

Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics
by: Dvir, Yotam, et al.
Published: (2025)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory
by: Stassen, Philipp Jan Andries, et al.
Published: (2024)

Functional Array Programming in an Extended Pi-Calculus
by: Hüttel, Hans, 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)

Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
by: Ackerman, Nathanael L., et al.
Published: (2023)

HaliVer: Deductive Verification and Scheduling Languages Join Forces
by: Haak, Lars B. van den, et al.
Published: (2024)

A programming language combining quantum and classical control
by: Dave, Kinnari, et al.
Published: (2025)

Syntactically and semantically regular languages of lambda-terms coincide through logical relations
by: Moreau, Vincent, et al.
Published: (2023)

Complete and tractable machine-independent characterizations of second-order polytime
by: Hainry, Emmanuel, et al.
Published: (2022)

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

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
by: Powell, Thomas
Published: (2023)

Extended multi-adjoint logic programming
by: Cornejo, M. Eugenia, et al.
Published: (2024)

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

Defining implication relation for classical logic
by: Fu, Li
Published: (2013)