@article{xai2020-interaction-trees,
author = {Xia, Li-yao and Zakowski, Yannick and He, Paul and Hur, Chung-Kil and Malecha, Gregory and Pierce, Benjamin C. and Zdancewic, Steve},
title = {Interaction {T}rees: {R}epresenting {R}ecursive and {I}mpure {P}rograms in {C}oq},
year = {2019},
issue_date = {January 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {POPL},
url = {https://doi.org/10.1145/3371119},
doi = {10.1145/3371119},
journal = {Proc. ACM Program. Lang.},
month = dec,
articleno = {51},
numpages = {32},
keywords = {compiler correctness, coinduction, monads, Coq}
}