Choice trees: Representing nondeterministic, recursive, and impure programs in coq
This paper introduces ctrees, a monad for modeling nondeterministic, recursive, and impure
programs in Coq. Inspired by Xia et al.'s itrees, this novel data structure embeds …
programs in Coq. Inspired by Xia et al.'s itrees, this novel data structure embeds …
A two-phase infinite/finite low-level memory model: Reconciling integer–pointer casts, finite space, and undef at the llvm ir level of abstraction
C Beck, I Yoon, H Chen, Y Zakowski… - Proceedings of the ACM …, 2024 - dl.acm.org
This paper provides a novel approach to reconciling complex low-level memory model
features, such as pointer--integer casts, with desired refinements that are needed to justify …
features, such as pointer--integer casts, with desired refinements that are needed to justify …
Program adverbs and Tlön embeddings
Free monads (and their variants) have become a popular general-purpose tool for
representing the semantics of effectful programs in proof assistants. These data structures …
representing the semantics of effectful programs in proof assistants. These data structures …
Calculating compilers for concurrency
Choice trees have recently been introduced as a general structure for defining the semantics
of programming languages with a wide variety of features and effects. In this article we focus …
of programming languages with a wide variety of features and effects. In this article we focus …
A Two-Phase Infinite/Finite Low-Level Memory Model
C Beck, I Yoon, H Chen, Y Zakowski… - arXiv preprint arXiv …, 2024 - arxiv.org
This paper provides a novel approach to reconciling complex low-level memory model
features, such as pointer--integer casts, with desired refinements that are needed to justify …
features, such as pointer--integer casts, with desired refinements that are needed to justify …
Algebraic Effects Meet Hoare Logic in Cubical Agda
This paper presents a novel formalisation of algebraic effects with equations in Cubical
Agda. Unlike previous work in the literature that employed setoids to deal with equations, the …
Agda. Unlike previous work in the literature that employed setoids to deal with equations, the …
Monadic Interpreters for Concurrent Memory Models: Executable Semantics of a Concurrent Subset of LLVM IR
N Chappe, L Henrio, Y Zakowski - Proceedings of the 14th ACM …, 2025 - dl.acm.org
Monadic interpreters have gained attention as a powerful tool for modeling and reasoning
about first order languages. In particular in the Coq ecosystem, the Choice Tree (CTree) …
about first order languages. In particular in the Coq ecosystem, the Choice Tree (CTree) …
Monadic Interpreters for Concurrent Memory Models
N Chappe, L Henrio, Y Zakowski - CPP'25, 2025 - dl.acm.org
Monadic interpreters have gained attention as a powerful tool for modeling and reasoning
about first order languages. In particular in the Coq ecosystem, the Choice Tree (CTree) …
about first order languages. In particular in the Coq ecosystem, the Choice Tree (CTree) …
[PDF][PDF] MODULAR SEMANTICS AND METATHEORY FOR LLVM IR
E Yoon - 2023 - euisuny.github.io
With great computational power comes great responsibility. The history of computing
unveiled the cost of errors in safety-critical systems. In the 1980s, the Therac-25 radiation …
unveiled the cost of errors in safety-critical systems. In the 1980s, the Therac-25 radiation …
[PDF][PDF] Choice trees
Authors' addresses: Nicolas Chappe, Univ Lyon, EnsL, UCBL, CNRS, Inria, LIP, F-69342,
LYON Cedex 07, France, nicolas. chappe@ ens-lyon. fr; Paul He, University of …
LYON Cedex 07, France, nicolas. chappe@ ens-lyon. fr; Paul He, University of …