The Coq mailing list

[Jesper Cockx <jesper AT sikanda.be>]

==========================================================

CALL FOR CONTRIBUTIONS

Second Workshop on the Implementation of Type Systems

August 28th, 2023, Braga, Portugal

https://ifl23.github.io/call_papers_wits.html

==========================================================

=== Important Dates ===

* Abstract Submission Deadline: 30th June, 2023 (AoE)

* Notification: 21st July, 2023 (AoE)

* Workshop: 28th August, 2023 (AoE)

Submission site: https://wits23.hotcrp.com (submissions will open soon)

=== Scope and topics ===

The Second Workshop on the Implementation of Type Systems (WITS 2023) will be held on August 28, 2023, in Braga, Portugal, co-located with IFL 2023. 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. 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.

=== Paper categories ===

We are looking for contributions in two categories:

- Discussion proposals (1 page abstract) should highlight a particular technique or aspect of type system implementation that is applicable to different programming languages. These should not present novel ideas, but rather focus on building a shared understanding between the different communities working on type systems.

- Talk proposals (1 page abstract) should present a novel idea or technique, an implementation of a new type system feature (which can be work in progress), or highlight a particular problem that came up in the implementation of a type system.

Both types of contribution will be evaluated based on their relevance, clarity, and their potential to generate interesting discussions. We especially welcome submissions from people who are new to the field or work in adjacent areas. Reviewing will be single blind, so there is no need to anonymize submissions.

Accepted submissions will be made available publicly on the WITS website. There are no formal proceedings, so you are free to submit work that has also been submitted elsewhere.

=== Program Committee ===

PC Chairs:

- Jesper Cockx (Delft University of Technology, The Netherlands)

- Richard Eisenberg (Jane Street, USA)

Committee Members:

- Guillaume Allais (University of Strathclyde, Scotland)

- Alexis King (Tweag Software Innovation Lab, France)

- Xavier Leroy (Collège de France, France)

- Jon Sterling (Aarhus University, Denmark)

- Sebastian Ullrich (Karlsruhe Institute of Technology, Germany)

Attachment: publickey - jesper AT sikanda.be - 0x42DD5655.asc
Description: application/pgp-keys

Attachment: signature.asc
Description: OpenPGP digital signature