Principal Type Inference for Object-Oriented Programming in a Boolean Algebra of Types

Speaker: Dr. Lionel Parreaux
         Assistant Professor
         Department of Computer Science and Engineering

Title:  "Principal Type Inference for Object-Oriented Programming in a
         Boolean Algebra of Types"

Date:   Monday, 22 November 2021

Time:   4:00pm - 5:00pm

Venue:  Lecture Theater F (Leung Yat Sing Lecture Theater)
        (near lift 25/26, HKUST)

Zoom link:

Meeting ID:     955 3204 9042
Passcode:       CSE

**Note to CSE PGs with NIHK status, please attend the seminar via zoom**


What would TypeScript look like if it had been designed with type
inference and soundness in mind? We provide one possible answer in
MLscript, an object-oriented and functional programming language with
records, generic classes, first-class unions and intersections, instance
matching, and ML-style principal type inference. We define the constructs
of our language using union, intersection, and complement (or negation)
connectives, making sure they form a Boolean algebra, and add enough
structure to derive a sound and complete type inference algorithm. With
this work, we aim to disprove a long-held belief that principal type
inference is not feasible for object- oriented programming languages with
expressive subtyping systems. Thereby, we hope to encourage and help the
implementation of better type inference for functional and object-oriented


Lionel Parreaux is an Assistant Professor at the Department of Computer
Science and Engineering (CSE), Hong Kong University of Science and
Technology (HKUST). His main research interests include programming
language theory and implementation, compiler optimization, and functional
programming. He is interested in making high-level programming languages
both safer and more efficient, mainly through innovations in type systems,
compiler optimization, and metaprogramming, thereby achieving the goal of
"Abstraction Without Regret". His research on metaprogramming received
Best Paper award at GPCE 2017. Lionel obtained his PhD at EPFL in
Lausanne, Switzerland.