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

E. Brady, Programming and reasoning with algebraic effects and dependent types, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, pp.133-144, 2013.

E. Brady, Resource-Dependent Algebraic Effects, Trends in Functional Programming, pp.18-33, 2015.
DOI : 10.1007/978-3-319-14675-1_2

A. Chlipala, /. Ur, and . Web, A simple model for programming the web, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pp.153-165, 2015.

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, 1986.
DOI : 10.1016/0890-5401(88)90005-3

URL : https://hal.archives-ouvertes.fr/inria-00076024

D. Delahaye, A Tactic Language for the System Coq, Logic for Programming and Automated Reasoning, 7th International Conference Proceedings, pp.85-95, 1955.
DOI : 10.1007/3-540-44404-1_7

URL : https://hal.archives-ouvertes.fr/hal-01125070

S. Fowler and E. Brady, Dependent Types for Safe and Secure Web Programming, Proceedings of the 25th symposium on Implementation and Application of Functional Languages, IFL '13, p.49, 2013.
DOI : 10.1145/2620678.2620683

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

P. Hudak, S. P. Jones, and P. Wadler, Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.2), ACM SIGPLAN Notices, vol.27, issue.5, 1992.

I. Jacobson, M. Christerson, P. Jonsson, and G. Övergaard, Object-oriented software engineering -a use case driven approach, 1992.

J. Simon-peyton, Tackling the awkward squad: monadic input/output , concurrency, exceptions, and foreign-language calls in haskell, Engineering theories of software construction, pp.47-96, 2001.

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

P. Letouzey, Extraction in Coq: An Overview, Proceedings, pp.359-369, 2008.
DOI : 10.1007/978-3-540-69407-6_39

URL : https://hal.archives-ouvertes.fr/hal-00338973

G. Malecha, G. Morrisett, and R. Wisnesky, Trace-based verification of imperative programs with I/O, Journal of Symbolic Computation, vol.46, issue.2, pp.95-118, 2011.
DOI : 10.1016/j.jsc.2010.08.004

Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, 1992.
DOI : 10.1007/978-1-4612-0931-7

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

E. Moggi, Computational lambda-calculus and monads, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.14-23, 1989.
DOI : 10.1109/LICS.1989.39155

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot: Reasoning with the awkward squad, ACM SIGPLAN International Conference on Functional Programming, 2008.

U. Norell, Dependently typed programming in agda, Proceedings of TLDI'09, pp.1-2, 2009.

D. Gordon, M. Plotkin, and . Pretnar, Handlers of algebraic effects Held as Part of the Joint European Conferences on Theory and Practice of Software, Programming Languages and Systems, 18th European Symposium on Programming Proceedings, pp.80-94, 2009.

C. John and . Reynolds, Separation logic: A logic for shared mutable data structures, 17th IEEE Symposium on Logic in Computer Science, pp.22-25, 2002.

J. Vouillon, Lwt, Proceedings of the 2008 ACM SIGPLAN workshop on ML, ML '08, pp.3-12, 2008.
DOI : 10.1145/1411304.1411307

URL : https://hal.archives-ouvertes.fr/hal-00495983

P. Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '92, pp.1-14, 1992.
DOI : 10.1145/143165.143169