Author of the publication

Modular Denotational Semantics for Effects with Guarded Interaction Trees.

, , and . Proc. ACM Program. Lang., 8 (POPL): 332-361 (January 2024)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Fully abstract from static to gradual., , and . Proc. ACM Program. Lang., 5 (POPL): 1-30 (2021)Mechanized logical relations for termination-insensitive noninterference., , , and . Proc. ACM Program. Lang., 5 (POPL): 1-29 (2021)Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code., , , , , , and . J. ACM, 71 (1): 3:1-3:59 (2024)Category Theory in Coq 8.5., and . CoRR, (2015)Cumulative Inductive Types In Coq., and . FSCD, volume 108 of LIPIcs, page 29:1-29:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2018)Category Theory in Coq 8.5., and . FSCD, volume 52 of LIPIcs, page 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2016)Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic., , , , , and . CoRR, (2021)Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)., and . CoRR, (2017)The future is ours: prophecy variables in separation logic., , , , , , and . Proc. ACM Program. Lang., 4 (POPL): 45:1-45:32 (2020)The Logical Essence of Well-Bracketed Control Flow., , and . Proc. ACM Program. Lang., 8 (POPL): 575-603 (January 2024)