WITS 2026
as the organisers put it
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. Sp ...
who it's for
proof assistant developers, dependently typed language implementers, type-checker implementers, compiler engineers, metaprogramming tool authors, runtime systems engineers, programming language researchers
topics
Lean kernel reimplementation; executable Lean typechecker; type-safe program extraction; garbage collection for higher inductive types; e-graph guided GC normalization; meta-programming for proof assistants; implementation of type inference; omnidirectional type inference; homogeneous observational equality; hybrid resolution before inference; verified dependent type-checkers; partial generalization for let-bindings
| title | author | length |
|---|---|---|
| Lean4Lean: Mechanizing the Metatheory of Lean | Mario Carneiro | 01h 04m |
A complete reimplementation of the kernel is written in Lean and produces an executable Lean-written typechecker that is the first alternative to the C++… | ||
| A Dependent Language with Type-Safe Program Extraction | Greg Brown | 22m |
Extractly is a first‑order language inspired by Polarity that removes large elimination and requires all data type definitions to be small, so extraction… | ||
| Garbage Collection for Higher Inductive Types | Islam Talipov, Pavel Sokolov | 21m |
Runtime integrates path-aware replacement into the normalization engine to reduce allocations by redirecting pointers to propositionally equivalent values… | ||
| Code Generation via Meta-programming in Dependently Typed Proof Assistants | Mathis Bouverot-Dupuis, Yannick Forster | 24m |
A survey implements seven implementations of a Functor-deriving meta program that generates the map function for option/list/tree and other boilerplate across… | ||
| Type Inference Techniques: Implementation and Formalization, Better Together | Ningning Xie, Andong Fan | 29m |
Argues that informal compiler hacks need formal proofs and demonstrates this with two concrete cases: scope checks for high‑rank polymorphism implemented via… | ||
| Omnidirectional type inference for ML | Alistair O'Brien, Didier Rémy, Gabriel Scherer | 21m |
Proposes omnidirectional type inference: constraints can suspend on unification variables and resume when shape information arrives via suspended match… | ||
| Observing Definitional Equality | András Kovács | 29m |
Proposes replacing the usual dependent observational equality used in heterogeneous unification (Gundry, McBride, Juan) with homogeneous observational equality… | ||
| Type Narrowing the Hard Way | Ben Greenman, Hanwen Guo | 26m |
A litmus-suite called the if t benchmark runs on eight real typecheckers and shows everyone handles basic narrowing but disagree widely on harder cases… | ||
| Decoupling Resolution from Type Inference | Lionel Parreaux | 24m |
Prototype language wit implements hybrid resolution: a fast, local type-aware static analysis that runs before full type inference to choose overloads and… | ||
| Verifying Dependent Type-checkers | Meven Lennon-Bertrand | 01h 03m |
Formal verification of a dependent type-checker for a Coq-like calculus (Metarok) uses assumed normalization axioms and yields concrete wins: it found a bug in… | ||
| nothing matches | ||