Hyper Separation Logic (Artifact)

Zenodo (CERN European Organization for Nuclear Research) 2026 Open access

Read full text
Authors: Trayan Gospodinov, Peter Müller, Thibault Dardinier
DOI: 10.5281/zenodo.19091148
Cited by: 1

Abstract

This artifact supports the PLDI 2026 paper “Hyper Separation Logic.” It consists of an Isabelle/HOL mechanization that fully supports the formal claims made in the paper and a VirtualBox VM image with Ubuntu 24.04 that contains Isabelle 2025 and our mechanization.

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
18 March 2026