Cover Image

A beginner guide to Iris, Coq and separation logic

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Dietrich, Elizabeth
Format:	Preprint
Published:	2021
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

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

Towards a Coq-verified Chain of Esterel Semantics
by: Berry, Gérard, et al.
Published: (2019)

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

First Steps Towards Probabilistic Iris: Harmonizing Independence, Conditioning, and Dynamic Heap Allocation
by: Lohse, Janine, et al.
Published: (2026)

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

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

A Graphical Interface for Category Theory Proofs in Coq
by: Chabassier, Luc
Published: (2025)

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

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

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)

Teaching Divisibility and Binomials with Coq
by: Boldo, Sylvie, et al.
Published: (2024)

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 Nominal Approach to Probabilistic Separation Logic
by: Li, John M., et al.
Published: (2024)

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

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)

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

A formalization of System I with type Top in Agda
by: Séttimo, Agustín, 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 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)

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 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)

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

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

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
by: Tang, Xichen
Published: (2025)

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

Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
by: Zilberstein, Noam
Published: (2024)

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

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