Author of the publication

Interaction trees: representing recursive and impure programs in Coq.

, , , , , , and . Proc. ACM Program. Lang., 4 (POPL): 51:1-51:32 (2020)

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

A type system for extracting functional specifications from memory-safe imperative programs., , , , , , , , , and 1 other author(s). Proc. ACM Program. Lang., 5 (OOPSLA): 1-29 (2021)Interaction trees: representing recursive and impure programs in Coq., , , , , , and . Proc. ACM Program. Lang., 4 (POPL): 51:1-51:32 (2020)Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq., , , , and . CoRR, (2022)An equational theory for weak bisimulation via generalized parameterized coinduction., , , and . CPP, page 71-84. ACM, (2020)The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability., , , , and . CoRR, (2018)Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq., , , , and . Proc. ACM Program. Lang., 7 (POPL): 1770-1800 (January 2023)Semantics for Noninterference with Interaction Trees., , , , and . ECOOP, volume 263 of LIPIcs, page 29:1-29:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2023)A simple soundness proof for dependent object types., , , and . Proc. ACM Program. Lang., 1 (OOPSLA): 46:1-46:27 (2017)Semantics for Noninterference with Interaction Trees (Artifact)., , , , and . Dagstuhl Artifacts Ser., 9 (2): 06:1-06:2 (2023)The Satisfiability of Word Equations: Decidable and Undecidable Theories., , , , and . RP, volume 11123 of Lecture Notes in Computer Science, page 15-29. Springer, (2018)