ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Sun 12 Oct 2025 11:00 - 11:30 at Seminar Room 2 - Session 1

Invariants are an essential aspect to take into account for the correct implementation of data structures and their operations. This paper explores how to encode and enforce invariants at type level in Haskell, using Binary Search Trees (BSTs) and AVL trees as case studies. This means the encoding of invariants at type level using advanced features of Haskell type system and their later verification by the type checker. We compare three approaches for the type-level encoding of invariants: fully externalist, externalist, and internalist, each offering a different balance between modularity, safety, and complexity. We also show how to systematically extract standard implementations from correct, invariant-based code.

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