SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 16:25 - 16:40 at Zurich E - ICFP 2021 Papers Chair(s): Cyrus Omar

Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program's computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq.

Thu 21 Oct

Displayed time zone: Central Time (US & Canada) change

15:40 - 17:00
ICFP 2021 PapersSIGPLAN Papers at Zurich E
Chair(s): Cyrus Omar University of Michigan
15:40
15m
Talk
An Order-Aware Dataflow Model for Parallel Unix Pipelines
SIGPLAN Papers
Shivam Handa Massachusetts Institute of Technology, Konstantinos Kallas University of Pennsylvania, Nikos Vasilakis Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology
DOI
15:55
15m
Talk
Compositional Optimizations for CertiCoq
SIGPLAN Papers
Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton
DOI
16:10
15m
Talk
Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations
SIGPLAN Papers
Chaitanya S. Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook
DOI
16:25
15m
Talk
Reasoning about the Garden of Forking Paths
SIGPLAN Papers
Yao Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Stephanie Weirich University of Pennsylvania
DOI
16:40
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers