Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems
This program is tentative and subject to change.
Recent research has demonstrated the effectiveness of extending the Hindley-Milner (HM) type system with Boolean kinds to support type inference for a wide variety of features. However, the means to support classic type system provisions such as local let generalization and polymorphic recursion is either limited or unknown for such extensions. This paper contributes procedures for equational generalization and semiunification in arbitrary Boolean rings, enabling let generalization and polymorphic recursion in Boolean-kinded type inference. Additionally, methods to minimize the number of bound Boolean type variables are developed to keep types small in these systems. Boolean-kinded HM extensions are exemplified with \textit{nullable reference types}, and how to use the developed procedures to support let generalization and polymorphic recursion is outlined.
This program is tentative and subject to change.
Wed 14 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:40 | |||
14:00 25mTalk | Extensible Data Types with Ad-Hoc Polymorphism POPL Matthew Toohey University of Toronto, Yanning Chen University of Toronto, Ara Jamalzadeh University of Toronto, Ningning Xie University of Toronto DOI Pre-print | ||
14:25 25mTalk | Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems POPL Joseph Zullo Purdue University DOI | ||
14:50 25mTalk | Local Contextual Type Inference POPL Xu Xue University of Hong Kong, Chen Cui University of Hong Kong, Shengyi Jiang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
15:15 25mTalk | Typing Strictness POPL Daniel Sainati University of Pennsylvania, Joseph W. Cutler University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI | ||