In recent years, programming language design is more active than ever. Existing languages have seen a dramatic surge of new features that significantly extends the their expressive power, and numerous new languages are being actively developed. Unfortunately, without careful formalization, programming languages can be bogus, which in turn leads to ad-hoc fixes and solutions. My work tackles this challenge by applying theoretical rigor to design reliable and scalable programming languages, such that existing as well as new language features can be reasoned in a precise manner from first principles. As an example, I will describe the design of the kind inference algorithm for the Haskell programming language. This work provides type-theoretic formalization of the algorithm, which establishes desirable language properties and guides the continued evolution of language implementations.
 
In the second part, I will show how to support computational effects through formal type and effect systems in the Koka programming language, such that side-effects of programs can be reasoned and their implementations are guaranteed to be efficient.

Ningning Xie is a PhD candidate at the Programming Languages Group at the University of Hong Kong. Prior to graduate school, she received her B.S. degree in Computer Science from Zhejiang University. Her research interests are in the field of programming languages, focusing on functional programming and type theory. During her Ph.D study, Ningning was an intern at Microsoft Research Redmond. She is a recipient of the ACM SIGPLAN Distinguished Paper Award at the Symposium on Principles of Programming Languages (POPL 2020), and was selected for Rising Stars 2020 organized by UC Berkeley.