Programmer avec des modules de première classe dans un langage noyau pourvu de sous-typage, sortes

Programmer avec des modules de première classedans un langage noyau pourvu de sous-typage,sortes singletons et types existentiels ouvertsSoutenance de thèseBenoît Montagusous la direction de Didier RémyÉcole Polytechnique — INRIA Paris-Rocquencourt, projet GalliumMercredi 15 décembre 2010Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 1 / 41MainWfprogWfterm I Complex projectsWftypeNormalizeEnvParser_utils AnswerAst_utils ModeLexerParserAst ErrorLocation Label VarMyString MyIntDependency graph of the Fzip typechecker.Modularity in software developmentToday’s software: big and complex projectsI Big projectsProject Lines of codeUnison (2.32.52) 27,000Coq (8.3) 193,000Objective Caml (3.12) 240,000Emacs (23.2) 1,200,000Mozilla Firefox (3.6) 3,101,000GCC (4.4.5) 3,800,000LibreOffice.org (3.2.99.3) 5,640,000Linux Kernel (2.6.36.1) 8,900,000From SLOCCount, rounded.Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 2 / 41Project Lines of codeUnison (2.32.52) 27,000Coq (8.3) 193,000Objective Caml (3.12) 240,000Emacs (23.2) 1,200,000Mozilla Firefox (3.6) 3,101,000GCC (4.4.5) 3,800,000LibreOffice.org (3.2.99.3) 5,640,000Linux Kernel (2.6.36.1) 8,900,000From SLOCCount, rounded.Modularity in software developmentToday’s software: big and complex projectsMainI Big projectsWfprogWfterm I Complex projectsWftypeNormalizeEnvParser_utils AnswerAst_utils ModeLexerParserAst ErrorLocation Label VarMyString ...