List of Seminar Talks

Slides to be found at seminar-talks. Other past events include booking reading and paper reading.

2025

• Environment-Based Polymorphism Jinhao 2025/4/23
• Type Inference as Rewriting Chen Cui 2025/4/9
• Normalization by Evaluation for Non-cumulativity Shengyi Jiang 2025/3/26
• Lazier Fixpoints Yicong 2025/3/5
• An Effectful Modal Calculus with Small-Step Environment-Based Semantics Jinhao 2025/2/19
• Contextual Local Function Inference Chen 2025/2/12
• Two Practice Talks for POPL Shengyi & Litao 2025/1/15



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