Expansion for Universal Quantifiers

Abstract : Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the λ-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g.intersection introduction) until enough information has been gathered to make the right decision. Furthermore, these choices can be equivalent to inserting uses of such typing rules at deeply nested positions in a typing derivation, without needing to actually inspect or modify (or even have) the typing derivation. Expansion has in recent years become simpler due to the use of expansion variables (e.g., in System E). This paper extends expansion and expansion variables to systems with ∀-quantifiers. We present System F s , an extension of System F with expansion, and prove its main properties. This system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future.
Type de document :
Communication dans un congrès
European Symposium On Programming (ESOP 2012), Mar 2012, Tallinn, Estonia. pp.456 - 475, 2012, 〈10.1007/978-3-642-28869-2_23〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

Contributeur : Sergueï Lenglet <>
Soumis le : mercredi 30 novembre 2016 - 14:37:44
Dernière modification le : mercredi 4 octobre 2017 - 14:56:17
Document(s) archivé(s) le : lundi 27 mars 2017 - 09:07:13


Fichiers produits par l'(les) auteur(s)



Sergueï Lenglet, J Wells. Expansion for Universal Quantifiers. European Symposium On Programming (ESOP 2012), Mar 2012, Tallinn, Estonia. pp.456 - 475, 2012, 〈10.1007/978-3-642-28869-2_23〉. 〈hal-01405792〉



Consultations de la notice


Téléchargements de fichiers