Algebraic Effects Meet Hoare Logic in Cubical Agda

Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu. Algebraic Effects Meet Hoare Logic in Cubical Agda. Proceedings of the ACM on Programming Languages, 8(POPL):1663-1695, January 2024. [doi]

Abstract

Abstract is missing.