APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto
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 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
30m
Talk
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
30m
Talk
Random-access lists, from EE to FP
Research Papers
Pierre-Evariste Dagand IRIF / CNRS , Titouan Quennet Université Paris Cité, CNRS, IRIF
12:00
30m
Talk
Generic Reasoning of the Locally Nameless Representation
Research Papers
Yicheng Ni Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University