M. Pradel and K. Sen, The Good, the Bad, and the Ugly: An Empirical Study of Implicit Type Conversions in JavaScript, 29th European Conference on Object-Oriented Programming (ECOOP 2015). Ed. by John Tang Boyland, vol.37, pp.519-541, 2015.

P. Wadler, Comprehending Monads". In: Mathematical Structures in Computer Science, vol.2, issue.4, pp.461-493, 1992.

X. Yang, Finding and understanding bugs in C compilers, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.283-294, 2011.

A. Abel, Verifying haskell programs using constructive type theory, Proceedings of the ACM SIGPLAN Workshop on Haskell, pp.62-73, 2005.

J. Abrial and J. Abrial, The B-Book: Assigning Programs to Meanings, 2005.

H. Apfelmus, The operational package

A. Asperti, A new type for tactics

R. Atkey, Parameterised notions of computation, J. Funct. Program, vol.19, pp.335-376, 2009.

M. Barnett, Specification and verification: the Spec# experience, Commun. ACM, vol.54, pp.81-91, 2011.

A. Bauer and M. Pretnar, Programming with Algebraic Effects and Handlers, Journal of Logical and Algebraic Methods in Programming, vol.84, pp.108-123, 2015.

S. Olivier, A. W. Bélanger, and . Appel, Shrink fast correctly!, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, pp.49-60, 2017.

E. Brady, Resource-dependent algebraic effects, International Symposium on Trends in Functional Programming, pp.18-33, 2014.

J. Choi, Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification, Proceedings of the ACM on Programming Languages, vol.1, p.24, 2017.

G. Claret and . Coqchick,

G. Claret and Y. Régis-gianas,

G. Claret and Y. Régis-gianas, Mechanical Verification of Interactive Programs Specified by Use Cases, 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, pp.61-67, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01255107

G. Claret, Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation, Interactive Theorem Proving -4th International Conference, ITP 2013, vol.7998, pp.67-83, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00870110

B. Dobing and J. Parsons, Understanding the Role of Use Cases in UML: A Review and Research Agenda, J. Database Manag, vol.11, pp.28-36, 2000.

G. Dowek, Higher-Order Unification and Matching, Handbook of Automated Reasoning, pp.1009-1062, 2001.

S. Dylus, J. Christiansen, and F. Teegen, One Monad to Prove Them All, Programming Journal, vol.3, p.8, 2019.

C. Flanagan, Extended static checking for Java, SIGPLAN Notices, vol.48, pp.22-33, 2002.

L. Del and C. González-huesca, Incrementality and effect simulation in the simply typed lambda calculus. (Incrémentalité et simulation d'effets dans le lambda calcul simplement typé, 2015.

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

J. C. Michael and . Gordon, A Metalanguage for Interactive Proof in LCF, Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp.119-130, 1978.

T. Heyman, R. Scandariato, and W. Joosen, Reusable Formal Models for Secure Software Architectures, 2012 Joint Working IEEE/IFIP Conference on Software Architecture and European Conference on Software Architecture, WICSA/ECSA 2012, pp.41-50, 2012.

, Mathematics of Program Construction -12th International Conference, MPC 2015, vol.9129, 2015.

D. Jackson, Software Abstractions: Logic, Language and Analysis, 2012.

J. Kaiser, Mtac2: typed tactics for backward reasoning in Coq, vol.78, p.31, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01890511

O. Kiselyov and H. Ishii, Freer Monads, More Extensible Effects, ACM SIGPLAN Notices, vol.50, pp.94-105, 2015.

N. Koh, From C to interaction trees: specifying, verifying, and testing a networked server, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.234-248, 2019.

T. Letan, FreeSpec: a Compositional Reasoning Framework for the Coq Theorem Prover, 2018.

T. Letan, Specifying and Verifying Hardware-based Security Enforcement Mechanisms. (Spécifier et vérifier des stratégies d'application de politiques de sécurité s'appuyant sur des mécanismes matériels, 2018.
URL : https://hal.archives-ouvertes.fr/tel-01989940

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, pp.333-343, 1995.

B. Liskov and J. M. Wing, A Behavioral Notion of Subtyping, ACM Trans. Program. Lang. Syst, vol.16, pp.1811-1841, 1994.

, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019.

K. Maillard, Dijkstra Monads for All, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02398919

P. Melliès, Game Semantics and Program Verification, Dagstuhl Seminar Proceedings. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, vol.10252, 2010.

B. Meyer, Applying "Design by Contract, IEEE Computer, vol.25, pp.40-51, 1992.

R. Milner, LCF: A Way of Doing Proofs with a Machine, Mathematical Foundations of Computer Science 1979, Proceedings, 8th Symposium, vol.74, pp.146-159, 1979.

E. Moggi, Notions of Computation and Monads, Inf. Comput. 93, vol.1, pp.55-92, 1991.

A. Nanevski, Ynot: Dependent Types for Imperative Programs, ACM Sigplan Notices, vol.43, issue.9, pp.229-240, 2008.

M. Odersky and M. Zenger, Scalable component abstractions, Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2005, pp.41-57, 2005.

P. David-lorge, A Technique for Software Module Specification with Examples (Reprint), Commun. ACM, vol.26, issue.1, pp.75-78, 1983.

F. Pessaux, FoCaLiZe: inside an F-IDE, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01203501

L. Simon, P. Jones, and P. Wadler, Imperative Functional Programming, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.71-84, 1993.

J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, 17th IEEE Symposium on Logic in Computer Science (LICS 2002, pp.55-74, 2002.

T. Uustalu, Topics in Theoretical Computer Science -Second IFIP WG 1.8 International Conference, vol.10608, pp.91-105, 2017.

P. Wadler, Comprehending Monads". In: Mathematical Structures in Computer Science, vol.2, issue.4, pp.461-493, 1992.

L. Xia, Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress, 2019.

B. Ziliani, Interactive typed tactic programming in the Coq proof assistant, 2015.

A. Umut, R. Acar, and . Ley-wild, Advanced Functional Programming, 6th International School, Revised Lectures. Ed. by Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra, vol.5832, pp.1-38, 2008.

T. Altenkirch, N. Anders-danielsson, and N. Kraus, Partiality, Revisited -The Partiality Monad as a Quotient Inductive-Inductive Type". In: Foundations of Software Science and Computation Structures -20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10203, pp.534-549, 2017.

M. Alvarez-picallo and C. Ong, Change Actions: Models of Generalised Differentiation, Foundations of Software Science and Computation Structures -22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, vol.11425, pp.45-61, 2019.

Y. Cai, A theory of changes for higher-order languages: incrementalizing ?-calculi by static differentiation, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, pp.145-155, 2014.

Y. Chen, A. Umut, K. Acar, and . Tangwongsan, Functional programming for dynamic and large data with self-adjusting computation, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp.227-240, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01100337

P. Dagand, N. Tabareau, and É. Tanter, Foundations of dependent interoperability, J. Funct. Program, vol.28, p.9, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01629909

P. Dagand, N. Tabareau, and É. Tanter, Partial type equivalences for verified dependent interoperability, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, pp.298-310, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01328012

E. D. Demaine, J. Iacono, and S. Langerman, Retroactive data structures, In: ACM Trans. Algorithms, vol.3, p.13, 2007.

T. Ehrhard and L. Regnier, The differential lambda-calculus, In: Theor. Comput. Sci, vol.309, pp.1-41, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00150572

C. Elliott, The simple essence of automatic differentiation, PACMPL 2.ICFP, vol.70, p.29, 2018.

S. Finne and S. , Programming Reactive Systems in Haskell, Proceedings of the 1994 Glasgow Workshop on Functional Programming, pp.50-65, 1994.

P. G. Giarrusso, Optimizing and incrementalizing higher-order collection queries by AST transformation, 2018.

P. G. Giarrusso, Y. Régis-gianas, and P. Schuster, Incremental ? -Calculus in Cache-Transfer Style -Static Memoization by Program Transformation, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, vol.11423, pp.553-580, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02405864

G. Gilbert, Definitional proof-irrelevance without K, PACMPL 3.POPL, vol.3, p.28, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01859964

L. Del and C. González-huesca, Incrementality and effect simulation in the simply typed lambda calculus. (Incrémentalité et simulation d'effets dans le lambda calcul simplement typé, 2015.

A. Matthew, U. A. Hammer, and . Acar, Memory management for self-adjusting computation, Proceedings of the 7th International Symposium on Memory Management, pp.51-60, 2008.

R. Hinze and R. Paterson, Finger trees: a simple general-purpose data structure, J. Funct. Program, vol.16, issue.2, pp.197-217, 2006.

P. Jaillet, R. Michael, and . Wagner, Online Optimization, 2012.

. Janestreet, The incremental library for self-adjusting computations in OCaml

J. Lambek, Cartesian Closed Categories and Typed Lambda-calculi, Combinators and Functional Programming Languages, vol.242, pp.136-175, 1985.

R. Ley-wild, U. A. Acar, and M. Fluet, A cost semantics for self-adjusting computation, 2009.

A. Yanhong, S. D. Liu, T. Stoller, and . Teitelbaum, Static Caching for Incremental Computation, In: ACM Trans. Program. Lang. Syst, vol.20, pp.546-585, 1998.

A. Nanevski, F. Pfenning, and B. Pientka, Contextual modal type theory, ACM Trans. Comput. Log, vol.9, p.49, 2008.

F. Pottier, Static Name Control for FreshML, 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), pp.356-365, 2007.

M. Puech, Certificates for Incremental Type Checking, 2013.

Y. Régis, -. , and F. Pottier, A Hoare Logic for Call-by-Value Functional Programs, Mathematics of Program Construction, 9th International Conference, vol.5133, pp.305-335, 2008.

A. Sabry and M. Felleisen, Reasoning about Programs in Continuation-Passing Style, Lisp and Symbolic Computation, vol.6, pp.289-360, 1993.

T. Uustalu and N. Veltri, Partiality and Container Monads". In: Programming Languages and Systems -15th Asian Symposium, vol.10695, pp.406-425, 2017.

H. Xi, Dependent ML An approach to practical programming with dependent types, J. Funct. Program, vol.17, pp.215-286, 2007.

A. Bacchelli and C. Bird, Expectations, outcomes, and challenges of modern code review, Proceedings of the 2013 international conference on software engineering, pp.712-721, 2013.

G. Barthe, J. M. Crespo, and C. Kunz, Beyond 2-safety: Asymmetric product programs for relational program verification, International Symposium on Logical Foundations of Computer Science, pp.29-43, 2013.

G. Barthe, J. M. Crespo, and C. Kunz, Product programs and relational program logics, J. Log. Algebr. Meth. Program, vol.85, pp.847-859, 2016.

G. Barthe, Coupling proofs are probabilistic product programs, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, pp.161-174, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01649028

K. Beck, Test Driven Development. By Example, 2002.

N. Benton, Simple relational correctness proofs for static analyses and program transformations, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.14-25, 2004.

N. Benton, Simple Relational Correctness Proofs for Static Analyses and Program Transformations (Revised, Long Version), 2005.

. Circle-ci,

A. Edmundson, An empirical study on the effectiveness of security code review, International Symposium on Engineering Secure Software and Systems, pp.197-212, 2013.

J. , C. Filliâtre, and A. Paskevich, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, vol.7792, pp.125-128, 2013.

T. Girka, D. Mentré, and Y. Régis-gianas, A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences, International Symposium on Automated Technology for Verification and Analysis, pp.64-79, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01238704

T. Girka, D. Mentré, and Y. Régis-gianas, Verifiable semantic difference languages, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, pp.73-84, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01653283

, GitLab

C. Hawblitzel, Mutual Summaries: Unifying Program Comparison Techniques

J. Hunt, An algorithm for differential file comparison

C. Le-goues, K. Rustan, M. Leino, and M. Moskal, The Boogie Verification Debugger (Tool Paper)". In: Software Engineering and Formal Methods -9th International Conference, SEFM 2011, vol.7041, pp.407-414, 2011.

K. and R. M. Leino, Program proving using intermediate verification languages (IVLs) like boogie and why3, Proceedings of the 2012 ACM Conference on High Integrity Language Technology, HILT '12, pp.25-26, 2012.

S. Mcintosh, The impact of code review coverage and code review participation on software quality: A case study of the qt, vtk, and itk projects, Proceedings of the 11th Working Conference on Mining Software Repositories, pp.192-201, 2014.

S. Panichella, Would static analysis tools help developers with code reviews?, In: 2015 IEEE 22nd International Conference on Software Analysis, Evolution and Reengineering (SANER), pp.161-170, 2015.

N. Partush and E. Yahav, Abstract Semantic Differencing for Numerical Programs, Static Analysis Symposium, vol.7935, pp.238-258, 2013.

N. Partush and E. Yahav, Abstract semantic differencing via speculative correlation, ACM SIGPLAN Notices, vol.49, issue.10, pp.811-828, 2014.

S. Person, Differential symbolic execution, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, pp.226-237, 2008.

C. Mcmillan, Differential Assertion Checking, pp.8-2013

, The Most Frequent Commit Messages on GitHub are Mostly Useless

. Travis-ci,

M. Andreas, B. Abel, and . Pientka, Wellfounded recursion with copatterns: A unified approach to termination and productivity, 18th ACM SIGPLAN International Conference on Functional Programming, vol.48, pp.185-196, 2013.

A. Abel, Copatterns: programming infinite structures by observations, ACM SIGPLAN conference on Principle of Programming Languages, vol.48, pp.27-38, 2013.

, Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt, 2012.

A. Doumane, On the infinitary proof theory of logics with fixed points. (Théorie de la démonstration infinitaire pour les logiques à points fixes, 2017.
URL : https://hal.archives-ouvertes.fr/tel-01676953

P. Downen, Codata in Action, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, vol.11423, pp.119-146, 2019.

C. Hur, The power of parameterization in coinductive proof, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.193-206, 2013.

J. Jeannin, D. Kozen, and A. Silva, CoCaml: Functional Programming with Regular Coinductive Types, Fundamenta Informaticae, vol.150, pp.347-377, 2017.

P. Laforgue and Y. Régis-gianas, Copattern matching and first-class observations in OCaml, with a macro, Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, pp.97-108, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01653261

, Dependently Typed Programming in Agda, 4th International Workshop on Types in Language Design and Implementation. TLDI '09, pp.1-2, 2009.

Y. Régis, -. , and F. Pottier, A Hoare Logic for Call-by-Value Functional Programs, Mathematics of Program Construction, 9th International Conference, vol.5133, pp.305-335, 2008.

A. Setzer, Unnesting of copatterns, International Conference on Rewriting Techniques and Applications, pp.31-45, 2014.

M. Sozeau, Equations: A Dependent Pattern-Matching Compiler, Interactive Theorem Proving, First International Conference, ITP 2010, vol.6172, pp.419-434, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00628862

D. Thibodeau, A. Cave, and B. Pientka, Indexed codata types, 21st ACM SIGPLAN International Conference on Functional Programming, pp.351-363, 2016.

H. Xi, C. Chen, and G. Chen, Guarded recursive datatype constructors, Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.224-235, 2003.

A. Bonenfant, Worst-Case Execution Times for a Purely Functional Language, Implementation and Application of Functional Languages, 18th International Symp osium, vol.4449, pp.235-252, 2006.

A. Guéneau, A. Charguéraud, and F. Pottier, A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10801, pp.533-560, 2018.

X. Leroy, Formal verification of a realistic compiler, Commun. ACM, vol.52, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

J. Marion, Developments in implicit computational complexity, Inf. Comput, pp.1-2, 2015.

Y. Régis, -. , and F. Pottier, A Hoare Logic for Call-by-Value Functional Programs, Mathematics of Program Construction, 9th International Conference, vol.5133, pp.305-335, 2008.

D. Sands, Complexity Analysis for a Lazy Higher-Order Language, ESOP'90, 3rd European Symposium on Programming, vol.432, pp.361-376, 1990.

H. Theiling, C. Ferdinand, and R. Wilhelm, Fast and Precise WCET Prediction by Separated Cache and Path Analyses, Real-Time Systems, vol.18, pp.157-179, 2000.

P. Tranquilli, Indexed Labels for Loop Iteration Dependent Costs, Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, vol.117, pp.19-33, 2013.

P. Wadler, Comprehending Monads". In: Mathematical Structures in Computer Science, vol.2, issue.4, pp.461-493, 1992.

. Wikipedia and . Intel-mcs-51,

R. Wilhelm, The worst-case execution-time problem -overview of methods and survey of tools, ACM Trans. Embedded Comput. Syst, vol.7, issue.3, p.53, 2008.

B. Zhan and M. P. Haslbeck, Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle, Automated Reasoning -9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC, vol.10900, pp.532-548, 2018.

L. A. Jan and . Van-de-snepscheut,

J. Abramatic, R. D. Cosmo, and S. Zacchiroli, Building the universal archive of source code, Communications of the ACM, vol.61, pp.29-31, 2018.
URL : https://hal.archives-ouvertes.fr/hal-02157125

A. Afroozeh and A. Izmaylova, Iguana: a practical data-dependent parsing framework, Proceedings of the 25th International Conference on Compiler Construction, pp.267-268, 2016.

A. V. Aho, Compilers: Principles, Techniques, and Tools, 2006.

J. Aycock, Practical earley parsing, The Computer Journal, vol.45, pp.620-630, 2002.

J. Aycock and R. Horspool, Schrödinger's token, In: Softw., Pract. Exper, vol.31, pp.803-814, 2001.

G. J. Mark, . Van-den, and . Brand, The asf+sdf meta-environment: A component-based language development environment, International Conference on Compiler Construction, pp.365-370, 2001.

M. Debian-policy,

J. Earley, An efficient context-free parsing algorithm, Communications of the ACM, vol.13, pp.94-102, 1970.

A. Izmaylova, A. Afroozeh, T. Van-der, and . Storm, Practical, general parser combinators, Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp.1-12, 2016.

N. Jeannerod, C. Marché, and R. Treinen, A Formally Verified Interpreter for a Shell-Like Programming Language, Verified Software. Theories, Tools, and Experiments -9th International Conference, vol.10712, pp.1-18, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01534747

N. Jeannerod and R. Treinen, Deciding the First-Order Theory of an Algebra of Feature Trees with Updates, Automated Reasoning -9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC, vol.10900, pp.439-454, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01807474

C. Steven and . Johnson, Yacc: Yet Another Compiler Compiler, UNIX Programmer's Manual, vol.2, pp.353-387, 1978.

E. Donald and . Knuth, On the translation of languages from left to right, Information and control, vol.8, issue.6, pp.607-639, 1965.

D. Pager, A practical general method for constructing LR (k) parsers, Acta Informatica, vol.7, pp.249-268, 1977.

F. Pottier and Y. Régis-gianas, The Menhir parser generator

, Maintainer script flowcharts

Y. Régis-gianas, N. Jeannerod, and R. Treinen, Morbig: a static parser for POSIX shell, Proceedings of the 11th ACM SIGPLAN International Conference on Software Language Engineering, pp.29-41, 2018.

E. Scott and A. Johnstone, GLL parsing, Electronic Notes in Theoretical Computer Science, vol.253, pp.177-189, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00722878

P. Stansifer and M. Wand, Parsing reflective grammars, Proceedings of the Eleventh Workshop on Language Descriptions, Tools and Applications, p.10, 2011.

M. Tomita and S. Ng, The generalized LR parsing algorithm, Generalized LR parsing, pp.1-16, 1991.

E. Visser, Scannerless generalized-LR parsing, 1997.