Sous-Typage par Saturation de Contraintes, Théorie et Implémentation

Abstract : This PHD thesis focuses on static analysis of programs by type inference in order to detect program errors before their execution. More precisely, we focus hear in the field of sub-typing, where program properties are described by sets of constraints of the form (t1 <= t2). Our verification mechanisms are based on the aggregation of sub-typing constraints and checking of their compatibility by saturation. The base language on which we define our type systems is an ML-like language provided with variants and pattern matching. We starts by defining a formalism to express our type systems thanks to inference rules. This formalism has the advantage to be sufficiently flexible to allow proving validity and termination properties of our systems, and sufficiently precise to allow a systematic derivation of our inference rules into a runnable typer. After the definition of a base type system for our language, we present three novel extensions: * An improvement of type inference for the pattern matching based on the addition of the "or" operator between sub-typing constraints. This operator allow to express a link, in each cases of a match, between the pattern and the constraints generated at typing time of the case expression. This allows us to refine the type of some functions, and then to accept more valid programs. * A new implementation of the generalization mechanism. This allows to distinguish constraints associated to the different occurrences of a function parameter in its body. Thanks to this mechanism, the "let" construction from ML is in particular obsolete. By mixing this extension with the first one, we obtain a type system able to encode "objects" without any additional language construction. * A formalization of GADT based on an novel implementation of existential type variables. In addition to be compatible with the sub-typing context of this thesis, this alternative to GADT has the advantage to improve type inference. As a consequence, most of type annotations, usually required in the presence of GADT, are now optional. Despite the fact that it is possible to directly derive an implementation of our type systems from their rules, that is principally interesting for their comprehension and prototyping, the effectiveness of such typer is insufficient to analyze real world programs. This is principally due to the extensions we provide to the language of constraints, and in particular to the "or" and "not" operators. At then end, we present multiple techniques we used in our implementation to extend the scalability of our analysis.
Document type :
Theses
Complete list of metadatas

https://pastel.archives-ouvertes.fr/tel-01356695
Contributor : Abes Star <>
Submitted on : Friday, August 26, 2016 - 11:10:52 AM
Last modification on : Wednesday, July 3, 2019 - 10:48:05 AM

File

41258_VAUGON_2016_archivage.pd...
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01356695, version 1

Citation

Benoit Vaugon. Sous-Typage par Saturation de Contraintes, Théorie et Implémentation. Langage de programmation [cs.PL]. Université Paris-Saclay, 2016. Français. ⟨NNT : 2016SACLY004⟩. ⟨tel-01356695⟩

Share

Metrics

Record views

404

Files downloads

247