Publications

Preprints

Completeness of Iris-Based Program Logics

2026

A generic framework for the completeness Iris program logics and the requisiteness of Iris WP assertion. Read more

Recommended citation: Johannes Hostert, Zichen Zhang, Puming Liu, Simon Oddershede Gregersen, Ralf Jung, and Joseph Tassarotti. 2026. Completeness of Iris-Based Program Logics. https://u8cat.github.io/files/complete.pdf
Download Paper | Download Bibtex

Building Extensible Program Logics through Effect Handlers

2025

This paper presents an approach for building extensible program logics based on effect handlers, and a relational logic for proving contextual refinements between programs using effects. Read more

Recommended citation: Zichen Zhang, Simon Oddershede Gregersen, and Joseph Tassarotti. 2025. Building Extensible Program Logics through Effect Handlers. https://u8cat.github.io/files/ficus.pdf
Download Paper | Download Bibtex