The Second Workshop on the Implementation of Type Systems (WITS 2023) will be held on August 28, 2023, in Braga, Portugal, co-located with IFL 2023. The goal of this workshop is to bring together the implementors of a variety of languages with advanced type systems. The main focus is on the practical issues that come up in the implementation of these systems, rather than the theoretical frameworks that underlie them. In particular, we want to encourage exchanging ideas between the communities around specific systems that would otherwise be accessible to only a very select group. The workshop will have a mix of invited and contributed talks, organized discussion times, and informal collaboration time. We invite participants to share their experiences, study differences among the implementations, and generalize lessons from those. We also want to promote the creation of a shared vocabulary and set of best practices for implementing type systems.

You can find all the papers here.

Important Dates

Event Day 28th August, 2023


Time Event
9:00 - 9:05 Workshop Opening
9:05 - 10:05 Keynote: Scaling Lean to the next millions of lines of proofs by Sebastian Ullrich
10:05 - 10:30 Nested Pattern Unification by András Kovács / Rafaël Bocquet
10:30 - 11:00 Coffee Break
11:00 - 11:25 Rank-2 Intersection Type Inference Revisited by Pedro Ângelo / Mário Florido
11:25 - 12:20 Discussion: Mixed inductive, coinductive, and quotient data types lead by Alex Keizer
12:30 - 14:00 Lunch Break
14:00 - 14:25 An Implementation Strategy for Gradual Dependent Types by Joseph Eremondi
14:25 - 14:50 Deriving Higher-Order Unification in Haskell by Nikolai Kudasov
14:50 - 15:45 Discussion: Constraint solving with higher-order constructs lead by Jesper Cockx
15:45 - 16:00 Coffee Break
16:00 - 16:25 Extracting and Evolving the Idris core type theory by Justus Matthiesen
16:25 - 17:20 Discussion: Language Servers and Proof Assistants lead by Sebastian Ullrich
17:20 - 17:30 Closing Discussion The Future of WITS
18:30 - 20:00 End-of-day Social Event at Braga City Center