, 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
Typage du bytecode Caml, Journées Françaises des Langages Applicatifs, JFLA02, vol.18, pp.43-60, 2002. ,
Label-Selective Lambda-Calculus Syntax and Confluence, vol.151, pp.353-383, 1995. ,
Escaped existential type, vol.105 ,
Engineering formal metatheory, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.127, p.24, 2008. ,
Compiling standard ML to java bytecodes, Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), vol.17, 1998. ,
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. ,
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
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
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. ,
Mixing the Objective Caml and C# programming models in the .NET framework. CoRR, vol.18, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-00145420
Program verification through characteristic formulae, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, vol.19, pp.321-332, 2010. ,
The locally nameless representation, J. Autom. Reasoning, vol.49, issue.3, p.10, 2012. ,
Locally nameless representation with cofinite quantification, vol.24, p.10 ,
TLC : a non-constructive library for Coq ,
The Design of the TILT Compiler for SML ,
Tilt : standard ml compiler based on typed intermediate languages, p.14 ,
Certified programming with dependent types -A pragmatic introduction to the Coq proof assistant, vol.3, pp.64-69, 2013. ,
A simple applicative language : mini-ml, LISP and Functional Programming, vol.21, pp.13-27, 1986. ,
The Categorical Abstract Machine, Science of Computer Programming, vol.8, pp.173-202, 1987. ,
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. ,
Vérification formelle d'un compilateur pour langages fonctionnels, vol.20, 2009. ,
Segfault from bug in gadt/module typing, vol.104 ,
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
Proving ML type soundness within Coq, Theorem Proving in Higher Order Logics, 13th International Conference, vol.20, pp.126-144, 2000. ,
Certification of a type inference tool for ML : Damas-Milner within Coq, J. Autom. Reasoning, vol.23, issue.3-4, pp.319-346, 1999. ,
A type system for the Java bytecode language and verifier, J. Autom. Reasoning, vol.30, issue.3-4, pp.271-321, 2003. ,
A certified implementation of ML with structural polymorphism and recursive types, Mathematical Structures in Computer Science, vol.25, issue.4, pp.867-891, 2015. ,
Programming with polymorphic variants, ML Workshop, tome 13, vol.7, 1998. ,
Relaxing the value restriction, The Third Asian Workshop on Programming Languages and Systems, APLAS'02, vol.88, pp.31-45, 2002. ,
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
Interprétation fonctionnelle et élimination des coupures de l'arithmé-tique d'ordre supérieur, vol.21, 1972. ,
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. ,
, Java SE 10 Edition. Oracle. Février, vol.17, 2018.
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. ,
Compilation of extended recursion in callby-value functional languages, vol.115, 2009. ,
Parametric overloading in polymorphic programming languages, ESOP '88, 2nd European Symposium on Programming, vol.14, pp.131-144, 1988. ,
How OCaml type checker works -or what polymorphism and garbage collection have in common, vol.65, 2013. ,
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. ,
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. ,
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
A modular module system, J. Funct. Program, vol.10, issue.3, pp.269-303, 2000. ,
URL : https://hal.archives-ouvertes.fr/hal-01499946
The ZINC experiment : an economical implementation of the ML language, INRIA, vol.18, 1990. ,
URL : https://hal.archives-ouvertes.fr/inria-00070049
The Java R Virtual Machine Specification, Java SE 10 Edition. Oracle. Février, vol.17, 2018. ,
Compilation des Langages Fonctionnels dans les Combinateurs Catégo-riques -Application au langage ML, vol.7, 1985. ,
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 lean specification for gadts : system f with first-class equality proofs, Higher Order Symbol. Comput, vol.23, issue.2, pp.145-166 ,
A theory of type polymorphism in programming, J. Comput. Syst. Sci, vol.17, issue.3, pp.348-375, 1978. ,
Definition of standard ML, vol.19, 1990. ,
Definition of standard ML (Revised), 1997. ,
, Langages fonctionnels, typage et interopérabilité : Objective Caml sur .NET. (Functional languages, typing and interoperability : Objective Caml on .NET)
, , vol.18, 2007.
From system F to typed assembly language, ACM Trans. Program. Lang. Syst, vol.21, issue.3, pp.527-568, 1999. ,
Proof-producing translation of higher-order logic into pure and stateful ML, J. Funct. Program, vol.24, issue.2-3, pp.284-315, 2014. ,
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. ,
Implementing the TILT Internal Language. Rapport technique CMU-CS-00-180 ,
,
Types and programming languages, vol.113, 2002. ,
Top Gear : Ambitious but Rubbish : The Secrets Behind Top Gear's Craziest Creations, vol.7, pp.978-1849905039, 2012. ,
The essence of ML type inference, Advanced Topics in Types and Programming Languages, vol.10, pp.389-489, 2005. ,
Extension of ML Type System with a Sorted Equational Theory on Types ,
Objective ML : an effective object-oriented extension to ML, TAPOS, vol.4, issue.1, pp.27-50, 1998. ,
, NET Standard. Microsoft. Août, 2018.
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
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
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
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
, System FC with Explicit Kind Equality. SIGPLAN Not, vol.48, issue.9, pp.275-286
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
, Le langage Caml. InterEditions, 1993. isbn, vol.7, pp.978-980
Simple imperative polymorphism, Lisp and Symbolic Computation, vol.8, pp.343-355, 1995. ,
DOI : 10.1007/bf01018828
A new check that 'let rec' bindings are well formed, vol.115 ,