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