E. Moggi, Notions of computation and monads, Information and Computation, vol.93, issue.1, pp.55-92, 1991.
DOI : 10.1016/0890-5401(91)90052-4

P. Pédrot and N. Tabareau, An effectful way to eliminate addiction to dependence, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp.1-12, 2017.
DOI : 10.1109/LICS.2017.8005113

G. Munch-maccagnoni, Models of a Non-associative Composition, 17th International Conference on Foundations of Software Science and Computation Structures, pp.396-410, 2014.
DOI : 10.1007/978-3-642-54830-7_26
URL : https://hal.archives-ouvertes.fr/hal-00996729

G. Kreisel, Interpretation of analysis by means of constructive functionals of finite types, Constructivity in Mathematics, pp.101-128, 1959.

J. P. Bernardy and M. Lasson, Realizability and Parametricity in Pure Type Systems, pp.108-122, 2011.
DOI : 10.1016/j.tcs.2006.12.042
URL : https://hal.archives-ouvertes.fr/hal-00589893

J. Avigad and S. Feferman, Gödel's functional ("Dialectica") interpretation. In: The Handbook of Proof Theory, pp.337-405, 1999.

T. Coquand and B. Mannaa, The independence of Markov's principle in type theory, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, pp.1-1718, 2016.

T. Coquand and G. P. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

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, CPP 2017, pp.182-194, 2017.
DOI : 10.1109/LICS.1989.39193
URL : https://hal.archives-ouvertes.fr/hal-01445835

, The Coq Development Team: The Coq proof assistant reference manual, 2017.

B. Werner, Une Théorie des Constructions Inductives, 1994.

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

J. C. Reynolds, Types, abstraction and parametric polymorphism, In: IFIP Congress, pp.513-523, 1983.

H. Friedman, Classically and intuitionistically provably recursive functions, pp.21-27, 1978.
DOI : 10.1007/BFb0103100

A. Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol.344, 1973.
DOI : 10.1007/BFb0066739

H. Herbelin, An Intuitionistic Logic that Proves Markov's Principle, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.11-14
DOI : 10.1109/LICS.2010.49

, Edinburgh, United Kingdom, pp.50-56, 2010.

C. Keller and M. Lasson, Parametricity in an impredicative sort In: Computer Science Logic (CSL'12) -26th International Workshop, 21st Annual Conference of the EACSL, CSL 2012, pp.381-395, 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.
DOI : 10.1145/292540.292560

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, POPL '14, pp.33-45, 2014.
DOI : 10.1145/2535838.2535883

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), pp.256-270, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01265793

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, pp.36-54, 2016.
DOI : 10.1007/978-3-662-46678-0_7

M. Vákár, A framework for dependent types and effects (2015) draft

E. Brady, Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol.36, issue.05, pp.552-593, 2013.
DOI : 10.1017/S0956796803004829

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

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, pp.79-90, 2009.

G. Barthe, J. Hatcliff, and M. H. Sørensen, CPS translations and applications: The cube and beyond. Higher Order Symbol, Comput, vol.12, issue.2, pp.125-170, 1999.

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.
DOI : 10.1007/978-3-540-24725-8_20
URL : https://hal.archives-ouvertes.fr/hal-01672735

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, pp.367-376, 2016.
DOI : 10.1007/BFb0014566
URL : https://hal.archives-ouvertes.fr/hal-01319066

O. Kammar and M. Pretnar, Abstract, Journal of Functional Programming, vol.10, 2017.
DOI : 10.1016/j.entcs.2013.09.007