Polymorphic Types with Polynomial Sizes
Jean-Louis Colaço  1, *  , Baptiste Pauget  2  , Marc Pouzet  3@  
1 : ANSYS
Ansys inc.
2 : Inria Paris-Rocquencourt
Institut National de Recherche en Informatique et en Automatique
INRIA Rocquencourt : Domaine de Voluceau, Rocquencourt B.P. 105 78153 le Chesnay Cedex -  France
3 : Ecole normale supérieure – PSL (Paris)
L'Institut National de Recherche en Informatique et e n Automatique (INRIA)
* : Auteur correspondant

We present a compile-time analysis for tracking the size of data-structures in a statically typed and strict functional language. This information is valuable for static checking and code generation. Rather than relying on dependent types, we propose a type-system close to that of ML: polymorphism is used to define functions that are generic in types and sizes; both can be inferred. This approach is convenient, in particular for a language used to program critical embedded systems, where sizes are indeed known at compile-time. By using sizes that are multivariate polynomials, we obtain a good compromise between the expressiveness of the size language and its properties (verification, inference).


Personnes connectées : 4 Vie privée
Chargement...