APLAS 2024 (series) / The 22nd Asian Symposium on Programming Languages and Systems /
Random-access lists, from EE to FP
Tue 22 Oct 2024 11:30 - 12:00 at Yamauchi Hall - Type theory and Semantic Frameworks Chair(s): Oleg Kiselyov
What if we could assemble data-types by first picking a recursive structure and then grafting data at selected locations, according to a well-defined blueprint? What if, moreover, this underlying structure had a straightforward semantics in terms of the number of elements it can support? This is the promise of Okasaki’s numerical representations.
This paper offers a journey from Electronic Engineering —computing with binary numbers— to Functional Programming —implementing a persistent random-access list datatype— guided by the type-theoretic framework of McBride’s ornaments.
Tue 22 OctDisplayed time zone: Osaka, Sapporo, Tokyo change
Tue 22 Oct
Displayed time zone: Osaka, Sapporo, Tokyo change
11:00 - 12:30 | Type theory and Semantic FrameworksResearch Papers at Yamauchi Hall Chair(s): Oleg Kiselyov Tohoku University | ||
11:00 30mTalk | Comparing semantic frameworks of dependently-sorted algebraic theories Research Papers Benedikt Ahrens Delft University of Technology, Peter Lefanu Lumsdaine Stockholm University, Paige Randall North Utrecht University | ||
11:30 30mTalk | Random-access lists, from EE to FP Research Papers | ||
12:00 30mTalk | Generic Reasoning of the Locally Nameless Representation Research Papers |