M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending coq with imperative features and its application to SAT verication, Interactive Theorem Proving, First International Conference, ITP 2010, vol.6172, p.8398, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.inria.fr/inria-00502496/file/fastcoq.pdf

F. Baader and T. Nipkow, Term rewriting and all that, 1998.

J. , O. Blech, and B. Grégoire, Certifying compilers using higherorder theorem provers as certicate checkers. Formal Methods in System Design, vol.38, p.3361, 2011.
DOI : 10.1007/s10703-010-0108-7

A. Bove and V. Capretta, Modelling general recursion in type theory, Mathematical Structures in Computer Science, vol.15, issue.4, p.671708, 2005.

A. Bove and V. Capretta, Computation by prophecy, Typed Lambda Calculi and Applications, 8th International Conference, vol.4583, pp.70-83, 2007.
DOI : 10.1007/978-3-540-73228-0_7

E. Brady, IDRIS : systems programming meets full dependent types, Proceedings of the 5th ACM Workshop Programming Languages meets Program Verication, p.4354, 2011.
DOI : 10.1007/978-3-319-15940-9_4

E. Brady, Idris, a general-purpose dependently typed programming language: Design and implementation, Journal of Functional Programming, vol.23, issue.5, p.552593, 2013.

E. Brady, Programming and reasoning with algebraic eects and dependent types, ACM SIGPLAN International Conference on Functional Programming, ICFP'13, p.133144, 2013.

E. Brady, Resource-dependent algebraic eects, Trends in Functional Programming-15th International Symposium, vol.8843, p.1833, 2014.

E. Brady and K. Hammond, Correct-by-construction concurrency: Using dependent types to verify implementations of eectful resource usage protocols, Fundamenta Informaticae, vol.102, issue.2, p.145176, 2010.

A. Charguéraud, Characteristic formulae for the verication of imperative programs, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, p.418430, 2011.

A. Chlipala, From network interface to multithreaded web applications: A case study in modular program verication, Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, p.609622, 2015.

A. Chlipala, Ur/web: A simple model for programming the web, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, p.153165, 2015.

A. Church, A set of postulates for the foundation of logic, Annals of Mathematics, vol.34, issue.4, p.839864, 1933.

K. Claessen, A poor man's concurrency monad, Journal of Functional Programming, vol.9, issue.3, p.313323, 1999.

G. Claret, L. Del-carmen-gonzález-huesca, Y. Régisgianas, and B. Ziliani, Lightweight proof by reection using a posteriori simulation of eectful computation, ITP, vol.7998, p.6783, 2013.

G. Claret and Y. Régis-gianas, Mechanical verication of interactive programs specied by use cases, 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE, p.6167, 2015.

T. Coquand and G. P. Huet, The calculus of constructions
URL : https://hal.archives-ouvertes.fr/inria-00076024

, Information and Computation, vol.76, issue.2/3, pp.90005-90008, 1988.

P. Corbineau, Autour de la clôture de congruence avec coq, 2001.

L. Damas and R. Milner, Principal type-schemes for functional programs, Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, p.207212, 1982.

D. Delahaye, Logic for Programming and Automated Reasoning, 7th International Conference, vol.1955, p.8595, 2000.

A. S. Elliott, A concurrency system for Idris and Erlang, 2015.

J. , C. Filliâtre, and A. Paskevich, Why3-where programs meet provers, Programming Languages and Systems-22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, vol.7792, p.125128, 1624.

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, p.49, 2013.

S. Glondu, Extraction certiée dans coq-en-coq, Vingtièmes Journées Francophones des Langages Applicatifs, p.383410, 2009.

G. Gonthier, The four colour theorem: Engineering of a formal proof, Computer Mathematics, 8th Asian Symposium, ASCM, vol.5081, p.333, 2007.

G. Gonthier, B. Ziliani, A. Nanevski, and D. Dreyer, How to make ad hoc proof automation less ad hoc

Z. Chakravarty, O. Hu, and . Danvy, Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, p.163175, 2011.

J. C. Michael, R. Gordon, C. P. Milner, . Wadsworth, and L. Edinburgh, Lecture Notes in Computer Science, vol.78, 1979.

B. Grégoire, L. Pottier, and L. Théry, Proof certicates for algebra and their application to automatic geometry theorem proving, Lecture Notes in Computer Science, vol.6301, p.4259, 2008.

J. Harrison, Metatheory and reection in theorem proving: A survey and critique, 1995.

M. Hentschel, R. Bubel, and R. Hähnle, Symbolic execution debugger (SED), Runtime Verication-5th International Conference, vol.8734, p.255262, 2014.

A. R. Charles and . Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, p.576580, 1969.

W. A. Howard, The Formulae-as-types Notion of Constructions, In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculs and Formalism, p.479490, 1980.

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

. Addison-wesley, , 1992.

W. H. Daniel, R. James, and . Hinze, A reection-based proof tactic for lattices in coq, Proceedings of the Tenth Symposium on Trends in Functional Programming, vol.10, p.97112, 2009.

J. Jourdan, V. Laporte, S. Blazy, X. Leroy, and D. Pichardie, A formally-veried C static analyzer, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.247259, 2015.

J. C. King, Symbolic execution and program testing, Communications of the ACM, vol.19, issue.7, p.385394, 1976.

D. Leijen and . Koka, Programming with row polymorphic eect types, Proceedings 5th Workshop on Mathematically Structured Functional Programming, vol.153, p.100126, 2014.

X. Leroy, Formal verication of a realistic compiler, Communications of the ACM, vol.52, issue.7, p.107115, 2009.

P. Letouzey, Extraction in coq: An overview, Arnold Beck
URL : https://hal.archives-ouvertes.fr/hal-00338973

, Logic and Theory of Algorithms, 4th Conference on Computability in Europe, vol.5028, p.359369, 2008.

S. Liang, P. Hudak, and M. P. Jones, Monad transformers and modular interpreters, Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, p.333343, 1995.

G. Malecha, G. Morrisett, and R. Wisnesky, Trace-based verication of imperative programs with I/O, Journal of Symbolic Computation, vol.46, issue.2, p.95118, 2011.

Z. Manna and A. Pnueli, The temporal logic of reactive and concurrent systems-specication, 1992.

R. Milner, M. Tofte, and R. Harper, Denition of standard ML, 1990.

E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), p.1423, 1989.
DOI : 10.1109/lics.1989.39155

A. Nanevski, P. Govereau, and G. Morrisett, Towards typetheoretic semantics for transactional concurrency, Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, p.7990, 2009.

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal, Ynot: dependent types for imperative programs, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, p.229240, 2008.

C. Newcombe, T. Rath, F. Zhang, B. Munteanu, M. Brooker et al., How amazon web services uses formal methods, Communications of the ACM, vol.58, issue.4, p.6673, 2015.

S. Peyton-jones, Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in haskell

M. Hoare, R. Broy, and . Steinbrueggen, Engineering Theories of Software Construction, NATO ASI Series, p.4796, 2000.

S. Peyton-jones, Beautiful concurrency, Beautiful Code: Leading Programmers Explain How They Think. O'Reilly Media, 2007.

D. Gordon, M. Plotkin, and . Pretnar, Handlers of algebraic eects, Programming Languages and Systems, p.18

, Held as Part of the Joint European Conferences on Theory and Practice of Software, vol.5502, p.8094, 2009.

C. Queinnec, Inverting back the inversion of control or, continuations versus page-centric programming, SIGPLAN Notices, vol.38, p.5764, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199504

J. C. Reynolds, Separation logic: A logic for shared mutable data structures, 17th IEEE Symposium on Logic in Computer Science (LICS 2002, p.5574, 2002.

D. Ricketts, V. Robert, D. Jang, Z. Tatlock, and S. Lerner, Automating formal proofs for reactive systems, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, p.452462, 2014.

I. Sergey, A. Nanevski, and A. Banerjee, Mechanized verication of ne-grained concurrent programs, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, p.7787, 2015.

I. Sergey, A. Nanevski, and A. Banerjee, Specifying and verifying concurrent algorithms with histories and subjectivity, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, vol.9032, p.333358, 2015.

S. Stéphane and . Somé, Formalization of textual use cases based on petri nets, International Journal of Software Engineering and Knowledge Engineering, vol.20, issue.5, p.695737, 2010.

M. Sozeau, Subset coercions in coq, Types for Proofs and Programs, International Workshop, vol.4502, p.237252, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00628869

M. Sozeau, Program-ing nger trees in coq, Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, p.1324, 2007.

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, vol.2, issue.42, p.230265, 1936.

R. J. Van-glabbeek and G. D. Plotkin, On CSP and the algebraic theory of eects

. Wood, , p.333369

. Springer, , 2010.

J. Vouillon, Lwt: a cooperative thread library, Proceedings of the ACM Workshop on ML, p.312, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00495983

P. Wadler, Comprehending monads, Mathematical Structures in Computer Science, vol.2, p.461493, 1992.
DOI : 10.1017/s0960129500001560
URL : https://www.pure.ed.ac.uk/ws/files/7944776/Comprehending_monads.pdf

P. M. Whitman, Free lattices, Annals of Mathematics, vol.42, issue.1, p.325330, 1941.

B. Ziliani and M. Sozeau, A unication algorithm for coq featuring universe polymorphism and overloading, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, vol.2015, p.179191, 2015.
DOI : 10.1145/2784731.2784751