ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia

The Workshop on Type-Driven Development (TyDe) aims to show how static type information may be used effectively in the development of computer programs. Co-located with ICFP, this workshop brings together leading researchers and practitioners who are using or exploring types as a means of program development.

We welcome all contributions, both theoretical and practical, on a range of topics including:

  • dependently typed programming;
  • generic programming;
  • design and implementation of programming languages, exploiting types in novel ways;
  • exploiting typed data, data dependent data, or type providers;
  • static and dynamic analyses of typed programs;
  • tools, IDEs, or testing tools exploiting type information;
  • pearls, being elegant, instructive examples of types used in the derivation, calculation, or construction of programs.

For information about the TyDe workshop series, see the permanent website.

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

Sun 11 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

08:00 - 09:00
RegistrationCatering & social at Foyer 2 +120h +48h +96h +72h

All speakers speaking in the morning session should arrive early to submit the slides. We recommend that you arrive already at 8:00.

08:00
60m
Registration
Registration
Catering & social

09:00 - 10:30
TyDe 1TyDe at Club CD
Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica
09:00
18m
Full-paper
A Hoare-Logic Style Refinement Types FormalisationVirtual
TyDe
Zilin Chen UNSW Sydney
Link to publication DOI
09:18
18m
Full-paper
Computing with Generic Trees in Agda
TyDe
09:36
18m
Short-paper
Contextual Algebraic Theories: Generic Boilerplate beyond Abstraction (Extended Abstract)
TyDe
Andreas Nuyts KU Leuven, Belgium
Link to publication
09:54
18m
Short-paper
Provingly Correct Optimisations on Intrinsically Typed Expressions (Extended Abstract)
TyDe
Matthias Heinzel Utrecht University
Pre-print
10:12
18m
Full-paper
Structural Refinement Types
TyDe
David Binder University of Tübingen, Ingo Skupin University of Tübingen, David Läwen University of Tübingen, Germany, Klaus Ostermann University of Tübingen
Pre-print
10:30 - 11:00
Coffee breakCatering & social at Foyer 2 +96h +120h
10:30
30m
Coffee break
Coffee break
Catering & social

11:00 - 12:30
Tyde 2TyDe at Club CD
Chair(s): Gabriel Scherer INRIA Saclay
11:00
18m
Short-paper
Idris2-Table: evaluating dependently-typed tables with the Brown Benchmark for Table Types (Extended Abstract)
TyDe
Robert Wright The University of Edinburgh, UK, Michel Steuwer University of Edinburgh, Ohad Kammar University of Edinburgh
11:18
18m
Short-paper
Syntax-Generic Operations, Reflectively Reified (Extended Abstract)
TyDe
Tzu-Chi Lin Institute of Information Science, Academia Sinica, Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica
Pre-print
11:36
18m
Short-paper
Toward Grammar Inference via Refinement Types (Extended Abstract)
TyDe
Pre-print Media Attached
11:54
18m
Short-paper
Towards Dependently-Typed Control Effects (Extended Abstract)Virtual
TyDe
Youyou Cong Tokyo Institute of Technology, Kenichi Asai Ochanomizu University
File Attached
12:12
18m
Full-paper
tylr, a tiny tile-based structure editor
TyDe
David Moon University of Michigan, Andrew Blinn University of Michigan, Cyrus Omar University of Michigan
DOI Pre-print
12:30 - 14:00
LunchCatering & social at Foyer 2 +120h +96h
12:30
90m
Lunch
Lunch
Catering & social

14:00 - 15:30
TyDe 3 / Zena's Birthday 1TyDe at Club CD
Chair(s): Gabriel Scherer INRIA Saclay, Marco Gaboardi Boston University
14:00
18m
Short-paper
Normalization by Evaluation with Free Extensions (Extended Abstract)
TyDe
Nathan Corbyn University of Oxford, Ohad Kammar University of Edinburgh, Sam Lindley The University of Edinburgh, UK, Nachiappan Valliappan Chalmers University of Technology, Jeremy Yallop University of Cambridge
Pre-print
14:18
18m
Talk
Zena's birthday introduction
TyDe
Marco Gaboardi Boston University
14:36
18m
Talk
Compiling without continuations
TyDe
Simon Peyton Jones Epic Games
14:54
18m
Talk
On the power of syntactic methods: It is all syntax after all…
TyDe
Amr Sabry Indiana University
15:12
18m
Talk
The impact of delimited control and call-by-need in proof theory
TyDe
15:30 - 16:00
Coffee breakCatering & social at Foyer 2 +96h +120h
15:30
30m
Coffee break
Coffee break
Catering & social

16:00 - 17:30
Zena's Birthday 2TyDe at Club CD
Chair(s): Marco Gaboardi Boston University
16:00
18m
Talk
A Computational Interpretation of Girard's Intuitionistic Proof-Nets
TyDe
Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France
16:18
18m
Talk
Duality of intersection and union types - where and how?
TyDe
Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA
16:36
18m
Talk
Mu tilde (re)cycled
TyDe
Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt
16:54
18m
Talk
OPLSS over twenty years (online)
TyDe
Robert Harper Carnegie Mellon University
17:12
18m
Talk
Happy Birthday, Zena!
TyDe

Call for Papers

The Workshop on Type-Driven Development (TyDe) aims to show how static type information may be used effectively in the development of computer programs. Co-located with ICFP, this workshop brings together leading researchers and practitioners who are using or exploring types as a means of program development.

We welcome all contributions, both theoretical and practical, on a range of topics including:

  • dependently typed programming;
  • generic programming;
  • design and implementation of programming languages, exploiting types in novel ways;
  • exploiting typed data, data dependent data, or type providers;
  • static and dynamic analyses of typed programs;
  • tools, IDEs, or testing tools exploiting type information;
  • pearls, being elegant, instructive examples of types used in the derivation, calculation, or construction of programs.

Proceedings and Copyright

We will have formal proceedings, published by the ACM. Accepted papers will be included in the ACM Digital Library. Authors must grant ACM publication rights upon acceptance, but may retain copyright if they wish. Authors are encouraged to publish auxiliary material with their paper (source code, test data, and so forth). The proceedings will be freely available for download from the ACM Digital Library from one week before the start of the conference until two weeks after the conference.

The official publication date is the date the papers are made available in the ACM Digital Library. This date may be up to two weeks prior to the first day of the conference. The official publication date affects the deadline for any patent filings related to published work.

Submission Details

Submissions should fall into one of two categories:

  • regular research papers (12 pages);
  • extended abstracts (3 pages).

The bibliography will not be counted against the page limits for either category.

Regular research papers are expected to present novel and interesting research results, and will be included in the formal proceedings. Extended abstracts should report work in progress that the authors would like to present at the workshop. Extended abstracts will be distributed to workshop attendees but will not be published in the formal proceedings.

We welcome submissions from PC members (with the exception of the two co-chairs), but these submissions will be held to a higher standard.

Submission is handled through HotCRP:

https://tyde22.hotcrp.com

All submissions should be in portable document format (PDF) and formatted using the ACM SIGPLAN style guidelines:

https://www.sigplan.org/Resources/Author/

Note that submissions should use the new ‘acmart’ format and the two-column ‘sigplan’ subformat (not to be confused with the one-column ‘acmsmall’ subformat).

Extended abstracts must be submitted with the label ‘Extended Abstract’ clearly in the title.

Participant Support

Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover participation-related expenses. PAC also offers other support, such as for child-care expenses during the meeting or for accommodations for members with physical disabilities. For details on the PAC program, see its web page:

https://www.sigplan.org/PAC/