ICFP/SPLASH 2025 (series) / TyDe 2025 (series) / TyDe 2025 /
Representing Data Structures with Invariants in Haskell: the cases of BST and AVL [Remote]
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 OctDisplayed time zone: Perth change
Sun 12 Oct
Displayed time zone: Perth change
11:00 - 12:30 | |||
11:00 30mTalk | 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 30mTalk | Towards a Performance Comparison of Syntax and Type-Directed NbE (Extended Abstract) [Remote] TyDe Pre-print | ||
12:00 30mTalk | The conatural numbers form an exponential commutative semiring TyDe Pre-print |