Reasoning about the Garden of Forking Paths
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 OctDisplayed time zone: Central Time (US & Canada) change
15:40 - 17:00 | |||
15:40 15mTalk | 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 15mTalk | Compositional Optimizations for CertiCoq SIGPLAN Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI | ||
16:10 15mTalk | 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 15mTalk | 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 20mLive Q&A | Discussion, Questions and Answers SIGPLAN Papers |