Seminar Talks

4 Feb

A typed embedding of Redex DSL in Haskell

Xu Xue CB308

21 Jan

Merges with Semantic Typing (thrice upon a time)

Qianyong CB308

3 Dec

Mechanizing Step-Indexed Logical Relations with Small-Step Environment Semantics

Jinhao CB313

19 Nov

Typing Compositions, Locally

Chen Cui CB308

5 Nov

Parallel substitution and strengthening

Yicong Luo CB308

22 Oct

Casual Gathering with Wenhao

Shengyi Jiang CB308

8 Oct

Local Contextual Type Inference

Xu Xue CB308

19 Sep

MoonBit and the Future of AI-Native Programming Languages

Hongbo Zhang CB328

10 Sep

The Power of Formalization in LLM Reasoning

Jiyao Zhang CB308

3 Sep

Induction-recursion, Impredicativity and a New Way to Formalize MLTT in Rocq

Qianyong CB313

20 Aug

Typing as Reduction: Yet Another Perspective on Type Inference

Chen Zoom

2 Jul

Distributive Recursive Subtyping via Translation

Litao CB313

18 Jun

New Techniques for Coinduction Formalizations

Litao CB308

4 Jun

Merges with Semantic Typing (continued)

Qianyong CB308

14 May

Free Variables as Bitmaps

Xu Xue CB308

30 Apr

Environment-Based Polymorphism

Jinhao CB308

9 Apr

Type Inference as Rewriting

Chen Cui CB308

26 Mar

Normalization by Evaluation for Non-cumulativity

Shengyi Jiang CB313

5 Mar

Lazier Fixpoints

Yicong CB308

19 Feb

An Effectful Modal Calculus with Small-Step Environment-Based Semantics

Jinhao CB308

12 Feb

Contextual Local Function Inference

Chen CB313

15 Jan

Two Practice Talks for POPL

Shengyi & Litao Zoom

4 Dec

Formalized Normalization-by-Evaluation of (Non-cumulative) MLTT

Shengyi Jiang CB313

20 Nov

Merges with Semantic Typing

Qianyong CB308

5 Nov

Modular Borrowing Without Ownership or Linear Types

Lionel Parreaux CB308

16 Oct

Contextual Typing for Polymorphic Systems

Xu Xue CB308

2 Oct

Yet another practice talk for OOPSLA

Yaozhu CB313

11 Sep

Two practice talks for OOPSLA

Litao, Jinhao CB308

2 Jul

Higher-rank Polymorphism with Intersection and Union Types

Shengyi Jiang CB308

18 Jun

Testing and debugging your language with PLT Redex

Qianyong CB308

28 May

Principles and Experiences of Programming System Design for Low-Code Platform

Weixin CB308

21 May

Karp: A Language for Reduction

Chenhao Zhang CB308

15 May

Modern Type Theories and Their Applications

Zhaohui Luo zoom

7 May

Liberating the Merge Operator with Type Apartness and Guarded Upcasting

Snow CB308

30 Apr

Layered Modal Type Theory

Jason Hu CB308

23 Apr

Merging Gradual Typing

Wenjia Ye CB313

10 Apr

Semantic Approach to Type Soundness

Litao CB308

12 Mar

Decidability of Nondeterministic Worklist Algorithms

Chen Cui CB308

5 Mar

A formal treatment of bidirectional typing

Xu Xue CB308

20 Feb

Updates about Full Iso-recursive Types

Qianyong CB308

6 Feb

Let Next Argument Go First

Yaozhu CB328

30 Jan

Module Types via Intersection Types

Jinhao Tan CB328

18 Jan

Two more talks

Marco Servetto CB328

15 Jan

Why Withers are not enough. Problems attempting to unify FP and OOP

Marco Servetto CB308

9 Jan

An Alternative Constraint-solving Approach for Nominal Subtyping

Shengyi Jiang CB328

13 Dec

Contextual Type Inference (Continued)

Xu Xue CB308

6 Dec

Collecting all possibilities

Wenjia Ye CB308

22 Nov

Dead Code Analysis in the Compiler of MoonBit

Yaozhu CB308

15 Nov

Adding Currying to Subtyping

Jinhao Tan CB308

8 Nov

A Type System for Scope Safety

Lionel Parreaux CB308

18 Oct

Extending Higher-rank Polymorphism to Intersection and Union Type

Shengyi CB308

11 Oct

Two Practice Talks for OOPSLA

Chen, Wenjia CB308

27 Sep

Relating Expressiveness of Recursive Types

Litao CB308

13 Sep

Full Iso-recursive Types

Litao CB308

13 Jul

Backwards Bidirectional Typing for Non-Linear Terms, Leveraging Intersection Types

Snow CB308

29 Jun

Dependent Merges and First-Class Environments (Practice Talk for ECOOP)

Jinhao Tan CB308

15 Jun

No Unification Variable Left Behind - Fully Grounding Type Inference for the HDM System

Roger Bosman CB328

8 Jun

Contextual Type Inference

Xu Xue CB308

25 May

Formalisation of Higher-order Pattern Unification

Alvin CB308

18 May

Apartness for Intersection and Union types

Han Xu CB308

11 May

Call-By-Push-Value

Chen CB308

4 May

Separate Compilation of Compositional Programming

Yaozhu CB308

27 Apr

Formalise Your Type System, Intrinsically

Xu Xue CB308

20 Apr

Pragmatic Gradual Polymorphism with References

Ye Wenjia CB308

16 Mar

SuperOOP: Another Solution to the Expression Problem

Yaozhu CB308

9 Mar

Revisiting Disjoint Polymorphism

Baber CB308

2 Mar

Algebraic Effects

Shengyi CB308

9 Feb

How to Worklist for Dependent Type Inference

Alvin CB308

2 Feb

Labelling a type/proposition

Jinhao Tan CB308

13 Jan

Two practice talks for POPL 2023

Yaoda, Han Xu CB308

25 Nov

Another two practice talks for SPLASH 2022

Yaozhu, Xu Xue CB308

23 Nov

Taming Intersection Types and the Merge Operator

Snow CB308

11 Nov

Practice talk for SPLASH 2022

Yaoda CB308

4 Nov

Elaborating Merges to Records: Modeling the Compilation of Fi+ to JavaScript

Snow CB308

28 Oct

Disjoint Switches with Disjoint Functions

Baber Rehman CB328

21 Oct

Type Inference with Bounded Quantification

Chen CB328

23 Sep

Beyond Parametric Polymorphism

Shengyi Jiang CB313

16 Sep

Subtyping, Preservation, and Top-Like Types

Snow CB328

30 Aug

Types as Contexts

Jinhao Tan CB308

23 Aug

Revisiting F-bounded Polymorphism

Yaoda CB313

5 Jul

Applicative Subtyping

Xu Xue CB 308

21 Jun

Relational Parametricity and Gradual Guarantee

Ye Wenjia CB308 + Zoom

7 Jun

Direct Foundations for Compositional Programming

Andong Fan Zoom

31 May

Union Types with Disjoint Switches

Baber Rehman CB 313

24 May

Mechanisation of Higher-order Terms

Alvin CB313

17 May

Compositional Embeddings of DSLs

Yaozhu CB313

7 Jan

Type Inference for Erlang

Chen CB308

17 Dec

On the understanding of subtyping recursive types

Yaoda Mixed mode (CB 308 + zoom)

10 Dec

Encoding Labeled and Optional Arguments in λ<: and λi+

Yaozhu CB308

19 Nov

Type Directed Operational Semantics Gradual Typing for Object

YE Wenjia CB308

12 Nov

From Occurrence Typing to Refinement Types

Xu Xue CB308

29 Oct

Generalizing Worklist-based Inference for Dependent Types

Alvin CB308

22 Oct

Revisiting Occurrence Typing: Global Context and Disjointness

Baber CB 313

17 Sep

Simplifying Type Inference

Chen Cui CB308

31 Aug

On the Deduction Theorem and Subtyping Relations

Jinhao CB313

17 Aug

Union Types with Disjoint Switches

Baber Rehman CB 313

10 Aug

Distributing Intersection and Union Types with Splits and Duality

Snow CB 313

27 Jul

Revisiting type disjointness

Snow CB 313

6 Jul

Applicative Intersection Types

Xu Xue CB 313

22 Jun

Type-Directed Operational Semantics for Gradual Typing

Wenjia CB 313

22 Jun

A Dependently Typed Calculus with Polymorphic Subtyping

Alvin CB 313

8 Jun

A conjecture on the expressiveness of subtyping recursive types

Yaoda CB313

25 May

Revisiting Iso-recrusive Subtyping

Yaoda CB313

18 May

How to perform fewer dynamic checks in Gradual Typing

Wenjia Ye CB 313

4 May

Compositional Programming

Yaozhu CB313

27 Apr

Some discussions about type classes

Alvin CB313

20 Apr

Formalized Higher-Ranked Polymorphic Type Inference Algorithms

Jimmy CB313

30 Mar

Type Directed Operational Semantics for Gradual Typing

YE Wenjia CB313

19 Jan

Polymorphic Subtyping and Dependent Types

Alvin Zoom 5206196412

10 Nov

Zord Meets WebAssembly: Compiling a Functional Language

Yaozhu CB308

3 Nov

Type Inference with Rank-1 Restriction

Jimmy CB308

22 Sep

Direct Gradually Typed Lambda Calculus with Merge Operator

YE Wenjia CB308

7 Jul

Type Bounds with DuoTyping

Baber CB 308

30 Jun

Higher-rank Polymophism on a Dependent Type System

XUE Alvin Mingqi CB308

23 Jun

Revisiting Merges and Disjointness

Snow CB 308

20 Jan

Kind Inference For Datatypes

Ningning

4 Nov

Towards Language Support For Object Algebras

Weixin

28 Oct

Elaboration For The Worklist Algorithm

Jimmy

16 Sep

Type Inference For Object Oriented Programming With Higher Ranked Polymorphism

Jimmy

26 Aug

Performance Comparison Of Different Subtyping Algorithms

Hongsen

21 Jul

Duotyping

Baber

17 Jun

Iso Disjoint Intersection Types

Yaoda

3 Jun

Intersection In Typescript

Baber

20 May

Parallel Application

Weixin

29 Apr

Type Inference Via Worklist Context

Jimmy

22 Apr

Duotyping

Baber

24 Mar

Iso Disjoint Intersection Types

Yaoda

29 Jan

Shallow EDSLs and Object-Oriented Programming: Beyond Simple Compositionality

Weixin CB 313

22 Jan

On the Expressive Power of Disjoint Polymorphism

Ningning CB 313

8 Jan

Probabilistic Programming and its Semantics

Carol Mak CB 328

11 Dec

Towards Better Modularity in Multiple Inheritance

Grace CB 313

20 Nov

Disjoint intersection types: theory and practice

Jeremy CB 313

13 Nov

Worklist Context

Jimmy CB 313

30 Oct

Pattern Matching in an Open World

Weixin CB 313

23 Oct

From Row Polymorphism to Disjoint Polymorphism

Yaoda CB 313

5 Oct

Coercion Quantification

Ningning CB 313

21 Sep

Design an Operational Semantics for Disjoint Intersection Types

Snow CB 313

17 Aug

Smart combinators for test data generation

Haoyuan CB 313

10 Aug

Meta-theory on Cascading Contexts

Jimmy CB 313

29 Jun

a practice talk

Grace unknown

29 Jun

a practice talk

Jeremy unknown

29 Jun

a practice talk

Jimmy unknown

15 Jun

Giving Disjoint Polymorphism a Promotion

Jeremy CB 313

8 Jun

Modular Monadic Parsing with Unfolds

Haoyuan CB 313

1 Jun

a problem session

Grace CB 313

1 Jun

a problem session

Snow CB 313

25 May

Formalizing higher-order type systems without output contexts

Jimmy CB 313

18 May

Unified Subtyping with Strong Dependent Pairs

Linus CB 313

11 May

Resolving Unintentional State Conflicts: FHJ+

Grace CB 313

4 May

Pattern Matching in an Open World

Weixin CB 328

8 Dec

Desugaring First-class Modules

Linus CB 313

8 Dec

Composable pattern matching with visitors

Weixin CB 313

1 Dec

On intersection types, from theory to practice

Jeremy CB 313

17 Nov

Let Arguments Go into Disjoint Intersection Types

Snow CB 313

10 Nov

Towards machanized proofs on output contexts

Jimmy CB 313

3 Nov

Consistent Subtyping for All

Ningning CB 313

20 Oct

Unifying Typing and Subtyping

Linus CB 313

20 Oct

Type-Safe Modular Parsing

Haoyuan CB 313

22 Sep

Call-by-value Iso-types

Linus CB 313

13 Sep

Modular Imperative Visitors

Weixin CB 313

6 Sep

Modular Unfolds

Haoyuan CB 313

30 Aug

Revisiting Disjointness and Coherence

Jeremy CB 313

16 Aug

Higher-Rank Type Checking with Worklist

Jimmy CB 313

9 Aug

Modular language components with explicit ASTs

Li Huang CB 313

2 Aug

Unifying Subtyping with Typing, Reloaded

Linus CB 313

14 Jun

Towards Unification for Dependent Types

Ningning CB 313

14 Jun

EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse

Weixin CB 313

7 Jun

Resolving Unintended Method Conflicts

Yanlin CB 313

31 May

When EVF meets Scala

Weixin CB 313

17 May

SEDEL -- Safe and Expressive Delegation-Based Programming

Jeremy CB 313

26 Apr

Persistent Code Identifiers for Dependency Management

Tomas CB 313

19 Apr

Disjoint Polymorphism

João CB 328

22 Mar

A built-in solution for bindings - An introduction to Abella

Jimmy CB 313

8 Mar

let arguments go first, again

Ningning CB 313

1 Mar

Type-safe Modular Parsing

Li Huang CB 313

8 Feb

Unifying Subtyping with Typing

Linus CB 328

20 Jan

Dive into Sized Types & Copatterns

Jeremy CB 313

6 Jan

Extensible Domain-Specific Languages in Object-Oriented Programming

Weixin CB 313

18 Nov

A more theoretical view of Intersection/Union Types

Jimmy CB 313

11 Nov

Embedding a Refinement Calculus in Coq

João CB 313

28 Oct

Types in PFPL

Ningning CB 313

14 Oct

Extensible Parsers

Li Huang CB 313

30 Sep

Search-focused Programming Environments

Tomas CB 313

9 Sep

Explore different inheritance models and method conflict resolution

Yanlin CB 313

1 Sep

Revisiting Lambda Encodings of Datatypes

Linus CB 313

25 Aug

EVF: An Extensible and Expressive Visitor Framework

Weixin CB 313

18 Aug

A Dependently Typed Language with Intersection Types

Jeremy CB 313

11 Aug

Functional extensible parsers

Haoyuan CB 313

28 Jul

Disjoint Intersection Types and Disjoint Quantification

João CB 313

21 Jul

Type Inference Again!

Xie Ningning CB 313

14 Jul

The use of Modular Reifiable Matching (MRM)

Li Huang CB 313

7 Jul

Generalizing Casts with Full Reduction

Linus CB 313

23 Jun

Return of Living Datalog

Tomas CB 313

16 Jun

RapidPL

Yanlin CB 328

22 Apr

Embedding Extensible DSLs in Object-Oriented Languages

Weixin CB 328

15 Apr

Subtyping dependent types

Jeremy CB 328

8 Apr

Family Polymorphism in Java, continued

Haoyuan CB 328

1 Apr

Disjoint Intersection Types

João CB 328

11 Mar

Modular Architecture for Code and Metadata Sharing

Tomas CB 313

4 Mar

Constructive Logic

Ningning CB 328

26 Feb

Introduction to Supercompilation

Li Huang CB 328

14 Jan

Encoding GADTs with Type Equality Constraints

Linus CB 328

14 Jan

Classless Java, Continued

Yanlin CB 328

7 Jan

Object Algebras as Visitors

Weixin CB 308

17 Dec

Towards First-class Modules in Dependently Typed Languages

Jeremy CB 313

10 Dec

Classless Java Formalization

Haoyuan CB 313

26 Nov

Tail Calls in the JVM with Imperative Functional Objects

Tomas CB 313

19 Nov

Homotopy Type Theory Primer

George CB 313

4 Nov

Encodings of data types

Li Huang CB 313

29 Oct

Introduction of Type Inference

Ningning CB 313

15 Oct

Encoding GADTs with Casts

Linus CB 313

8 Oct

Scrap Your Boilerplate with Object Algebras

Haoyuan CB 328

24 Sep

Symbolic Property-based Testing for Functional Languages

Weixin CB 313

10 Sep

Fun - fun playing with dependent types

Jeremy CB 313

13 Aug

Why code generation matters

Haoyuan CB 313

6 Aug

Disjoint Intersection Types and Disjoint Quantification

George CB 313

16 Jul

Twitterize You a Haskell for Great Profit

Tomas CB 313

25 Jun

Disjoint Intersection Types and Disjoint Quantification

George CB 313

11 Jun

Explicit Calculus of Constructions with Recursion

Linus CB 313

4 Jun

Building modular high-performance interpreters with Truffle + OA

Yanlin CB 313

28 May

Symbolic execution for property based testing in practice

Weixin CB 313

7 May

Giving FCore a Promotion: by adding a dependently typed core

Jeremy CB 313

30 Apr

Syntax for Object Algebras

Haoyuan CB 313

23 Apr

Improved F& and a source-level syntax support for extensibility

George CB 313

16 Apr

From Namespaces to Dependencies and Reproducible Builds

Tomas CB 313

9 Apr

Implement a dependently typed core language in Haskell

Linus CB 313

27 Mar

An introduction to context-oriented programming and an approach

Prof. Aotani Tomoyuki CB 328

26 Mar

Let Object Algebras Fly — Explore pattern matching in OAs

Yanlin CB 313

19 Mar

When Functional Languages Meet Symbolic Evaluation

Weixin CB 313

5 Mar

How to Make FCore Thread-safe

Jeremy CB 313

12 Feb

Object Algebras in Our Language

Haoyuan CB 313