ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore

This program is tentative and subject to change.

Sun 12 Oct 2025 11:30 - 12:00 at Seminar Room 2 - Session 1

A key part of any dependent type-checker is the method for checking whether two types are equal. A common claim is that syntax-directed equality is more performant, although type-directed equality is more expressive. However, this claim is difficult to make precise, since implementations choose only one or the other approach, making a direct comparison impossible. We present some work-in-progress developing a realistic platform for direct, apples-to-apples, comparison of the two approaches, quantifying how much slower type-directed equality checking is, and analyzing why and how it can be improved.

This program is tentative and subject to change.

Sun 12 Oct

Displayed time zone: Perth change

11:00 - 12:30
Session 1TyDe at Seminar Room 2
11:00
30m
Talk
Representing Data Structures with Invariants in Haskell: the cases of BST and AVL [Remote]
TyDe
Nicolas Rodriguez Instituto de Computación, Universidad de la República, Alberto Pardo Universidad de la Republica, Uruguay, Marcos Viera University of the Republic, Uruguay
11:30
30m
Talk
Towards a Performance Comparison of Syntax and Type-Directed NbE (Extended Abstract) [Remote]
TyDe
Chester Gould University of British Columbia, William J. Bowman University of British Columbia
Pre-print
12:00
30m
Talk
The conatural numbers form an exponential commutative semiring
TyDe
Szumi Xie Eötvös Loránd University (ELTE), Viktor Bense Eötvös Loránd University (ELTE)
Pre-print