D. Ahman, N. Ghani, and G. D. Plotkin, Dependent Types and Fibred Computational Effects, 19th International Conference on Foundations of Software Science and Computation Structures, vol.36, 2016.

G. Barthe, J. Hatcliff, M. Heine, and B. Sùrensen, CPS Translations and Applications: The Cube and Beyond, Higher Order Symbol. Comput, vol.12, pp.125-170, 1999.

J. , P. Bernardy, and M. Lasson, Realizability and Parametricity in Pure Type Systems, Foundations of Software Science and Computational Structures, vol.6604, pp.108-122, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00589893

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

S. Boulier, P. Pédrot, and N. Tabareau, The next 700 syntactical models of type theory, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01445835

W. Bowman, Y. Cong, N. Rioux, and A. Ahmed, Type-Preserving CPS Translation of ? and ? Types is Not Not Possible, Proceedings of the 45st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '18, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01672735

E. Brady, Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol.23, pp.552-593, 2013.

J. Breitner, Y. Spector-zabusky, C. Li, J. Rizkallah, S. Wiegley et al., Ready, Set, Verify! Applying hs-to-coq to Real-World Haskell Code (Experience Report), Proceedings of the ACM on Programming Languages, vol.2, p.16, 2018.

C. Casinghino, V. Sjöberg, and S. Weirich, Combining Proofs and Programs in a Dependently Typed Language, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014.

A. Chlipala, G. Malecha, G. Morrisett, A. Shinnar, and R. Wisnesky, Effective Interactive Proofs for Higher-order Imperative Programs, Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09), 2009.

J. Cockx and A. Abel, Sprinkles of Extensionality for Your Vanilla Type Theory, 22nd International Conference on Types for Proofs and Programs, 2016.

T. Coquand and G. P. Huet, The Calculus of Constructions, Inf. Comput, vol.76, issue.3, pp.90005-90008, 1988.
URL : https://hal.archives-ouvertes.fr/inria-00076024

G. Jaber, G. Lewertowski, P. Pédrot, M. Sozeau, and N. Tabareau, The Definitional Side of the Forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01319066

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML: A Verified Implementation of ML, Principles of Programming Languages (POPL), pp.179-191, 2014.

X. Leroy, S. Blazy, D. Kästner, B. Schommer, M. Pister et al., CompCert ? A Formally Verified Optimizing Compiler, ERTS 2016: Embedded Real Time Software and Systems. SEE, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01238879

P. Letouzey, Programmation fonctionnelle certifiée : l'extraction de programmes dans l'assistant Coq, 2004.

L. Paul-blain, Call-by-push-value, 2001.

A. Mahboubi and E. Tassi, Mathematical Components, 2008.

E. Moggi, Notions of Computation and Monads. Information and Computation, vol.93, issue.1, 1991.

A. Nanevski, G. Morrisett, and L. Birkedal, Hoare type theory, polymorphism and separation, Journal of Functional Programming, vol.18, pp.5-6, 2008.

, Dependently Typed Programming in Agda, Advanced Functional Programming, vol.5832, pp.230-266, 2008.

P. , M. Pédrot, and N. Tabareau, An effectful way to eliminate addiction to dependence, 32nd Annual Symposium on Logic in Computer Science, LICS 2017, 2017.

P. , M. Pédrot, and N. Tabareau, Failure is Not an Option -An Exceptional Type Theory, Proceedings of the 27th European Symposium on Programming Languages and Systems, vol.10801, pp.245-271, 2018.

, The Coq Proof Assistant Reference Manual, 2019.

J. C. Reynolds, Types, Abstraction and Parametric Polymorphism, 1983.

I. In and . Congress,

M. Sozeau and N. Oury, First-Class Type Classes, Proceedings of the 21st International Conference on Theorem Proving in Higher-Order Logics, pp.278-293, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00628864

N. Swamy, C. Hri?cu, C. Keller, A. Rastogi, A. Delignat-lavaud et al., Dependent Types and Multi-Monadic Effects in F*, 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 256?270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793

É. Tanter and N. Tabareau, Gradual Certified Programming in Coq, Proceedings of the 11th ACM Dynamic Languages Symposium, pp.26-40, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01238774

, Univalent Foundations Project. 2013. Homotopy Type Theory: Univalent Foundations for Mathematics

M. Vákár, A Framework for Dependent Types and Effects, 2015.

F. Wiedijk, Pollack-inconsistency, Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers (UITP10), vol.285, 2012.

H. Xi and F. Pfenning, Dependent Types in Practical Programming, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '99, pp.214-227, 1999.