@inproceedings(cfml,
 author       = {Arthur Chargu\'{e}raud},
 year         = {2010},
 title        = {{Program Verification through Characteristic Formulae}},
 booktitle    = {Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming},
 series       = {ICFP '10},
 publisher    = {Association for Computing Machinery},
 address      = {New York, NY, USA},
 pages        = {321\IeC{\textendash}332},
 doi          = {10.1145/1863543.1863590},
)
@article(cfml2,
 author       = {Arthur Chargu{\'{e}}raud},
 year         = {2020},
 title        = {{Separation logic for sequential programs (functional pearl)}},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {4},
 number       = {{ICFP}},
 pages        = {116:1--116:34},
 doi          = {10.1145/3408998},
)
@inproceedings(why3,
 author       = {Jean-Christophe Filli\^atre and Andrei Paskevich},
 year         = {2013},
 title        = {{Why3 --- Where Programs Meet Provers}},
 editor       = {Matthias Felleisen and Philippa Gardner},
 booktitle    = {Proceedings of the 22nd European Symposium on Programming},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer},
 pages        = {125--128},
 doi          = {10.1007/978-3-642-37036-6_8},
)
@book(prog-in-sml,
 author       = {Robert Harper},
 year         = {2011},
 title        = {{Programming in Standard ML}},
 publisher    = {Licensed under the Creative Commons Attribution-Noncommercial-No Derivative Works 3.0},
)
@inproceedings(free-spec,
 author       = {Thomas Letan and R\'{e}gis-Gianas, Yann},
 year         = {2020},
 title        = {{FreeSpec: Specifying, Verifying, and Executing Impure Computations in Coq}},
 booktitle    = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 series       = {CPP 2020},
 publisher    = {Association for Computing Machinery},
 pages        = {32\IeC{\textendash}46},
 doi          = {10.1145/3372885.3373812},
)
@book(smldef,
 author       = {Robin Milner and Mads Tofte and David Macqueen},
 year         = {1997},
 title        = {{The Definition of Standard ML}},
 publisher    = {MIT Press},
 doi          = {10.7551/mitpress/2319.001.0001},
)
@inproceedings(ynot,
 author       = {Aleksandar Nanevski and Greg Morrisett and Avraham Shinnar and Paul Govereau and Lars Birkedal},
 year         = {2008},
 title        = {{Ynot: Dependent Types for Imperative Programs}},
 booktitle    = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
 series       = {ICFP '08},
 publisher    = {Association for Computing Machinery},
 pages        = {229\IeC{\textendash}240},
 doi          = {10.1145/1411204.1411237},
)
@article(eqtns,
 author       = {Matthieu Sozeau and Cyprien Mangin and P\IeC{\'e}drot, Pierre-Marie and Emilio Jes\IeC{\'u}s Gallego Arias and Ga\IeC{\"e}tan Gilbert and Robin Green and D\IeC{\'e}n\IeC{\`e}s, Maxime and Hugo Herbelin and Guillaume Claret and Siddharth and Enrico Tassi and Anton Trunov and Joachim Breitner and Antonio Nikishaev and SimonBoulier and N\IeC{\o}rb\IeC{\ae}k, S\IeC{\o}ren and Vincent Laporte and Yves Bertot},
 year         = {2020},
 title        = {{mattam82/Coq-Equations: Equations 1.2.3 for Coq 8.11}},
 doi          = {10.5281/zenodo.3967149},
)
@article(hs-to-coq,
 author       = {Spector-Zabusky, Antal and Joachim Breitner and Christine Rizkallah and Stephanie Weirich},
 year         = {2018},
 title        = {{Total Haskell is reasonable Coq}},
 journal      = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs - CPP 2018},
 doi          = {10.1145/3167092},
)
@inproceedings(fstar,
 author       = {Nikhil Swamy and Catalin Hritcu and Chantal Keller and Aseem Rastogi and Delignat-Lavaud, Antoine and Simon Forest and Karthikeyan Bhargavan and C\'{e}dric Fournet and Pierre-Yves Strub and Markulf Kohlweiss and Jean-Karim Zinzindohou\'e and {Zanella-B\'eguelin}, Santiago},
 year         = {2016},
 title        = {{Dependent Types and Multi-Monadic Effects in {F*}}},
 booktitle    = {43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
 publisher    = {ACM},
 pages        = {256--270},
 doi          = {10.1145/2837614.2837655},
)
@article(interaction-trees,
 author       = {Li-yao Xia and Yannick Zakowski and Paul He and Chung-Kil Hur and Gregory Malecha and Benjamin C. Pierce and Steve Zdancewic},
 year         = {2020},
 title        = {{Interaction trees: representing recursive and impure programs in Coq}},
 journal      = {Proceedings of the ACM on Programming Languages},
 volume       = {4},
 number       = {POPL},
 pages        = {1\IeC{\textendash}32},
 doi          = {10.1145/3371119},
)