J. R. Abrial, The B-book: Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

S. F. Allen, R. L. Constable, D. J. Howe, and W. E. Aitken, The semantics of reflected proof, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.95-105, 1990.
DOI : 10.1109/LICS.1990.113737

B. H. Bloom, Space/time trade-offs in hash coding with allowable errors, Communications of the ACM, vol.13, issue.7, pp.422-426, 1970.
DOI : 10.1145/362686.362692

F. Bobot, J. C. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, The Why3 platform. LRI, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00822856

A. Charguéraud, Characteristic formulae for the verification of imperative programs, International Conference on Functional programming, pp.418-430, 2011.

D. Cock, G. Klein, and T. Sewell, Secure Microkernels, State Monads and Scalable Refinement, Theorem Proving in Higher Order Logics (TPHOL'08), pp.167-182, 2008.
DOI : 10.1145/358818.358825

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for Free!, pp.147-162, 2013.
DOI : 10.1007/978-3-319-03545-1_10
URL : https://hal.archives-ouvertes.fr/hal-01113453

B. Delaware, C. Pit-claudel, J. Gross, and A. Chlipala, Fiat: Deductive synthesis of abstract data types in a proof assistant, Principles of Programming Languages (POPL'15, pp.689-700, 2015.

M. Dénès, A. Mörtberg, and V. Siles, A refinement-based approach to computational algebra in Coq, Interactive Theorem Proving (ITP'12), pp.83-98, 2012.

J. C. Filliâtre, Verifying Two Lines of C with Why3: An Exercise in Program Verification, Verified Software: Theories, Tools, Experiments (VSTTE'12), pp.83-97, 2012.
DOI : 10.1145/360051.360224

A. Fox and M. Myreen, A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture, Interactive Theorem Proving (ITP'10), pp.243-258, 2010.
DOI : 10.1007/978-3-642-14052-5_18

G. Gonthier and A. Mahboubi, A small scale reflection extension for the Coq system, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

M. Hedberg, A coherence theorem for Martin-L??f's type theory, Journal of Functional Programming, vol.8, issue.4, pp.413-436, 1998.
DOI : 10.1017/S0956796898003153

A. Kennedy, N. Benton, J. B. Jensen, and P. E. Dagand, Coq, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.13-24, 2013.
DOI : 10.1145/2505879.2505897
URL : https://hal.archives-ouvertes.fr/hal-01081548

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

F. Mérillon, L. Réveilì-ere, C. Consel, R. Marlet, and G. Muller, Devil: an IDL for hardware programming, Symposium on Operating Systems Design and Implementation (OSDI'00), 2000.

G. C. Necula, Translation validation for an optimizing compiler, Conference on Programming Language Design and Implementation (PLDI'00, pp.83-94, 2000.

M. Richards, Backtracking algorithms in mcpl using bit patterns and recursion, 1997.

H. S. Warren, Hacker's Delight, 2012.