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.
This program is tentative and subject to change.
Sat 25 JanDisplayed time zone: Mountain Time (US & Canada) change
09:00 - 10:30 | |||
09:00 60mKeynote | Invited Talk: Type inference in OCaml and GHC using Levels WITS Richard A. Eisenberg Jane Street | ||
10:00 30mTalk | Towards Generic Higher-Order Unification Implementations in HaskellRemote WITS Nikolai Kudasov Innopolis University, Artem Starikov Innopolis University, Fedor Ivanov Innopolis University, Damir Alfiatonov Innopolis University File Attached | ||
11:00 - 12:30 | |||
11:00 30mTalk | Towards Generic Type Checking Implementations in Haskell via Second-Order Abstract SyntaxRemote WITS Nikolai Kudasov Innopolis University, Anastasia Smirnova Innopolis University, Vladislav Deryabkin Innopolis University, Diana Tomilovskaia Innopolis University, Ekaterina Maksimova Innopolis University File Attached | ||
11:30 30mTalk | McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory WITS Junyoung Jang McGill University, Jason Z.S. Hu Amazon Web Services, USA, Antoine Gaulin McGill University, Brigitte Pientka McGill University Pre-print File Attached | ||
12:00 30mTalk | Eta conversion for the unit type (is still not that simple)Remote WITS András Kovács University of Gothenburg and Chalmers University of Technology File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:30 | |||
14:00 30mOther | Collaboration Time 1 WITS | ||
14:30 30mTalk | Semantic Analysis of Normalisation for Directional Logic ProgrammingRemote WITS Vikraman Choudhury Università di Bologna & Inria OLAS, Neel Krishnaswami University of Cambridge, Ariadne Si Suo University of Cambridge File Attached | ||
15:00 30mTalk | Incremental Bidirectional Typing via Order Maintenance WITS Thomas J. Porter University of Michigan, Marisa Kirisame University of Utah, Liam Mulcahy University of Michigan, Pavel Panchekha University of Utah, Cyrus Omar University of Michigan File Attached | ||
16:00 - 17:30 | |||
16:00 30mOther | Collaboration Time 2 WITS | ||
16:30 30mTalk | Formalizing locally nameless syntax with cofinite quantification WITS Elif Uskuplu Indiana University, Bloomington File Attached | ||
17:00 30mOther | Closing WITS | ||
Accepted Papers
Call for Participation
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.
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://wits25.hotcrp.com/.
Important Dates
- Abstract submission deadline: 10 November, 2024 (AoE)
- Notification: 1 December, 2024
- Workshop in Denver: 25 January, 2025
Attendance and registration
WITS 2025 is colocated with POPL 2025 in Denver, US. Information on registration and attendance will be posted on the POPL website at https://popl25.sigplan.org/.
| Sat 25 Jan 2025 Workshop |
| Sun 1 Dec 2024 Notification |
| Sun 10 Nov 2024 Abstract submission deadline |
Andrej Bauer
University of Ljubljana
Slovenia
Jacques Carette
McMaster University
Canada
Kuen-Bang Hou (Favonia)
University of Minnesota
United States
Chandrakana Nandi
Certora
United States
Gabriel Scherer
Université Paris Cité - Inria - CNRS
France
Nikhil Swamy
Microsoft Research
United States
Sebastian UllrichChair
Lean FRO
Germany