T. Acar, C. Fournet, and D. Shumow, Design and verification of a cryptoagile distributed key manager, 2010.

A. W. Appel, Axiomatic bootstrapping: a guide for compiler hackers, ACM Transactions on Programming Languages and Systems, vol.16, issue.6, 1994.
DOI : 10.1145/197320.197336

M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, ITP, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

L. , A. Avijit, A. Datta, and R. Harper, Cayenne: A language with dependent types Distributed programming with distributed authorization, ICFP TLDI, 1998.
DOI : 10.1145/1708016.1708021
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.149.9360

A. Aydemir, B. C. Charguéraud, R. Pierce, S. Pollack, and . Weirich, Engineering formal metatheory, POPL, 2008.
DOI : 10.1145/1328438.1328443
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.5948

B. Barras, Sets in coq, coq in sets, J. Formalized Reasoning, 2010.

J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis, Refinement types for secure implementations, CSF, 2008.
DOI : 10.1145/1890028.1890031
URL : https://hal.archives-ouvertes.fr/hal-01294973

K. Bhargavan, R. Corin, P. Dénielou, C. Fournet, and J. Leifer, Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, 2009 22nd IEEE Computer Security Foundations Symposium, 2009.
DOI : 10.1109/CSF.2009.26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.187

K. Bhargavan, C. Fournet, and A. D. Gordon, Modular verification of security protocol code by typing, POPL, 2010.

C. Casinghino, H. D. Eades, G. Kimmell, V. Sjöberg, T. Sheard et al., The preliminary design of the Trellys core language, PLPV, 2011.

J. Chen, R. Chugh, and N. Swamy, Type-preserving compilation of end-toend verification of security enforcement, PLDI, 2010.

A. Chlipala, A verified compiler for an impure functional language, POPL, 2010.
DOI : 10.1145/1707801.1706312
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.2833

A. Chlipala, Ur: statically-typed metaprogramming with type-level record computation, 2010.

C. Colby, P. Lee, G. C. Necula, F. Blau, M. Plesko et al., A certifying compiler for Java, PLDI, 2000.
DOI : 10.1145/358438.349315
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.6143

J. Davis, A self-verifying theorem prover, 2009.

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, 2008.
DOI : 10.1007/978-3-540-78800-3_24

T. Dierks and E. Rescorla, The Transport Layer Security (TLS) Protocol Version 1, 2008.

T. Hart and M. Levin, The new compiler, 1962.

J. Jia, K. Vaughan, J. Mazurak, L. Zhao, J. Zarko et al., Aura: A programming language for authorization and audit, ICFP, 2008.

C. Keller and B. Werner, Importing HOL Light into Coq, ITP, 2010.
DOI : 10.1007/978-3-642-14052-5_22
URL : https://hal.archives-ouvertes.fr/inria-00520604

. Leroy, A locally nameless solution to the POPLmark challenge, Research report, vol.6098, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00123945

X. Leroy, The CompCert verified compiler, software and commented proof, 2011.
DOI : 10.1145/1111037.1111042

P. Letouzey, Extraction in Coq: An Overview, LTA '08, 2008.
DOI : 10.1007/978-3-540-69407-6_39
URL : https://hal.archives-ouvertes.fr/hal-00338973

S. Maffeis, M. Abadi, C. Fournet, and A. D. Gordon, Code-Carrying Authorization, ESORICS '08, 2008.
DOI : 10.1007/3-540-56610-4_62
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.140.9520

. Mcbride, Epigram: Practical Programming with Dependent Types, In Advanced Functional Programming School, 2004.
DOI : 10.1007/11546382_3

G. Morrisett, D. Walker, K. Crary, and N. Glew, From System F to typed assembly language, ACM Trans. Program. Lang. Syst, vol.21, issue.3, 1999.

M. O. Myreen and J. Davis, A Verified Runtime for a Verified Theorem Prover, Interactive Theorem Proving, 2011.
DOI : 10.1007/978-3-540-71067-7_6

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot: dependent types for imperative programs, ICFP, 2008.

. Pollack, How to Believe a Machine-Checked Proof, Twenty-Five Years of Constructive Type Theory, 1998.
DOI : 10.7146/brics.v4i18.18945

M. Sozeau, Equations: A Dependent Pattern-Matching Compiler, LNCS, p.6172, 2010.
DOI : 10.1007/978-3-642-14052-5_29
URL : https://hal.archives-ouvertes.fr/inria-00628862

A. Stump, M. Deters, A. Petcher, T. Schiller, and T. Simpson, Verified programming in Guru, Proceedings of the 3rd workshop on Programming languages meets program verification, PLPV '09, 2008.
DOI : 10.1145/1481848.1481856

N. Swamy, B. J. Corcoran, and M. Hicks, Fable: A Language for Enforcing User-defined Security Policies, 2008 IEEE Symposium on Security and Privacy (sp 2008), 2008.
DOI : 10.1109/SP.2008.29

N. Swamy, J. Chen, and R. Chugh, Enforcing Stateful Authorization and Information Flow Policies in Fine, ESOP, 2010.
DOI : 10.1007/978-3-642-11957-6_28

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan et al., Secure distributed programming with value-dependent types, ICFP, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00939188

H. Xi, Applied Type System, Types for Proofs and Programs, pp.394-408, 2003.
DOI : 10.1007/978-3-540-24849-1_25