WITS 2025
as the organisers put it
WITS 2025 is the fourth Workshop on the Implementation of Type Systems. The workshop will be held on January 25, 2025, in Denver, USA, 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.
who it's for
language implementors, compiler engineers, programming language researchers, proof assistant developers, functional language engineers, tooling and library authors
topics
bidirectional typing implementations; Hindley-Milner type inference; Free Foil scope-safe representation; second-order abstract syntax; higher-order unification algorithms; eta conversion for unit type; normalization-by-evaluation (NbE); level-based generalization / lexical levels; incremental typing with order maintenance; cumulative universe hierarchy and verified proof checker
| title | author | length |
|---|---|---|
| Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax | Nikolai Kudasov, Anastasia Smirnova, Vladislav Deryabkin, Diana Tomilovskaia, Ekaterina Maksimova | 20m |
Claims a reusable Haskell implementation strategy for bidirectional typing and Hindley-Milner inference built on the scope-safe Free Foil representation… | ||
| Eta conversion for the unit type (is still not that simple) | András Kovács | 28m |
Argues that eta for unit needs type-directed conversion and proposes a bidirectional elaboration core interleaved with normalization-by-evaluation that… | ||
| Semantic Analysis of Normalisation for Directional Logic Programming | Vikraman Choudhury, Neel Krishnaswami, Ariadne Si Suo | 25m |
Claims a formal bridge: bidirectional type checking becomes directional logic programs whose evaluation is normalisation as cut reductions in classical linear… | ||
| Towards Generic Higher-Order Unification Implementations in Haskell | Nikolai Kudasov, Artem Starikov, Fedor Ivanov, Damir Alfiatonov | 17m |
Claims a reusable Haskell library approach that uses Free Foil and a separate signature for parameterised metavariables to produce a limited Second‑Order… | ||
| Invited Talk: Type inference in OCaml and GHC using Levels | Richard A. Eisenberg | 01h 00m |
Claim: both OCaml and GHC implement let-generalization using lexical levels on types or levels on variables, and those levels also power other checks (escape… | ||
| Incremental Bidirectional Typing via Order Maintenance | Thomas J. Porter, Marisa Kirisame, Liam Mulcahy, Pavel Panchekha, Cyrus Omar | 34m |
Presents an incremental algorithm that maintains total bidirectional typing for a gradually typed language via small-step update propagation that lets edits… | ||
| McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory | Junyoung Jang, Jason Z. S. Hu, Antoine Gaulin, Brigitte Pientka | 36m |
A correct-by-construction Coq implementation of Martin-Löf type theory produces an end-to-end proof checker, with formalized cumulative universe hierarchy and… | ||
| nothing matches | ||