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-46, 2014.
DOI : 10.1145/2535838.2535883

R. L. Constable, S. F. Allen, M. Bromley, R. Cleaveland, J. F. Cremer et al., Implementing mathematics with the Nuprl proof development system, 1986.

T. Coquand and G. 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

L. Damas and R. Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '82, pp.207-212, 1982.
DOI : 10.1145/582153.582176

J. Garrigue, Relaxing the Value Restriction, Functional and Logic Programming, pp.196-213, 2004.
DOI : 10.1007/978-3-540-24754-8_15

T. G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '90, pp.47-58, 1990.
DOI : 10.1145/96709.96714

R. Harper and M. Lillibridge, ML with callcc is unsound, 1991.

D. J. Howe, Equality in lazy computation systems, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.198-203, 1989.
DOI : 10.1109/LICS.1989.39174

P. Hyvernat, The size-change termination principle for constructor based languages, Logical Methods in Computer Science, vol.10, issue.1, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00547440

L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko et al., AURA: a programming language for authorization and audit, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.27-38, 2008.

J. Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, pp.199-207, 2007.
DOI : 10.1007/s10990-007-9018-9
URL : https://hal.archives-ouvertes.fr/hal-00154508

J. Krivine, Realizability in classical logic In: Interactive models of computation and program behaviour, Panoramas et synthèses, pp.197-229, 2009.

R. Lepigre, A realizability model for a semantical value restriction (2015), https

X. Leroy, Polymorphism by name for references and continuations, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '93, pp.220-231, 1993.
DOI : 10.1145/158511.158632
URL : https://hal.archives-ouvertes.fr/hal-01499970

X. Leroy and P. Weis, Polymorphic type inference and assignment, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.291-302, 1991.
DOI : 10.1145/99583.99622
URL : https://hal.archives-ouvertes.fr/hal-01499974

D. R. Licata and R. Harper, Positively dependent types, Proceedings of the 3rd workshop on Programming languages meets program verification, PLPV '09, pp.3-14, 2009.
DOI : 10.1145/1481848.1481851

P. Martin-löf, Constructive Mathematics and Computer Programming, Logic, Methodology and Philosophy of Science VI, Studies in Logic and the Foundations of Mathematics, pp.153-175, 1982.
DOI : 10.1016/S0049-237X(09)70189-2

N. P. Mendler, Recursive types and type constraints in second-order lambda calculus, Proceedings of the Symposium on Logic in Computer Science (LICS) 1987, pp.30-36, 1987.

A. Miquel, Le Calcul des Constructions Implicites : Syntaxe et Sémantique, 2001.

G. Munch-maccagnoni, Focalisation and Classical Realisability, 18th Annual Conference of the EACSL, pp.409-423, 2009.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00409793

U. Norell, Dependently Typed Programming in Agda, Lecture Notes from the Summer School in Advanced Functional Programming, 2008.

S. Owre, S. Rajan, J. Rushby, N. Shankar, and M. Srivas, PVS: Combining specification, proof checking, and model checking, Computer-Aided Verification, CAV '96 No. 1102 in Lecture Notes in Computer Science, pp.411-414, 1996.
DOI : 10.1007/3-540-61474-5_91

M. Parigot, ????-Calculus: An algorithmic interpretation of classical natural deduction, In: Lecture Notes in Computer Science, vol.624, pp.190-201, 1992.
DOI : 10.1007/BFb0013061

C. Raffalli, L'Arithmétiques Fonctionnelle du Second Ordre avec Points Fixes, 1994.

C. Raffalli, A normaliser for pure and typed ?-calculus, 1996.

C. Raffalli, The PML programming language, 2012.

N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan et al., Secure distributed programming with value-dependent types, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, pp.266-278, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00939188

M. Tofte, Type inference for polymorphic references, Information and Computation, vol.89, issue.1, pp.1-34, 1990.
DOI : 10.1016/0890-5401(90)90018-D

A. K. Wright, Simple imperative polymorphism, LISP and Symbolic Computation, pp.343-356, 1995.
DOI : 10.1007/BF01018828

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1994.
DOI : 10.1006/inco.1994.1093

H. Xi, Applied Type System (extended abstract), Proceedings of TYPES 2003, pp.394-408, 2004.

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