Programmer avec des modules de première classe dans un langage noyau  pourvu de sous-typage, sortes
100 Pages
English
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

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

-

Downloading requires you to have access to the YouScribe library
Learn all about the services we offer
100 Pages
English

Description

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 ...

Subjects

Informations

Published by
Reads 20
Language English

Exrait

Programmer avec des modules de première classe
dans un langage noyau pourvu de sous-typage,
sortes singletons et types existentiels ouverts
Soutenance de thèse
Benoît Montagu
sous la direction de Didier Rémy
École Polytechnique — INRIA Paris-Rocquencourt, projet Gallium
Mercredi 15 décembre 2010
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 1 / 41Main
Wfprog
Wfterm I Complex projects
Wftype
Normalize
Env
Parser_utils Answer
Ast_utils Mode
Lexer
Parser
Ast Error
Location Label Var
MyString MyInt
Dependency graph of the Fzip typechecker.
Modularity in software development
Today’s software: big and complex projects
I Big projects
Project Lines of code
Unison (2.32.52) 27,000
Coq (8.3) 193,000
Objective Caml (3.12) 240,000
Emacs (23.2) 1,200,000
Mozilla Firefox (3.6) 3,101,000
GCC (4.4.5) 3,800,000
LibreOffice.org (3.2.99.3) 5,640,000
Linux Kernel (2.6.36.1) 8,900,000
From SLOCCount, rounded.
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 2 / 41Project Lines of code
Unison (2.32.52) 27,000
Coq (8.3) 193,000
Objective Caml (3.12) 240,000
Emacs (23.2) 1,200,000
Mozilla Firefox (3.6) 3,101,000
GCC (4.4.5) 3,800,000
LibreOffice.org (3.2.99.3) 5,640,000
Linux Kernel (2.6.36.1) 8,900,000
From SLOCCount, rounded.
Modularity in software development
Today’s software: big and complex projects
Main
I Big projects
Wfprog
Wfterm I Complex projects
Wftype
Normalize
Env
Parser_utils Answer
Ast_utils Mode
Lexer
Parser
Ast Error
Location Label Var
MyString MyInt
Dependency graph of the Fzip typechecker.
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 2 / 41Project Lines of code
Unison (2.32.52) 27,000
Coq (8.3) 193,000
Objective Caml (3.12) 240,000
Emacs (23.2) 1,200,000
Mozilla Firefox (3.6) 3,101,000
GCC (4.4.5) 3,800,000
LibreOffice.org (3.2.99.3) 5,640,000
Linux Kernel (2.6.36.1) 8,900,000
From SLOCCount, rounded.
Modularity in software development
Today’s software: big and complex projects
Main
I Big projects
Wfprog
Wfterm I Complex projects
Wftype
NormalizeSoftware developments needs:
Env
I isolation of independent components;
Parser_utils Answer
I reusability of generic components.
Ast_utils Mode
Lexer
Parser
Ast Error
Location Label Var
MyString MyInt
Dependency graph of the Fzip typechecker.
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 2 / 41I Functors: parametrized modules Generic libraries
I Abstract types Isolation of components
I Hierarchical composition Namespace management
I Extensible structures Ease of use
I Type definitions Concision
Ingredients Features
ML modules
Key features
The ML module language
I Similar to compilation units, but more powerful
I A language on top of the ML language
I Can be adapted to any other
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 3 / 41I Abstract types Isolation of components
I Hierarchical composition Namespace management
I Extensible structures Ease of use
I Type definitions Concision
ML modules
Key features
The ML module language
I Similar to compilation units, but more powerful
I A language on top of the ML language
I Can be adapted to any other
Ingredients Features
I Functors: parametrized modules Generic libraries
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 3 / 41I Hierarchical composition Namespace management
I Extensible structures Ease of use
I Type definitions Concision
ML modules
Key features
The ML module language
I Similar to compilation units, but more powerful
I A language on top of the ML language
I Can be adapted to any other
Ingredients Features
I Functors: parametrized modules Generic libraries
I Abstract types Isolation of components
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 3 / 41I Extensible structures Ease of use
I Type definitions Concision
ML modules
Key features
The ML module language
I Similar to compilation units, but more powerful
I A language on top of the ML language
I Can be adapted to any other
Ingredients Features
I Functors: parametrized modules Generic libraries
I Abstract types Isolation of components
I Hierarchical composition Namespace management
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 3 / 41I Type definitions Concision
ML modules
Key features
The ML module language
I Similar to compilation units, but more powerful
I A language on top of the ML language
I Can be adapted to any other
Ingredients Features
I Functors: parametrized modules Generic libraries
I Abstract types Isolation of components
I Hierarchical composition Namespace management
I Extensible structures Ease of use
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 3 / 41ML modules
Key features
The ML module language
I Similar to compilation units, but more powerful
I A language on top of the ML language
I Can be adapted to any other
Ingredients Features
I Functors: parametrized modules Generic libraries
I Abstract types Isolation of components
I Hierarchical composition Namespace management
I Extensible structures Ease of use
I Type definitions Concision
Benoît Montagu (X-INRIA) Soutenance de thèse 15 décembre 2010 3 / 41