xOur data center is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Wed 25 Aug 2021 20:00 - 20:15 at ICFP Talks - Session 6
Thu 26 Aug 2021 08:00 - 08:15 at ICFP Talks - Session 6

The Rust language offers a promising approach to safe systems programming based on the principle of \emph{aliasing XOR mutability}: a value may be \emph{either} aliased \emph{or} mutable, but not both at the same time. However, to implement pointer-based data structures with internal sharing, such as graphs or doubly-linked lists, we need to be able to mutate aliased state. To support such data structures, Rust provides a number of APIs that offer so-called \emph{interior mutability}: the ability to mutate data via method calls on a shared reference. Unfortunately, the existing APIs sacrifice flexibility, concurrent access, and/or performance, in exchange for safety.

In this paper, we propose a new Rust API called GhostCell which avoids such sacrifices by \emph{separating permissions from data}: it enables the user to safely synchronize access to a \emph{collection} of data via a single permission. GhostCell repurposes an old trick from typed functional programming: \emph{branded types} (as exemplified by Haskell's \texttt{ST} monad), which combine phantom types and rank-2 polymorphism to simulate a lightweight form of state-dependent types. We have formally proven the soundness of GhostCell by adapting and extending RustBelt, a semantic soundness proof for a representative subset of Rust, mechanized in Coq.

Wed 25 Aug

Displayed time zone: Seoul change

19:00 - 20:45
19:00
15m
Talk
Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap Fragments
Research Papers
Kimball Germane Brigham Young University, Jay McCarthy University of Massachusetts Lowell
DOI Media Attached
19:15
15m
Talk
Grafs: Declarative Graph Analytics
Research Papers
Farzin Houshmand University of California at Riverside, Mohsen Lesani University of California at Riverside, Keval Vora Simon Fraser University
DOI Media Attached
19:30
15m
Talk
Certifying the Synthesis of Heap-Manipulating Programs
Research Papers
Yasunari Watanabe Yale-NUS College; National University of Singapore, Kiran Gopinathan National University of Singapore, George Pîrlea National University of Singapore, Singapore, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore
DOI Pre-print Media Attached
19:45
15m
Talk
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)
Research Papers
Adam Chlipala Massachusetts Institute of Technology
DOI Media Attached
20:00
15m
Talk
GhostCell: Separating Permissions from Data in Rust
Research Papers
Joshua Yanovski MPI-SWS, Hoang-Hai Dang MPI-SWS, Ralf Jung MPI-SWS, Derek Dreyer MPI-SWS
DOI Media Attached
20:15
15m
Talk
Catala: A Programming Language for the Law
Research Papers
Denis Merigoux INRIA, Nicolas Chataing ENS Paris, Jonathan Protzenko Microsoft Research, Redmond
DOI Media Attached
20:30
15m
Talk
Persistent Software Transactional Memory in Haskell
Research Papers
Nicolas Krauter Johannes Gutenberg University Mainz, Patrick Raaf Johannes Gutenberg University Mainz, Peter Braam University of Oxford, Reza Salkordeh Johannes Gutenberg-Universität Mainz, Sebastian Erdweg JGU Mainz, André Brinkmann Johannes Gutenberg U Mainz
DOI Media Attached

Thu 26 Aug

Displayed time zone: Seoul change

07:00 - 08:45
Session 6Research Papers at ICFP Talks
07:00
15m
Talk
Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap Fragments
Research Papers
Kimball Germane Brigham Young University, Jay McCarthy University of Massachusetts Lowell
DOI Media Attached
07:15
15m
Talk
Grafs: Declarative Graph Analytics
Research Papers
Farzin Houshmand University of California at Riverside, Mohsen Lesani University of California at Riverside, Keval Vora Simon Fraser University
DOI Media Attached
07:30
15m
Talk
Certifying the Synthesis of Heap-Manipulating Programs
Research Papers
Yasunari Watanabe Yale-NUS College; National University of Singapore, Kiran Gopinathan National University of Singapore, George Pîrlea National University of Singapore, Singapore, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore
DOI Pre-print Media Attached
07:45
15m
Talk
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)
Research Papers
Adam Chlipala Massachusetts Institute of Technology
DOI Media Attached
08:00
15m
Talk
GhostCell: Separating Permissions from Data in Rust
Research Papers
Joshua Yanovski MPI-SWS, Hoang-Hai Dang MPI-SWS, Ralf Jung MPI-SWS, Derek Dreyer MPI-SWS
DOI Media Attached
08:15
15m
Talk
Catala: A Programming Language for the Law
Research Papers
Denis Merigoux INRIA, Nicolas Chataing ENS Paris, Jonathan Protzenko Microsoft Research, Redmond
DOI Media Attached
08:30
15m
Talk
Persistent Software Transactional Memory in Haskell
Research Papers
Nicolas Krauter Johannes Gutenberg University Mainz, Patrick Raaf Johannes Gutenberg University Mainz, Peter Braam University of Oxford, Reza Salkordeh Johannes Gutenberg-Universität Mainz, Sebastian Erdweg JGU Mainz, André Brinkmann Johannes Gutenberg U Mainz
DOI Media Attached