ICFP 2021
Sun 22 - Sat 28 August 2021
Mon 23 Aug 2021 17:00 - 17:15 at ICFP Talks - Session 1
Tue 24 Aug 2021 05:00 - 05:15 at ICFP Talks - Session 1

We develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.

Mon 23 Aug

Displayed time zone: Seoul change

16:00 - 17:30
16:00
15m
Talk
Client-Server Sessions in Linear LogicDistinguished Paper
Research Papers
Zesen Qian Aarhus University, Alex Kavvos University of Bristol, Lars Birkedal Aarhus University
DOI Media Attached
16:15
15m
Talk
An Order-Aware Dataflow Model for Parallel Unix Pipelines
Research 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 Media Attached
16:30
15m
Talk
CPS Transformation with Affine Types for Call-By-Value Implicit Polymorphism
Research Papers
Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan
DOI Media Attached
16:45
15m
Talk
Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingDistinguished Paper
Research Papers
Adam Paszke Google Research, Daniel D. Johnson Google Research, David Kristjanson Duvenaud University of Toronto, Dimitrios Vytiniotis DeepMind, Alexey Radul Google Research, Matthew J. Johnson Google Research, Jonathan Ragan-Kelley MIT CSAIL, Dougal Maclaurin Google Research
DOI Media Attached
17:00
15m
Talk
Propositions-as-Types and Shared State
Research Papers
Pedro Rocha Nova University of Lisbon, Luís Caires Universidade Nova de Lisboa and NOVA LINCS
DOI Media Attached
17:15
15m
Talk
Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations
Research 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 Media Attached

Tue 24 Aug

Displayed time zone: Seoul change

04:00 - 05:30
Session 1Research Papers at ICFP Talks
04:00
15m
Talk
Client-Server Sessions in Linear LogicDistinguished Paper
Research Papers
Zesen Qian Aarhus University, Alex Kavvos University of Bristol, Lars Birkedal Aarhus University
DOI Media Attached
04:15
15m
Talk
An Order-Aware Dataflow Model for Parallel Unix Pipelines
Research 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 Media Attached
04:30
15m
Talk
CPS Transformation with Affine Types for Call-By-Value Implicit Polymorphism
Research Papers
Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan
DOI Media Attached
04:45
15m
Talk
Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingDistinguished Paper
Research Papers
Adam Paszke Google Research, Daniel D. Johnson Google Research, David Kristjanson Duvenaud University of Toronto, Dimitrios Vytiniotis DeepMind, Alexey Radul Google Research, Matthew J. Johnson Google Research, Jonathan Ragan-Kelley MIT CSAIL, Dougal Maclaurin Google Research
DOI Media Attached
05:00
15m
Talk
Propositions-as-Types and Shared State
Research Papers
Pedro Rocha Nova University of Lisbon, Luís Caires Universidade Nova de Lisboa and NOVA LINCS
DOI Media Attached
05:15
15m
Talk
Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations
Research 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 Media Attached