J. Abrial and J. Abrial, The B-Book: Assigning Programs to Meanings, 2005.

A. Anand, S. Boulier, C. Cohen, M. Sozeau, and N. Tabareau, Towards Certified Meta-Programming with Typed Template-Coq, Interactive Theorem Proving -9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC, vol.10895, pp.20-39, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01809681

H. Apfelmus, The operational package, 2010.

M. Barnett, M. Fähndrich, K. Rustan, M. Leino, P. Müller et al., Specification and verification: the Spec# experience, Commun. ACM, vol.54, pp.81-91, 2011.

A. Bauer and M. Pretnar, Programming with Algebraic Effects and Handlers, Journal of Logical and Algebraic Methods in Programming, vol.84, pp.108-123, 2015.

E. Brady, Resource-dependent algebraic effects, International Symposium on Trends in Functional Programming, pp.18-33, 2014.

A. Charguéraud, Characteristic formulae for the verification of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011.

J. Choi, M. Vijayaraghavan, B. Sherman, and A. Chlipala, Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification, Proceedings of the ACM on Programming Languages, vol.1, p.24, 2017.

J. Christiansen, S. Dylus, and N. Bunkenburg, Verifying effectful Haskell programs in Coq, Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, pp.125-138, 2019.

G. Claret and Y. Régis-gianas, Mechanical Verification of Interactive Programs Specified by Use Cases, Proceedings of the Third FME Workshop on Formal Methods in Software Engineering, pp.61-67, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01255107

F. Deremer and H. H. Kron, Programming-in-the-Large Versus Programming-in-the-Small, IEEE Trans. Software Eng, vol.2, issue.2, pp.80-86, 1976.

S. Dylus, J. Christiansen, and F. Teegen, One Monad to Prove Them All, Programming Journal, vol.3, 2019.

J. , C. Filliâtre, and A. Paskevich, Why3 -Where Programs Meet Provers, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, vol.7792, pp.125-128, 2013.

K. Cormac-flanagan, M. Rustan, M. Leino, G. Lillibridge, J. B. Nelson et al., PLDI 2002: Extended static checking for Java. SIGPLAN Notices, vol.48, pp.22-33, 2013.

H. Víctor, R. García, M. Monroy, and . Quintana, Web Attack Detection Using ID3, Toward Category-Level Object Recognition, vol.4170, pp.323-332, 2006.

D. Harel, On Folk Theorems, Commun. ACM, vol.23, pp.379-389, 1980.

, 2015. Mathematics of Program Construction -12th International Conference, MPC 2015, vol.9129, 2015.

. Inria, The Coq Proof Assistant

J. Kaiser, B. Ziliani, and R. Krebbers, Mtac2: typed tactics for backward reasoning in Coq, ICFP, vol.2, p.31, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01890511

O. Kiselyov and H. Ishii, Freer Monads, More Extensible Effects, In ACM SIGPLAN Notices, vol.50, pp.94-105, 2015.

N. Koh, Y. Li, Y. Li, L. Xia, L. Beringer et al.,

, From C to interaction trees: specifying, verifying, and testing a networked server, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019.

, , pp.234-248

K. and R. M. Leino, Accessible Software Verification with Dafny, IEEE Software, vol.34, pp.94-97, 2017.

T. Letan, Y. Régis-gianas, P. Chifflier, and G. Hiet, Modular Verification of Programs with Effects and Effects Handlers in Coq, 22st International Symposium on Formal Methods (FM 2018), 2018.
URL : https://hal.archives-ouvertes.fr/hal-01799712

P. Letouzey, Extraction in Coq: An Overview, Logic and Theory of Algorithms, 4th Conference on Computability in Europe, vol.5028, pp.359-369, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00338973

B. Liskov and J. M. Wing, A Behavioral Notion of Subtyping, ACM Trans. Program. Lang. Syst, vol.16, pp.1811-1841, 1994.

K. Maillard, D. Ahman, R. Atkey, G. Martínez, C. Hritcu et al., Dijkstra monads for all, ICFP, vol.3, pp.1-104, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02398919

B. Meyer, Applying "Design by Contract, IEEE Computer, vol.25, pp.40-51, 1992.

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot: Dependent Types for Imperative Programs, ACM Sigplan Notices, vol.43, pp.229-240, 2008.

P. David-lorge, A Technique for Software Module Specification with Examples (Reprint), Commun. ACM, vol.26, pp.75-78, 1983.

F. Pessaux, FoCaLiZe: inside an F-IDE, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01203501

M. Sozeau, Un environnement pour la programmation avec types dépendants, 2008.

M. Sozeau and N. Oury, Proceedings (Lecture Notes in Computer Science), Otmane Aït Mohamed, Theorem Proving in Higher Order Logics, 21st International Conference, vol.5170, pp.278-293, 2008.

W. Swierstra and T. Baanen, A predicate transformer semantics for effects (functional pearl), PACMPL, vol.3, 2019.

, Topics in Theoretical Computer Science -Second IFIP WG 1.8 International Conference, vol.10608, pp.91-105, 2017.

Y. Li-yao-xia, P. Zakowski, C. He, G. Hur, B. C. Malecha et al., Interaction Trees: Representing Recursive and Impure Programs in Coq, The 47th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '20, 2013.

B. Ziliani, D. Dreyer, R. Neelakantan, A. Krishnaswami, V. Nanevski et al., Mtac: a monad for typed tactic programming in Coq, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, pp.87-100, 2013.