Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
| Autor: | Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, Steve Zdancewic |
|---|---|
| Přispěvatelé: | Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure de Lyon (ENS de Lyon), Compilation et Analyse, Logiciel et Matériel (CASH), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Lyon, Institut National de Recherche en Informatique et en Automatique (Inria), University of Pennsylvania, Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Programming Languages [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Theory of computation → Denotational semantics Concurrency Nondeterminism CCS Concepts Interaction Trees Program verification Concurrency CCS Concepts: Theory of computation → Denotational semantics Program verification Concurrency Nondeterminism Safety Risk Reliability and Quality Software Formal Semantics Programming Languages (cs.PL) |
| Zdroj: | Proceedings of the ACM on Programming Languages Proceedings of the ACM on Programming Languages, 2023, pp.1-31. ⟨10.1145/3571254⟩ |
| ISSN: | 2475-1421 |
| Popis: | 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 computations into coinductive trees with three kind of nodes: external events, and two variants of nondeterministic branching. This apparent redundancy allows us to provide shallow embedding of denotational models with internal choice in the style of CCS, while recovering an inductive LTS view of the computation. ctrees inherit a vast collection of bisimulation and refinement tools, with respect to which we establish a rich equational theory. We connect ctrees to the itree infrastructure by showing how a monad morphism embedding the former into the latter permits to use ctrees to implement nondeterministic effects. We demonstrate the utility of ctrees by using them to model concurrency semantics in two case studies: CCS and cooperative multithreading. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|