WITS 2022 is the first Workshop on the Implementation of Type Systems. The workshop will be held on January 22, 2022, in Philadelphia, PA, United States, 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.

Given the importance of collaboration among the attendees at WITS, if circumstances around covid-19 force POPL (and its co-located events) to go virtual, WITS will be deferred until a time when we can come together safely in person.

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 chairs in case you are unsure if a topic falls within the scope of the workshop.

Important Dates

  • Abstract submission deadline: 16 November, 2021 (AoE)
  • Notification: 1 December, 2021 (AoE)
  • Workshop in Philadelphia: 22 January, 2022

Attendance and registration

WITS 2022 is colocated with POPL 2022 in Philadelphia, USA. More information on registration and attendance will be announced later.

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 22 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Session 1WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
09:00
15m
Talk
CN: A Refinement Type System for CRemote
WITS
Christopher Pulte University of Cambridge, UK, Dhruv Makwana University of Cambridge, Kayvan Memarian University of Cambridge, Jean Pichon-Pharabod Aarhus University, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge
09:15
45m
Other
Type-aware equational rewriting (discussion)In-Person
WITS
09:15
45m
Other
Multi case trees: confluence and coverage (discussion)In-Person
WITS
Tesla Zhang The Pennsylvania State University
09:15
45m
Other
Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)Remote
WITS
Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
File Attached
09:15
45m
Other
The Expression Problem and Theorem Proving (discussion)Remote
WITS
Yao Li University of Pennsylvania, Nick Rioux University of Pennsylvania, Stephanie Weirich University of Pennsylvania
13:30 - 14:45
Session 3WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
13:30
15m
Talk
Tries that matchRemote
WITS
Sebastian Graf Karlsruhe Institute of Technology
13:45
15m
Talk
Gotta prove fast: building an ecosystem for effortless native compilation of tacticsRemote
WITS
Sebastian Ullrich Karlsruhe Institute of Technology
14:00
45m
Other
Benchmarking Binding (discussion)In-Person
WITS
Stephanie Weirich University of Pennsylvania
14:00
45m
Other
Fancy module systems (discussion)Remote
WITS
Jesper Cockx TU Delft
15:05 - 16:20
Session 4WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
15:05
15m
Talk
mitten: A Flexible Multimodal Proof AssistantRemote
WITS
Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University
15:20
15m
Talk
Understandable and Useful Error Messages for Liquid TypesRemote
WITS
Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa
15:35
15m
Talk
Deciding type equivalence with simple grammarsIn-Person
WITS
Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon
15:50
15m
Talk
Typechecking up to CongruenceIn-Person
WITS
Jad Elkhaleq Ghalayini University of Cambridge
16:05
15m
Talk
À bas l’η — Coq’s troublesome η-conversionRemote
WITS
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes
16:40 - 17:30
Session 5WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
16:40
15m
Talk
Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person
WITS
Matthew L. Daggitt Heriot-Watt University, Guillaume Allais University of St Andrews
16:55
15m
Talk
Setting the Record Straight with SingletonsRemote
WITS
Reed Mullanix University of Minnesota
17:10
15m
Talk
First-class pattern synonymsIn-Person
WITS
Tesla Zhang The Pennsylvania State University

Accepted Presentations

Title
À bas l’η — Coq’s troublesome η-conversionRemote
WITS
Benchmarking Binding (discussion)In-Person
WITS
CN: A Refinement Type System for CRemote
WITS
Deciding type equivalence with simple grammarsIn-Person
WITS
First-class pattern synonymsIn-Person
WITS
Gotta prove fast: building an ecosystem for effortless native compilation of tacticsRemote
WITS
Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)Remote
WITS
File Attached
mitten: A Flexible Multimodal Proof AssistantRemote
WITS
Multi case trees: confluence and coverage (discussion)In-Person
WITS
Setting the Record Straight with SingletonsRemote
WITS
The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoqRemote
WITS
The Expression Problem and Theorem Proving (discussion)Remote
WITS
Tries that matchRemote
WITS
Typechecking up to CongruenceIn-Person
WITS
Understandable and Useful Error Messages for Liquid TypesRemote
WITS
Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person
WITS

Call for Contributions

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 even 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.

WITS will be run as a hybrid (in-person and remote) workshop, using the infrastructure used to run a hybrid POPL. This page describes how WITS will play out in its hybrid incarnation. Jesper Cockx will be running the remote fork of WITS; Richard Eisenberg will be running the in-person fork.

First, read How to POPL, which describes how POPL talks will work in a hybrid setting. WITS will follow this format exactly: talks will be a mix of in-person and remote, where audiences both local and global will be able to hear, see, and ask questions. Events on the program are labeled Remote or In-Person depending on their status. (Events that have not yet been labeled are TBD.)

Like for POPL, all talks (in-person and remote) will be streamed on the SIGPLAN YouTube channel and will be made available on YouTube shortly after the workshop.

Discussions are harder to hybridize than talks, so each discussion will either be in-person or remote. Remote attendees can join only remote discussions. In-person attendees can join in-person discussions or, through the use of a headset and laptop, remote discussions.

On the day of WITS, there will be an opportunity to sign up to lead discussions on a topic of your choice. This opportunity will be presented both in-person and remotely. Local participants may choose to lead a remote discussion, if they wish to include remote participants.

In-person participants: please bring your laptop and charger. We’re hoping for opportunities to share code, talk about details, and trade implementation tricks. This works best with a laptop in front of you!

We are hoping to organize a WITS dinner after the workshop. If you will be attending in person and wish to join, please email Richard.

Questions? Use the WITS contact form.