11th Workshop on Type-driven Development (TyDe 2026)

Preliminary Program

Wednesday, August 26

09:00 Invited Talk
When LLMs and Proof Assistants Talk to Each Other
Guillaume Baudart
10:00 Full Paper
Programs and Proofs in Practice [PDF]
Ruben Backx, Sára Juhošová, Wouter Swierstra, Jesper Cockx
10:30 — Break —
11:00 Full Paper
On Eliminating the Impossible with Dependent Types: Choreographic Libraries with Proof-Carrying Located Values
Simon Daniel, Timon Böhler, David Richter, Pascal Weisenburger, Mira Mezini
11:30 Extended Abstract
A Rig of Transformations [PDF]
Emma Tye
12:00 — Lunch —
14:00 — ICFP Watch Party —

Thursday, August 27

09:00 Full Paper
Type-Driven Tokenization for Brahmic Scripts
Sai Hemanth Kapila, Rakshika Bagavathy
10:30 Invited Talk
Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence
Cyril Cohen
10:30 — Break —
11:00 Full Paper
Effects with Variable Binding
Jaro Reinders, Casper Bach, Benedikt Ahrens, Nicolas Wu
11:30 Full Paper
Mechanizing Choreographic Programs and Hoare Logic with State Transformers [PDF]
Timon Böhler, Simon Daniel, David Richter, Pascal Weisenburger, Mira Mezini
12:00 Extended Abstract
From Pattern Unification Towards Pattern Matching Unification [PDF]
David Richter, Timon Böhler
12:30 — Lunch —
14:00 — ICFP Watch Party —

Invited Speakers

When LLMs and proof assistants talk to each other, Guillaume Baudart

Large Language Models (LLMs) are increasingly being applied to scientific domains, and the verification of the output of these models becomes a critical problem. Theorem provers like Rocq, Lean, or Isabelle emerge as natural tools to ground LLMs for rigorous mathematical reasoning. This potential has not been lost on academic and industry players, triggering in the past few months a race toward stronger models for mathematics with impressive recent achievements. In this talk, I will review recent advances at the intersection of LLMs and formal mathematics, from reaching IMO gold medal level with fully formalized proofs to tackling increasingly ambitious research-level problems. I will then present our ongoing works, exploring how to improve model capabilities for formal reasoning, and conversely, how LLMs can be leveraged to improve existing formal mathematics projects.

Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence, Cyril Cohen

In this talk I present Trocq, a heterogeneous substitution framework for dependent type theory, through an introductive tutorial of its implementation in the Rocq prover. Trocq is based on a novel formulation of type equivalence, generalizing the univalent parametricity translation, but taking care of avoiding dependency on the axiom of univalence when possible, and usable with more relations than just equivalences.

Joint work with: Enzo Crance, Assia Mahboubi, Lucie Lahaye, Samy Avrillon and Tomás Vallejos.

Accepted Papers

Goals of the workshop

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 Functional Programmig Workshops 2026, this workshop brings together leading researchers and practitioners who are using or exploring types as a means of program development.

Call for submissions

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.

Submit on HotCRP

Important Dates

All dates are Anywhere on Earth

Date Event
June 3rd Research Papers – Submission Deadline
June 24th Extended Abstracts – Submission Deadline
July 1st Reviews Deadline
July 10th Notification
July 17th Camera-Ready Paper – Submission Deadline
August 26–27th Workshop at FPW26

Program committee

TO BE CONFIRMED

We will aim to have formal proceedings for full-length papers, 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:

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://tyde26.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.