Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Wed 26 Aug 2020 12:00 - 12:15 at ICFP NY 5 - New York 5 Chair(s): Richard A. Eisenberg
Wed 26 Aug 2020 23:00 - 23:15 at ICFP Asia 5 - Asia 5 Chair(s): Richard A. Eisenberg

In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a comonadic type discipline.

We establish the correctness of our type system via a simple denotational model, which we call the capability space model. Our model formalises the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is capability-safe if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the call-by-value $\beta$ and $\eta$ laws) for the imperative lambda calculus, and show its soundness relative to this semantics.

Finally, we give a translation of the pure simply-typed lambda calculus into our comonadic imperative calculus, and show that any two terms which are $\beta\eta$-equal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equation-preserving way into our imperative calculus.

Conference Day
Wed 26 Aug

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

11:00 - 13:00
New York 5ICFP Program at ICFP NY 5
Chair(s): Richard A. EisenbergTweag I/O

Public livestreams: YouTube, Bilibili (China)

11:00
15m
Talk
Denotational Recurrence Extraction for Amortized Analysis
ICFP Program
Joseph W. CutlerWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan University
DOI Media Attached
11:15
15m
Talk
Separation Logic for Sequential Programs (Functional Pearl)
ICFP Program
DOI Media Attached
11:30
15m
Talk
Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille
ICFP Program
Aaron StumpThe University of Iowa, USA, Chris JenkinsThe University of Iowa, Stephan SpahnThe University of Iowa, Colin McDonaldUniversity of Notre Dame
DOI Media Attached
11:45
15m
Talk
Duplo: A Framework for OCaml Post-Link Optimisation
ICFP Program
Nandor LickerUniversity of Cambridge, Timothy M. JonesUniversity of Cambridge, UK
DOI Media Attached
12:00
15m
Talk
Recovering Purity with Comonads and Capabilities
ICFP Program
Vikraman ChoudhuryIndiana University & University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge
DOI Media Attached
12:15
15m
Talk
A General Approach to Define Binders Using Matching Logic
ICFP Program
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
DOI Media Attached
12:30
15m
Talk
Parsing with Zippers (Functional Pearl)
ICFP Program
Pierce DarraghUniversity of Utah, Michael D. AdamsUniversity of Michigan
DOI Media Attached
12:45
15m
Talk
Regular Language Type Inference with Term Rewriting
ICFP Program
Timothée HaudebourgUniv Rennes, Inria, CNRS, IRISA, Thomas GenetIRISA, Univ Rennes, Thomas P. JensenINRIA Rennes
DOI Media Attached
22:30 - 00:00
Asia 5ICFP Program at ICFP Asia 5
Chair(s): Richard A. EisenbergTweag I/O

Public livestreams: YouTube, Bilibili (China)

22:00
30m
Talk
Denotational Recurrence Extraction for Amortized Analysis
ICFP Program
Joseph W. CutlerWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan University
DOI Media Attached
22:15
15m
Talk
Separation Logic for Sequential Programs (Functional Pearl)
ICFP Program
DOI Media Attached
22:30
15m
Talk
Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille
ICFP Program
Aaron StumpThe University of Iowa, USA, Chris JenkinsThe University of Iowa, Stephan SpahnThe University of Iowa, Colin McDonaldUniversity of Notre Dame
DOI Media Attached
22:45
15m
Talk
Duplo: A Framework for OCaml Post-Link Optimisation
ICFP Program
Nandor LickerUniversity of Cambridge, Timothy M. JonesUniversity of Cambridge, UK
DOI Media Attached
23:00
15m
Talk
Recovering Purity with Comonads and Capabilities
ICFP Program
Vikraman ChoudhuryIndiana University & University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge
DOI Media Attached
23:15
15m
Talk
A General Approach to Define Binders Using Matching Logic
ICFP Program
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
DOI Media Attached
23:30
15m
Talk
Parsing with Zippers (Functional Pearl)
ICFP Program
Pierce DarraghUniversity of Utah, Michael D. AdamsUniversity of Michigan
DOI Media Attached
23:45
15m
Talk
Regular Language Type Inference with Term Rewriting
ICFP Program
Timothée HaudebourgUniv Rennes, Inria, CNRS, IRISA, Thomas GenetIRISA, Univ Rennes, Thomas P. JensenINRIA Rennes
DOI Media Attached