J. Abrial, The B-Book, assigning programs to meaning, 1996.

W. Ahrendt, B. Beckert, R. Bubel, R. Hähnle, P. H. Schmitt et al., Deductive Software Verification -The KeY Book -From Theory to Practice, Lecture Notes in Computer Science, vol.10001, 2016.

D. Ancona and E. Zucca, An algebraic approach to mixins and modularity, 5th Intl. Conf. on Algebraic and Logic Programming, number 1139 in Lecture Notes in Computer Science, pp.179-193, 1996.

H. Burton and . Bloom, Space/time trade-offs in hash coding with allowable errors, Commun. ACM, vol.13, issue.7, pp.422-426, 1970.

J. Chrzaszcz, Modules in Type Theory with Generative Definitions, 2004.

J. , C. Filliâtre, and A. Paskevich, Why3 -where programs meet provers, Proceedings of the 22nd European Symposium on Programming, vol.7792, pp.125-128, 2013.

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx et al., VeriFast: A powerful, sound, predictable, fast verifier for C and Java, NASA Formal Methods, vol.6617, pp.41-55, 2011.

J. Koenig, K. Rustan, and M. Leino, Programming language features for refinement, Proceedings 17th International Workshop on Refinement, Refine@FM, vol.209, pp.87-106, 2015.

K. and R. M. Leino, Dafny: An automatic program verifier for functional correctness, LPAR-16, vol.6355, pp.348-370, 2010.

K. Rustan, M. Leino, and D. Matichuk, Modular Verification Scopes via Export Sets and Translucent Exports, pp.185-202, 2018.

X. Leroy, A modular module system, Journal of Functional Programming, vol.10, issue.3, pp.269-303, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00073825

P. Louridas, Real-World Algorithms: A Beginner's Guide, 2017.

M. Mitzenmacher and E. Upfal, Probability and Computing: Randomized Algorithms and Probabilistic Analysis, 2005.

R. Rieu-helft, C. Marché, and G. Melquiond, How to get an efficient yet verified arbitrary-precision integer library, 9th Working Conference on Verified Software: Theories, Tools, and Experiments, vol.10712, pp.84-101, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01519732

N. Schärli, S. Ducasse, O. Nierstrasz, and A. P. Black, Traits: Composable units of behaviour, ECOOP 2003 -Object-Oriented Programming, pp.248-274, 2003.

M. Sozeau and N. Oury, First-Class Type Classes, 21th International Conference on Theorem Proving in Higher Order Logics, vol.5170, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00628864

P. Wadler and S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '89, pp.60-76, 1989.