# Archives by Category

### 2015

- Towards First-class Modules in Dependently Typed Languages
- Classless Java Formalization
- Tail Calls in the JVM with Imperative Functional Objects
- Homotopy Type Theory Primer
- Encodings of data types
- Introduction of Type Inference
- Encoding GADTs with Casts
- Scrap Your Boilerplate with Object Algebras
- Symbolic Property-based Testing for Functional Languages
- Fun - fun playing with dependent types
- Why code generation matters
- Disjoint Intersection Types and Disjoint Quantification
- Twitterize You a Haskell for Great Profit
- Disjoint Intersection Types and Disjoint Quantification
- Explicit Calculus of Constructions with Recursion
- Building modular high-performance interpreters with Truffle + OA
- Symbolic execution for property based testing in practice
- Giving FCore a Promotion: by adding a dependently typed core
- Syntax for Object Algebras
- Improved F& and a source-level syntax support for extensibility
- From Namespaces to Dependencies and Reproducible Builds
- Implement a dependently typed core language in Haskell
- An introduction to context-oriented programming and an approach
- Let Object Algebras Fly — Explore pattern matching in OAs
- When Functional Languages Meet Symbolic Evaluation
- How to Make FCore Thread-safe
- Object Algebras in Our Language

### 2016

- A more theoretical view of Intersection/Union Types
- Embedding a Refinement Calculus in Coq
- Types in PFPL
- Extensible Parsers
- Search-focused Programming Environments
- Explore different inheritance models and method conflict resolution
- Revisiting Lambda Encodings of Datatypes
- EVF: An Extensible and Expressive Visitor Framework
- A Dependently Typed Language with Intersection Types
- Functional extensible parsers
- Disjoint Intersection Types and Disjoint Quantification
- Type Inference Again!
- The use of Modular Reifiable Matching (MRM)
- Generalizing Casts with Full Reduction
- Return of Living Datalog
- RapidPL
- Embedding Extensible DSLs in Object-Oriented Languages
- Subtyping dependent types
- Family Polymorphism in Java, continued
- Disjoint Intersection Types
- Modular Architecture for Code and Metadata Sharing
- Constructive Logic
- Introduction to Supercompilation
- Encoding GADTs with Type Equality Constraints
- Classless Java, Continued
- Object Algebras as Visitors

### 2017

- Composable pattern matching with visitors
- On intersection types, from theory to practice
- Let Arguments Go into Disjoint Intersection Types
- Towards machanized proofs on output contexts
- Consistent Subtyping for All
- Unifying Typing and Subtyping
- Type-Safe Modular Parsing
- Call-by-value Iso-types
- Modular Imperative Visitors
- Modular Unfolds
- Revisiting Disjointness and Coherence
- Higher-Rank Type Checking with Worklist
- Modular language components with explicit ASTs
- Unifying Subtyping with Typing, Reloaded
- Towards Unification for Dependent Types
- EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse
- Resolving Unintended Method Conflicts
- When EVF meets Scala
- SEDEL -- Safe and Expressive Delegation-Based Programming
- Persistent Code Identifiers for Dependency Management
- Disjoint Polymorphism
- A built-in solution for bindings - An introduction to Abella
- let arguments go first, again
- Type-safe Modular Parsing
- Unifying Subtyping with Typing
- Dive into Sized Types & Copatterns
- Extensible Domain-Specific Languages in Object-Oriented Programming

### 2018

- Towards Better Modularity in Multiple Inheritance
- Disjoint intersection types: theory and practice
- Worklist Context
- Pattern Matching in an Open World
- From Row Polymorphism to Disjoint Polymorphism
- Coercion Quantification
- Design an Operational Semantics for Disjoint Intersection Types
- Smart combinators for test data generation
- Meta-theory on Cascading Contexts
- a practice talk
- a practice talk
- a practice talk
- Giving Disjoint Polymorphism a Promotion
- Modular Monadic Parsing with Unfolds
- a problem session
- a problem session
- Formalizing higher-order type systems without output contexts
- Unified Subtyping with Strong Dependent Pairs
- Resolving Unintentional State Conflicts: FHJ+
- Pattern Matching in an Open World
- Desugaring First-class Modules

### 2019

- Shallow EDSLs and Object-Oriented Programming: Beyond Simple Compositionality
- On the Expressive Power of Disjoint Polymorphism
- Probabilistic Programming and its Semantics

### AotaniTomoyuki

### George

- Homotopy Type Theory Primer
- Disjoint Intersection Types and Disjoint Quantification
- Disjoint Intersection Types and Disjoint Quantification
- Improved F& and a source-level syntax support for extensibility

### Grace

- Towards Better Modularity in Multiple Inheritance
- a practice talk
- a problem session
- Resolving Unintentional State Conflicts: FHJ+

### Haoyuan

- Smart combinators for test data generation
- Modular Monadic Parsing with Unfolds
- Type-Safe Modular Parsing
- Modular Unfolds
- Functional extensible parsers
- Family Polymorphism in Java, continued
- Classless Java Formalization
- Scrap Your Boilerplate with Object Algebras
- Why code generation matters
- Syntax for Object Algebras
- Object Algebras in Our Language

### Jeremy

- Disjoint intersection types: theory and practice
- a practice talk
- Giving Disjoint Polymorphism a Promotion
- On intersection types, from theory to practice
- Revisiting Disjointness and Coherence
- SEDEL -- Safe and Expressive Delegation-Based Programming
- Dive into Sized Types & Copatterns
- A Dependently Typed Language with Intersection Types
- Subtyping dependent types
- Towards First-class Modules in Dependently Typed Languages
- Fun - fun playing with dependent types
- Giving FCore a Promotion: by adding a dependently typed core
- How to Make FCore Thread-safe

### Jimmy

- Worklist Context
- Meta-theory on Cascading Contexts
- a practice talk
- Formalizing higher-order type systems without output contexts
- Towards machanized proofs on output contexts
- Higher-Rank Type Checking with Worklist
- A built-in solution for bindings - An introduction to Abella
- A more theoretical view of Intersection/Union Types

### João

- Disjoint Polymorphism
- Embedding a Refinement Calculus in Coq
- Disjoint Intersection Types and Disjoint Quantification
- Disjoint Intersection Types

### LiHuang

- Modular language components with explicit ASTs
- Type-safe Modular Parsing
- Extensible Parsers
- The use of Modular Reifiable Matching (MRM)
- Introduction to Supercompilation
- Encodings of data types

### Linus

- Unified Subtyping with Strong Dependent Pairs
- Desugaring First-class Modules
- Unifying Typing and Subtyping
- Call-by-value Iso-types
- Unifying Subtyping with Typing, Reloaded
- Unifying Subtyping with Typing
- Revisiting Lambda Encodings of Datatypes
- Generalizing Casts with Full Reduction
- Encoding GADTs with Type Equality Constraints
- Encoding GADTs with Casts
- Explicit Calculus of Constructions with Recursion
- Implement a dependently typed core language in Haskell

### Ningning

- On the Expressive Power of Disjoint Polymorphism
- Coercion Quantification
- Consistent Subtyping for All
- Towards Unification for Dependent Types
- let arguments go first, again
- Types in PFPL
- Type Inference Again!
- Constructive Logic
- Introduction of Type Inference

### Snow

- Design an Operational Semantics for Disjoint Intersection Types
- a problem session
- Let Arguments Go into Disjoint Intersection Types

### Tomas

- Persistent Code Identifiers for Dependency Management
- Search-focused Programming Environments
- Return of Living Datalog
- Modular Architecture for Code and Metadata Sharing
- Tail Calls in the JVM with Imperative Functional Objects
- Twitterize You a Haskell for Great Profit
- From Namespaces to Dependencies and Reproducible Builds

### Visitors

### Weixin

- Shallow EDSLs and Object-Oriented Programming: Beyond Simple Compositionality
- Pattern Matching in an Open World
- Pattern Matching in an Open World
- Composable pattern matching with visitors
- Modular Imperative Visitors
- EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse
- When EVF meets Scala
- Extensible Domain-Specific Languages in Object-Oriented Programming
- EVF: An Extensible and Expressive Visitor Framework
- Embedding Extensible DSLs in Object-Oriented Languages
- Object Algebras as Visitors
- Symbolic Property-based Testing for Functional Languages
- Symbolic execution for property based testing in practice
- When Functional Languages Meet Symbolic Evaluation

### Yanlin

- Resolving Unintended Method Conflicts
- Explore different inheritance models and method conflict resolution
- RapidPL
- Classless Java, Continued
- Building modular high-performance interpreters with Truffle + OA
- Let Object Algebras Fly — Explore pattern matching in OAs