2026
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. 2026. Building Extensible Program Logics through Effect Handlers. arXiv:2607.12642 [cs.LO]. doi:10.48550/arXiv.2607.12642
Download Paper | Download Bibtex
2026
A completeness theoerm for Iris logically atomic triples and a reformulation of several linearizability proof techniques in Iris. Read more
Recommended citation: Zichen Zhang, Simon Oddershede Gregersen, and Joseph Tassarotti. 2026. Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic. arXiv:2607.11435 [cs.LO]. doi:10.48550/arXiv.2607.11435
Download Paper | Download Bibtex
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. Proc. ACM Program. Lang. 10, ICFP, Article 284 (August 2026), 36 pages. doi:10.1145/3828682
Download Paper | Download Bibtex