ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Mon 12 Sep 2022 16:30 - 16:50 at Linhart - (Gradual) Type Theory Chair(s): Jesper Cockx

How can we enumerate the inhabitants of an algebraic datatype? This paper explores a datatype generic solution that works for all regular types and indexed families. The enumerators presented here are provably both complete and unique—they will eventually produce every value exactly once—and fair—they avoid bias when composing enumerators. Finally, these enumerators memoise previously enumerated values whenever possible, thereby avoiding repeatedly recomputing recursive results.

Mon 12 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

15:50 - 16:50
(Gradual) Type TheoryICFP Papers and Events at Linhart
Chair(s): Jesper Cockx TU Delft
15:50
20m
Talk
Propositional Equality for Gradual Dependently Typed Programming
ICFP Papers and Events
Joseph Eremondi University of British Columbia, Ronald Garcia University of British Columbia, Éric Tanter University of Chile
DOI
16:10
20m
Talk
A Reasonably Gradual Type Theory
ICFP Papers and Events
Kenji Maillard Inria Nantes & University of Chile, Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile
DOI
16:30
20m
Talk
A completely unique account of enumeration
ICFP Papers and Events
Cas van der Rest Delft University of Technology, Wouter Swierstra Utrecht University, Netherlands
DOI