ICFP 2021
Sun 22 - Sat 28 August 2021
Mon 23 Aug 2021 16:30 - 16:45 at ICFP Talks - Session 1
Tue 24 Aug 2021 04:30 - 04:45 at ICFP Talks - Session 1

Transformation of programs into continuation-passing style (CPS) reveals the
notion of continuations, enabling many applications such as control operators
and intermediate representations in compilers. Although type preservation makes
CPS transformation more beneficial, achieving type-preserving CPS transformation
for implicit polymorphism with call-by-value (CBV) semantics is known to be
challenging. We identify the difficulty in the problem that we call scope
intrusion. To address this problem, we propose a new CPS target language
$\Lambda^{open}$ that supports two additional constructs for
polymorphism: one only binds and the other only generalizes type variables.
Unfortunately, their unrestricted use makes $\Lambda^{open}$ unsafe due
to undesired generalization of type variables. We thus equip
$\Lambda^{open}$ with affine types to allow only the type-safe
generalization. We then define a CPS transformation from Curry-style CBV
System F to type-safe $\Lambda^{open}$ and prove that the transformation
is meaning and type preserving. We also study parametricity of
$\Lambda^{open}$ as it is a fundamental property of polymorphic languages
and plays a key role in applications of CPS transformation. To establish
parametricity, we construct a parametric, step-indexed Kripke logical relation
for $\Lambda^{open}$ and prove that it satisfies the Fundamental Property
as well as soundness with respect to contextual equivalence.

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 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 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 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 Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook
DOI Media Attached