, Lemma check_term_if_impl: forall ctx exp ty, check_term_impl ctx (exp, ty) = true ? check_term ctx (exp, ty). Proof with eauto

, Lemma impl_if_check_term: forall ctx exp ty, check_term ctx (exp, ty) ? check_term_impl ctx (exp, ty) = true. Proof with eauto

, Lemma check_term_impl_correct: forall ctx exp ty, check_term ctx (exp, ty) ? check_term_impl ctx (exp, ty) = true. Proof with eauto. intros. split. apply check_term_if_impl. apply impl_if_check_term

S. Ailleret, Typage du bytecode Caml, Journées Françaises des Langages Applicatifs, JFLA02, vol.18, pp.43-60, 2002.

H. Aït-kaci and J. Garrigue, Label-Selective Lambda-Calculus Syntax and Confluence, vol.151, pp.353-383, 1995.

A. Florian-<octachron>, Escaped existential type, vol.105

B. E. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich, Engineering formal metatheory, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.127, p.24, 2008.

N. Benton, A. Kennedy, and G. Russell, Compiling standard ML to java bytecodes, Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), vol.17, 1998.

N. Benton, A. Kennedy, and C. V. Russo, Adventures in interoperability : the SML.NET experience, Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, vol.18, pp.215-226, 2004.

S. Blazy, Z. Dargaye, and X. Leroy, Formal verification of a C compiler front-end, FM 2006 : Int. Symp. on Formal Methods, tome 4085 de Lecture Notes in Computer Science, vol.20, pp.460-475, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00106401

S. Blazy and X. Leroy, Mechanized semantics for the Clight subset of the C language, Journal of Automated Reasoning, vol.43, issue.3, pp.263-288, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00352524

N. Govert-de-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem, INDAG. MATH, vol.34, pp.381-392, 1972.

E. Chailloux, G. Henry, and R. Montelatici, Mixing the Objective Caml and C# programming models in the .NET framework. CoRR, vol.18, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00145420

A. Charguéraud, Program verification through characteristic formulae, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, vol.19, pp.321-332, 2010.

A. Charguéraud, The locally nameless representation, J. Autom. Reasoning, vol.49, issue.3, p.10, 2012.

A. Charguéraud and F. Pottier, Locally nameless representation with cofinite quantification, vol.24, p.10

A. Charguéraud and F. Pottier, TLC : a non-constructive library for Coq

P. Cheng, R. Harper, J. G. Morrisett, L. Petersen, and C. A. Stone, The Design of the TILT Compiler for SML

P. Cheng, R. Harper, J. G. Morrisett, L. Petersen, and C. A. Stone, Tilt : standard ml compiler based on typed intermediate languages, p.14

A. Chlipala, Certified programming with dependent types -A pragmatic introduction to the Coq proof assistant, vol.3, pp.64-69, 2013.

D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn, A simple applicative language : mini-ml, LISP and Functional Programming, vol.21, pp.13-27, 1986.

G. Cousineau, P. Curien, and M. Mauny, The Categorical Abstract Machine, Science of Computer Programming, vol.8, pp.173-202, 1987.

L. Damas and R. Milner, Principal type-schemes for functional programs, Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, vol.23, pp.207-212, 1982.

Z. Dargaye, Vérification formelle d'un compilateur pour langages fonctionnels, vol.20, 2009.

. Stephen-<stdolan>-dolan, Segfault from bug in gadt/module typing, vol.104

D. Doligez and X. Leroy, A concurrent, generational garbage collector for a multithreaded implementation of ML, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.7, pp.113-123, 1993.
URL : https://hal.archives-ouvertes.fr/hal-01499969

C. Dubois, Proving ML type soundness within Coq, Theorem Proving in Higher Order Logics, 13th International Conference, vol.20, pp.126-144, 2000.

C. Dubois and V. Ménissier-morain, Certification of a type inference tool for ML : Damas-Milner within Coq, J. Autom. Reasoning, vol.23, issue.3-4, pp.319-346, 1999.

N. Stephen, J. C. Freund, and . Mitchell, A type system for the Java bytecode language and verifier, J. Autom. Reasoning, vol.30, issue.3-4, pp.271-321, 2003.

J. Garrigue, A certified implementation of ML with structural polymorphism and recursive types, Mathematical Structures in Computer Science, vol.25, issue.4, pp.867-891, 2015.

J. Garrigue, Programming with polymorphic variants, ML Workshop, tome 13, vol.7, 1998.

J. Garrigue, Relaxing the value restriction, The Third Asian Workshop on Programming Languages and Systems, APLAS'02, vol.88, pp.31-45, 2002.

J. Garrigue and . Didier-rémy, Ambivalent types for principal type inference with gadts, Programming Languages and Systems -11th Asian Symposium, vol.7, pp.257-272, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00914560

J. Girard, Interprétation fonctionnelle et élimination des coupures de l'arithmé-tique d'ordre supérieur, vol.21, 1972.

J. C. Michael, R. Gordon, L. Milner, M. C. Morris, C. P. Newey et al., A metalanguage for interactive proof in LCF, Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, vol.7, pp.119-130, 1978.

J. Gosling, B. Joy, G. Steele, G. Bracha, A. Buckley et al., Java SE 10 Edition. Oracle. Février, vol.17, 2018.

A. Guéneau, M. O. Myreen, R. Kumar, and M. Norrish, Verified characteristic formulae for cakeml, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.19, pp.584-610, 2017.

T. Hirschowitz, X. Leroy, and J. B. Wells, Compilation of extended recursion in callby-value functional languages, vol.115, 2009.

S. Kaes, Parametric overloading in polymorphic programming languages, ESOP '88, 2nd European Symposium on Programming, vol.14, pp.131-144, 1988.

O. Kiselyov, How OCaml type checker works -or what polymorphism and garbage collection have in common, vol.65, 2013.

O. Kiselyov, The design and implementation of BER metaocaml -system description, Functional and Logic Programming -12th International Symposium, FLOPS 2014, Kanazawa, vol.67, pp.86-102, 2014.

D. K. Lee, K. Crary, and R. Harper, Towards a mechanized metatheory of standard ML, Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.20, pp.173-184, 2007.

X. Leroy, A formally verified compiler back-end, Journal of Automated Reasoning, vol.43, issue.4, pp.363-446, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00360768

X. Leroy, A modular module system, J. Funct. Program, vol.10, issue.3, pp.269-303, 2000.
URL : https://hal.archives-ouvertes.fr/hal-01499946

X. Leroy, The ZINC experiment : an economical implementation of the ML language, INRIA, vol.18, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

T. Lindholm, F. Yellin, G. Bracha, and A. Buckley, The Java R Virtual Machine Specification, Java SE 10 Edition. Oracle. Février, vol.17, 2018.

M. Mauny, Compilation des Langages Fonctionnels dans les Combinateurs Catégo-riques -Application au langage ML, vol.7, 1985.

M. Mauny and A. Suárez, Implementing functional languages in the Categorical Abstract Machine, Proceedings of the ACM International Conference on Lisp and Functional Programming, vol.7, pp.266-278, 1986.

A. Middelkoop, A. Dijkstra, and S. D. Swierstra, A lean specification for gadts : system f with first-class equality proofs, Higher Order Symbol. Comput, vol.23, issue.2, pp.145-166

R. Milner, A theory of type polymorphism in programming, J. Comput. Syst. Sci, vol.17, issue.3, pp.348-375, 1978.

R. Milner, M. Tofte, and R. Harper, Definition of standard ML, vol.19, 1990.

R. Milner, M. Tofte, and R. Harper, Definition of standard ML (Revised), 1997.

R. Montelatici, Langages fonctionnels, typage et interopérabilité : Objective Caml sur .NET. (Functional languages, typing and interoperability : Objective Caml on .NET)

D. Thèse-de, , vol.18, 2007.

J. , G. Morrisett, D. Walker, K. Crary, and N. Glew, From system F to typed assembly language, ACM Trans. Program. Lang. Syst, vol.21, issue.3, pp.527-568, 1999.

M. O. Myreen and S. Owens, Proof-producing translation of higher-order logic into pure and stateful ML, J. Funct. Program, vol.24, issue.2-3, pp.284-315, 2014.

G. C. Necula, Proof-carrying code, Conference Record of POPL'97 : The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.18, pp.106-119, 1997.

L. Petersen, P. Cheng, R. Harper, and C. Stone, Implementing the TILT Internal Language. Rapport technique CMU-CS-00-180

J. Simon-peyton,

C. Benjamin and . Pierce, Types and programming languages, vol.113, 2002.

R. Porter, Top Gear : Ambitious but Rubbish : The Secrets Behind Top Gear's Craziest Creations, vol.7, pp.978-1849905039, 2012.

F. Pottier and . Didier-rémy, The essence of ML type inference, Advanced Topics in Types and Programming Languages, vol.10, pp.389-489, 2005.

D. Remy, Extension of ML Type System with a Sorted Equational Theory on Types

D. Rémy and J. Vouillon, Objective ML : an effective object-oriented extension to ML, TAPOS, vol.4, issue.1, pp.27-50, 1998.

M. Research, NET Standard. Microsoft. Août, 2018.

M. Sulzmann, M. T. Manuel, S. P. Chakravarty, K. Jones, and . Donnelly, System f with type equality coercions, Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, TLDI '07, pp.53-66, 2007.
DOI : 10.1145/1190315.1190324

Y. Tan, S. Owens, and R. Kumar, A verified type system for cakeml, Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL '15, vol.7, p.20, 2015.
DOI : 10.1145/2897336.2897344

URL : http://kar.kent.ac.uk/53891/1/ifl15a.pdf

D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper et al., Til : a type-directed, optimizing compiler for ml, SIGPLAN Not, vol.39, issue.4, pp.362-1340, 2004.
DOI : 10.21236/ada306265

URL : http://www.dtic.mil/dtic/tr/fulltext/u2/a306265.pdf

D. Tarditi, J. G. Morrisett, P. Cheng, C. A. Stone, R. Harper et al., TIL : A type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation (PLDI), vol.13, pp.181-192, 1996.
DOI : 10.21236/ada306265

URL : http://www.dtic.mil/dtic/tr/fulltext/u2/a306265.pdf

S. Weirich, J. Hsu, and R. A. Eisenberg, System FC with Explicit Kind Equality. SIGPLAN Not, vol.48, issue.9, pp.275-286

S. Weirich, D. Vytiniotis, S. P. Jones, and S. Zdancewic, Generative type abstraction and type-level computation, SIGPLAN Not, vol.46, issue.1, pp.227-240
DOI : 10.1145/1926385.1926411

URL : https://repository.upenn.edu/cgi/viewcontent.cgi?article=1598&context=cis_papers

P. Weis and X. Leroy, Le langage Caml. InterEditions, 1993. isbn, vol.7, pp.978-980

A. K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, vol.8, pp.343-355, 1995.
DOI : 10.1007/bf01018828

J. Yallop, A new check that 'let rec' bindings are well formed, vol.115