ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Fri 17 Oct 2025 10:30 - 11:00 at Peony SW - Language design Chair(s): Gergő Érdi

We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments that map variables to expressions in some new scope. By statically tracking scopes, users of this library gain confidence that they have correctly maintained the subtle invariants that stem from using de Bruijn indices. Behind the scenes, Rebound uses environments to optimize the application of substitutions, while providing explicit access to these data structures when desired. We demonstrate that this library is expressive by using it to implement a wide range of language features with sophisticated uses of binding and several different operations that use this abstract syntax. Our examples include pi-forall, a tutorial implementation of a type checker for a dependently-typed programming language. Finally, we benchmark Rebound to understand its performance characteristics and find that it produces faster code than competing libraries.

Fri 17 Oct

Displayed time zone: Perth change

10:30 - 12:15
Language designHaskell at Peony SW
Chair(s): Gergő Érdi Standard Chartered Bank
10:30
30m
Research paper
Rebound: Efficient, expressive, and well-scoped binding
Haskell
Noé De Santo University of Pennsylvania, Stephanie Weirich University of Pennsylvania
Link to publication DOI Pre-print
11:00
30m
Research paper
Total Type Classes
Haskell
Robert Weingart Imperial College London, Nicolas Wu Imperial College London
11:30
20m
Talk
Four Years of Embedded Haskell in Critical Real-Time Systems: Lessons and Insights
Haskell
11:50
20m
Talk
Haskell equations, thirty-eight years later
Haskell
Philip Wadler IOG; University of Edinburgh