HKU PL Group

List of Seminar Talks

2024

Merges with Semantic Typing Qianyong 2024/11/20
Modular Borrowing Without Ownership or Linear Types Lionel Parreaux 2024/11/5
Contextual Typing for Polymorphic Systems Xu Xue 2024/10/16
Yet another practice talk for OOPSLA Yaozhu 2024/10/2
Two practice talks for OOPSLA Litao, Jinhao 2024/9/11
Higher-rank Polymorphism with Intersection and Union Types Shengyi Jiang 2024/7/2
Testing and debugging your language with PLT Redex Qianyong 2024/6/18
Principles and Experiences of Programming System Design for Low-Code Platform Weixin 2024/5/28
Karp: A Language for Reduction Chenhao Zhang 2024/5/21
Modern Type Theories and Their Applications Zhaohui Luo 2024/5/15
Liberating the Merge Operator with Type Apartness and Guarded Upcasting Snow 2024/5/7
Layered Modal Type Theory Jason Hu 2024/4/30
Merging Gradual Typing Wenjia Ye 2024/4/23
Semantic Approach to Type Soundness Litao 2024/4/10
Decidability of Nondeterministic Worklist Algorithms Chen Cui 2024/3/12
A formal treatment of bidirectional typing Xu Xue 2024/3/5
Updates about Full Iso-recursive Types Qianyong 2024/2/20
Let Next Argument Go First Yaozhu 2024/2/6
Module Types via Intersection Types Jinhao Tan 2024/1/30
Two more talks Marco Servetto 2024/1/18
Why Withers are not enough. Problems attempting to unify FP and OOP Marco Servetto 2024/1/15
An Alternative Constraint-solving Approach for Nominal Subtyping Shengyi Jiang 2024/1/9

2023

Contextual Type Inference (Continued) Xu Xue 2023/12/13
Collecting all possibilities Wenjia Ye 2023/12/6
Dead Code Analysis in the Compiler of MoonBit Yaozhu 2023/11/22
Adding Currying to Subtyping Jinhao Tan 2023/11/15
A Type System for Scope Safety Lionel Parreaux 2023/11/8
Extending Higher-rank Polymorphism to Intersection and Union Type Shengyi 2023/10/18
Two Practice Talks for OOPSLA Chen, Wenjia 2023/10/11
Relating Expressiveness of Recursive Types Litao 2023/9/27
Full Iso-recursive Types Litao 2023/9/13
Backwards Bidirectional Typing for Non-Linear Terms, Leveraging Intersection Types Snow 2023/7/13
Dependent Merges and First-Class Environments (Practice Talk for ECOOP) Jinhao Tan 2023/6/29
No Unification Variable Left Behind - Fully Grounding Type Inference for the HDM System Roger Bosman 2023/6/15
Contextual Type Inference Xu Xue 2023/6/8
Formalisation of Higher-order Pattern Unification Alvin 2023/5/25
Apartness for Intersection and Union types Han Xu 2023/5/18
Call-By-Push-Value Chen 2023/5/11
Separate Compilation of Compositional Programming Yaozhu 2023/5/4
Formalise Your Type System, Intrinsically Xu Xue 2023/4/27
Pragmatic Gradual Polymorphism with References Ye Wenjia 2023/4/20
SuperOOP: Another Solution to the Expression Problem Yaozhu 2023/3/16
Revisiting Disjoint Polymorphism Baber 2023/3/9
Algebraic Effects Shengyi 2023/3/2
How to Worklist for Dependent Type Inference Alvin 2023/2/9
Labelling a type/proposition Jinhao Tan 2023/2/2
Two practice talks for POPL 2023 Yaoda, Han Xu 2023/1/13

2022

Another two practice talks for SPLASH 2022 Yaozhu, Xu Xue 2022/11/25
Taming Intersection Types and the Merge Operator Snow 2022/11/23
Practice talk for SPLASH 2022 Yaoda 2022/11/11
Elaborating Merges to Records: Modeling the Compilation of Fi+ to JavaScript Snow 2022/11/4
Disjoint Switches with Disjoint Functions Baber Rehman 2022/10/28
Type Inference with Bounded Quantification Chen 2022/10/21
Beyond Parametric Polymorphism Shengyi Jiang 2022/9/23
Subtyping, Preservation, and Top-Like Types Snow 2022/9/16
Types as Contexts Jinhao Tan 2022/8/30
Revisiting F-bounded Polymorphism Yaoda 2022/8/23
Applicative Subtyping Xu Xue 2022/7/5
Relational Parametricity and Gradual Guarantee Ye Wenjia 2022/6/21
Direct Foundations for Compositional Programming Andong Fan 2022/6/7
Union Types with Disjoint Switches Baber Rehman 2022/5/31
Mechanisation of Higher-order Terms Alvin 2022/5/24
Compositional Embeddings of DSLs Yaozhu 2022/5/17
Type Inference for Erlang Chen 2022/1/7

2021

On the understanding of subtyping recursive types Yaoda 2021/12/17
Encoding Labeled and Optional Arguments in λ<: and λi+ Yaozhu 2021/12/10
Type Directed Operational Semantics Gradual Typing for Object YE Wenjia 2021/11/19
From Occurrence Typing to Refinement Types Xu Xue 2021/11/12
Generalizing Worklist-based Inference for Dependent Types Alvin 2021/10/29
Revisiting Occurrence Typing: Global Context and Disjointness Baber 2021/10/22
Simplifying Type Inference Chen Cui 2021/9/17
On the Deduction Theorem and Subtyping Relations Jinhao 2021/8/31
Union Types with Disjoint Switches Baber Rehman 2021/8/17
Distributing Intersection and Union Types with Splits and Duality Snow 2021/8/10
Revisiting type disjointness Snow 2021/7/27
Applicative Intersection Types Xu Xue 2021/7/6
Type-Directed Operational Semantics for Gradual Typing Wenjia 2021/6/22
A Dependently Typed Calculus with Polymorphic Subtyping Alvin 2021/6/22
Revisiting Iso-recrusive Subtyping Yaoda 2021/5/25
How to perform fewer dynamic checks in Gradual Typing Wenjia Ye 2021/5/18
Compositional Programming Yaozhu 2021/5/4
Some discussions about type classes Alvin 2021/4/27
Formalized Higher-Ranked Polymorphic Type Inference Algorithms Jimmy 2021/4/20
Type Directed Operational Semantics for Gradual Typing YE Wenjia 2021/3/30
Polymorphic Subtyping and Dependent Types Alvin 2021/1/19

2020

Zord Meets WebAssembly: Compiling a Functional Language Yaozhu 2020/11/10
Type Inference with Rank-1 Restriction Jimmy 2020/11/3
Direct Gradually Typed Lambda Calculus with Merge Operator YE Wenjia 2020/9/22
Type Bounds with DuoTyping Baber 2020/7/7
Higher-rank Polymophism on a Dependent Type System XUE Alvin Mingqi 2020/6/30
Revisiting Merges and Disjointness Snow 2020/6/23
Kind Inference For Datatypes Ningning 2020/1/20

2019

Towards Language Support For Object Algebras Weixin 2019/11/4
Elaboration For The Worklist Algorithm Jimmy 2019/10/28
Type Inference For Object Oriented Programming With Higher Ranked Polymorphism Jimmy 2019/9/16
Performance Comparison Of Different Subtyping Algorithms Hongsen 2019/8/26
Duotyping Baber 2019/7/21
Iso Disjoint Intersection Types Yaoda 2019/6/17
Intersection In Typescript Baber 2019/6/3
Parallel Application Weixin 2019/5/20
Type Inference Via Worklist Context Jimmy 2019/4/29
Duotyping Baber 2019/4/22
Iso Disjoint Intersection Types Yaoda 2019/3/24
Shallow EDSLs and Object-Oriented Programming: Beyond Simple Compositionality Weixin 2019/1/29
On the Expressive Power of Disjoint Polymorphism Ningning 2019/1/22
Probabilistic Programming and its Semantics Carol Mak 2019/1/8

2018

Towards Better Modularity in Multiple Inheritance Grace 2018/12/11
Disjoint intersection types: theory and practice Jeremy 2018/11/20
Worklist Context Jimmy 2018/11/13
Pattern Matching in an Open World Weixin 2018/10/30
From Row Polymorphism to Disjoint Polymorphism Yaoda 2018/10/23
Coercion Quantification Ningning 2018/10/5
Design an Operational Semantics for Disjoint Intersection Types Snow 2018/9/21
Smart combinators for test data generation Haoyuan 2018/8/17
Meta-theory on Cascading Contexts Jimmy 2018/8/10
a practice talk Grace 2018/6/29
a practice talk Jeremy 2018/6/29
a practice talk Jimmy 2018/6/29
Giving Disjoint Polymorphism a Promotion Jeremy 2018/6/15
Modular Monadic Parsing with Unfolds Haoyuan 2018/6/8
a problem session Grace 2018/6/1
a problem session Snow 2018/6/1
Formalizing higher-order type systems without output contexts Jimmy 2018/5/25
Unified Subtyping with Strong Dependent Pairs Linus 2018/5/18
Resolving Unintentional State Conflicts: FHJ+ Grace 2018/5/11
Pattern Matching in an Open World Weixin 2018/5/4

2017

Desugaring First-class Modules Linus 2017/12/8
Composable pattern matching with visitors Weixin 2017/12/8
On intersection types, from theory to practice Jeremy 2017/12/1
Let Arguments Go into Disjoint Intersection Types Snow 2017/11/17
Towards machanized proofs on output contexts Jimmy 2017/11/10
Consistent Subtyping for All Ningning 2017/11/3
Unifying Typing and Subtyping Linus 2017/10/20
Type-Safe Modular Parsing Haoyuan 2017/10/20
Call-by-value Iso-types Linus 2017/9/22
Modular Imperative Visitors Weixin 2017/9/13
Modular Unfolds Haoyuan 2017/9/6
Revisiting Disjointness and Coherence Jeremy 2017/8/30
Higher-Rank Type Checking with Worklist Jimmy 2017/8/16
Modular language components with explicit ASTs Li Huang 2017/8/9
Unifying Subtyping with Typing, Reloaded Linus 2017/8/2
Towards Unification for Dependent Types Ningning 2017/6/14
EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse Weixin 2017/6/14
Resolving Unintended Method Conflicts Yanlin 2017/6/7
When EVF meets Scala Weixin 2017/5/31
SEDEL -- Safe and Expressive Delegation-Based Programming Jeremy 2017/5/17
Persistent Code Identifiers for Dependency Management Tomas 2017/4/26
Disjoint Polymorphism João 2017/4/19
A built-in solution for bindings - An introduction to Abella Jimmy 2017/3/22
let arguments go first, again Ningning 2017/3/8
Type-safe Modular Parsing Li Huang 2017/3/1
Unifying Subtyping with Typing Linus 2017/2/8
Dive into Sized Types & Copatterns Jeremy 2017/1/20
Extensible Domain-Specific Languages in Object-Oriented Programming Weixin 2017/1/6

2016

A more theoretical view of Intersection/Union Types Jimmy 2016/11/18
Embedding a Refinement Calculus in Coq João 2016/11/11
Types in PFPL Ningning 2016/10/28
Extensible Parsers Li Huang 2016/10/14
Search-focused Programming Environments Tomas 2016/9/30
Explore different inheritance models and method conflict resolution Yanlin 2016/9/9
Revisiting Lambda Encodings of Datatypes Linus 2016/9/1
EVF: An Extensible and Expressive Visitor Framework Weixin 2016/8/25
A Dependently Typed Language with Intersection Types Jeremy 2016/8/18
Functional extensible parsers Haoyuan 2016/8/11
Disjoint Intersection Types and Disjoint Quantification João 2016/7/28
Type Inference Again! Xie Ningning 2016/7/21
The use of Modular Reifiable Matching (MRM) Li Huang 2016/7/14
Generalizing Casts with Full Reduction Linus 2016/7/7
Return of Living Datalog Tomas 2016/6/23
RapidPL Yanlin 2016/6/16
Embedding Extensible DSLs in Object-Oriented Languages Weixin 2016/4/22
Subtyping dependent types Jeremy 2016/4/15
Family Polymorphism in Java, continued Haoyuan 2016/4/8
Disjoint Intersection Types João 2016/4/1
Modular Architecture for Code and Metadata Sharing Tomas 2016/3/11
Constructive Logic Ningning 2016/3/4
Introduction to Supercompilation Li Huang 2016/2/26
Encoding GADTs with Type Equality Constraints Linus 2016/1/14
Classless Java, Continued Yanlin 2016/1/14
Object Algebras as Visitors Weixin 2016/1/7

2015

Towards First-class Modules in Dependently Typed Languages Jeremy 2015/12/17
Classless Java Formalization Haoyuan 2015/12/10
Tail Calls in the JVM with Imperative Functional Objects Tomas 2015/11/26
Homotopy Type Theory Primer George 2015/11/19
Encodings of data types Li Huang 2015/11/4
Introduction of Type Inference Ningning 2015/10/29
Encoding GADTs with Casts Linus 2015/10/15
Scrap Your Boilerplate with Object Algebras Haoyuan 2015/10/8
Symbolic Property-based Testing for Functional Languages Weixin 2015/9/24
Fun - fun playing with dependent types Jeremy 2015/9/10
Why code generation matters Haoyuan 2015/8/13
Disjoint Intersection Types and Disjoint Quantification George 2015/8/6
Twitterize You a Haskell for Great Profit Tomas 2015/7/16
Disjoint Intersection Types and Disjoint Quantification George 2015/6/25
Explicit Calculus of Constructions with Recursion Linus 2015/6/11
Building modular high-performance interpreters with Truffle + OA Yanlin 2015/6/4
Symbolic execution for property based testing in practice Weixin 2015/5/28
Giving FCore a Promotion: by adding a dependently typed core Jeremy 2015/5/7
Syntax for Object Algebras Haoyuan 2015/4/30
Improved F& and a source-level syntax support for extensibility George 2015/4/23
From Namespaces to Dependencies and Reproducible Builds Tomas 2015/4/16
Implement a dependently typed core language in Haskell Linus 2015/4/9
An introduction to context-oriented programming and an approach Prof. Aotani Tomoyuki 2015/3/27
Let Object Algebras Fly — Explore pattern matching in OAs Yanlin 2015/3/26
When Functional Languages Meet Symbolic Evaluation Weixin 2015/3/19
How to Make FCore Thread-safe Jeremy 2015/3/5
Object Algebras in Our Language Haoyuan 2015/2/12