Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional ProgramsVirtual
Wed 20 Oct 2021 19:20 - 19:35 at Zurich D - Functional Programming - Mirror Chair(s): Atsushi Igarashi
Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, $\lambda^*$ , which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization.
Wed 20 OctDisplayed time zone: Central Time (US & Canada) change
10:50 - 12:10 | |||
10:50 15mTalk | Compiling with Continuations, CorrectlyVirtual OOPSLA DOI | ||
11:05 15mTalk | Synbit: Synthesizing Bidirectional Programs using Unidirectional SketchesVirtual OOPSLA Masaomi Yamaguchi Tohoku University, Kazutaka Matsuda Tohoku University, Cristina David University of Bristol, Meng Wang University of Bristol DOI | ||
11:20 15mTalk | Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional ProgramsVirtual OOPSLA Yuyan Bao University of Waterloo, Guannan Wei Purdue University, Oliver Bračevac Purdue University, Yuxuan Jiang Purdue University, Qiyang He Purdue University, Tiark Rompf Purdue University DOI | ||
11:35 15mTalk | Efficient Compilation of Algebraic Effect HandlersVirtual OOPSLA Georgios Karachalias Tweag, Filip Koprivec University of Ljubljana; Institute of Mathematics, Matija Pretnar University of Ljubljana; Institute of Mathematics, Tom Schrijvers KU Leuven DOI | ||
11:50 20mLive Q&A | Discussion, Questions and Answers OOPSLA |