WITS 2026 is the 5th Workshop on the Implementation of Type Systems. The workshop will be held on January 17, 2026, in Rennes, France, co-located with POPL. 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.
Sponsor
Great thanks to Jane Street for sponsoring WITS!
This program is tentative and subject to change.
Sat 17 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
09:00 - 10:30 | |||
09:00 60mKeynote | Lean4Lean: Mechanizing the Metatheory of Lean WITS Mario Carneiro Chalmers University of Technology | ||
10:00 22mTalk | Observing Definitional Equality WITS András Kovács University of Gothenburg and Chalmers University of Technology | ||
10:30 - 11:00 | |||
10:30 30mCoffee break | Break POPL Catering | ||
11:00 - 12:30 | |||
11:00 22mTalk | Decoupling Resolution from Type Inference WITS Lionel Parreaux Hong Kong University of Science and Technology | ||
11:22 22mTalk | First-Class Refinement Types in Scala WITS Matt Bovel EPFL | ||
11:45 22mTalk | Types as grammars WITS Gil Silva LASIGE, University of Lisbon, Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Diana Costa LASIGE, University of Lisbon, Andreia Mordido University of Lisbon, Diogo Poças Instituto de Telecomunicações, University of Lisbon, Vasco T. Vasconcelos LASIGE, University of Lisbon | ||
12:07 22mTalk | Omnidirectional type inference for ML WITS Alistair O'Brien University of Cambridge, Didier Rémy Inria, Gabriel Scherer Université Paris Cité - Inria - CNRS | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch POPL Catering | ||
14:00 - 15:30 | |||
14:00 22mTalk | A Dependent Language with Type-Safe Program Extraction WITS Greg Brown University of Edinburgh | ||
14:22 22mTalk | Code Generation via Meta-programming in Dependently Typed Proof Assistants WITS | ||
14:45 22mTalk | Garbage Collection for Higher Inductive Types WITS | ||
15:07 22mTalk | Type Inference Techniques: Implementation and Formalization, Better Together WITS | ||
15:30 - 16:00 | |||
15:30 30mCoffee break | Break POPL Catering | ||
16:00 - 18:00 | |||
16:00 40mKeynote | Verifying Dependent Type-checkers WITS Meven Lennon-Bertrand Inria – Université Paris Cité | ||
17:00 22mTalk | Type Narrowing the Hard Way WITS | ||
17:23 2mOther | Closing WITS Niki Vazou IMDEA Software Institute | ||
Accepted Papers
Call for Participation
WITS 2026 is the 5th Workshop on the Implementation of Type Systems. The workshop will be held on January 17, 2026, in Rennes, France, co-located with POPL. The goal of this workshop is to bring together the implementors of a variety of languages with advanced type systems. 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.
Scope
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.
Here are a few examples of topics we are interested to discuss:
- syntax with binders and substitution
- conversion modulo beta and eta
- implicit arguments and metavariables
- unification and constraint solving
- metaprogramming and tactic languages
- editor integration and automation
- discoverability of language features
- pretty printing and error messages
This list is not exhaustive, so please contact the PC chair in case you are unsure if a topic falls within the scope of the workshop.
Submissions
WITS solicits two kinds of submissions:
-
Contributed talks on the basis of an abstract. This can be on recently published or submitted work, work in progress, or a project that is still in the idea phase.
-
Proposals for roundtable discussions. This can be on any topic within the scope of the workshop, but should have a broader scope than a contributed talk. If accepted, you will be in charge of leading a discussion of 45 minutes around the proposed topic together with other interested attendees.
Both kinds of proposals should be accompanied by an abstract of max. 1 page (exclusive of references), formatted according to the guidelines for SIGPLAN conferences: use the sigplan option to the acmart LaTeX document class. WITS will have no published proceedings, so submitting to WITS does not interfere with submission (before, after, or simultaneously) with other venues. Submissions are handled via https://wits26.hotcrp.com/.
Important Dates
- Abstract submission deadline: 6 November, 2025 (AoE)
- Notification: 1 December, 2025
- Workshop in Rennes: 17 January, 2026
Attendance and registration
WITS 2026 is colocated with POPL 2026 in Rennes, France. Information on registration and attendance will be posted on the POPL website at https://popl26.sigplan.org/.
| Sat 17 Jan 2026 Workshop |
| Mon 1 Dec 2025 Notification |
| Thu 6 Nov 2025 Submission Deadline |
