ICFP 2021
Proceedings of the ACM on Programming Languages, Volume 5, Number ICFP

Title Page

Article: icfp21foreword-fm000-p doi:

Editorial Message

Article: icfp21foreword-fm001-p doi:

Sponsors

Article: icfp21foreword-fm003-p doi:

Client-Server Sessions in Linear Logic
Zesen Qian, G. A. Kavvos, and Lars Birkedal
(Aarhus University, Denmark; University of Bristol, UK)

Publisher's Version Distinguished Paper Article: icfp21main-p4-p doi:10.1145/3473567

Persistent Software Transactional Memory in Haskell
Nicolas Krauter, Patrick Raaf, Peter Braam, Reza Salkhordeh, Sebastian Erdweg, and André Brinkmann
(Johannes Gutenberg University Mainz, Germany; University of Oxford, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p6-p doi:10.1145/3473568

An Existential Crisis Resolved: Type Inference for First-Class Existential Types
Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee
(Tweag, France; ENS Lyon, France; University of Pennsylvania, USA)

Publisher's Version Article: icfp21main-p7-p doi:10.1145/3473569

An Order-Aware Dataflow Model for Parallel Unix Pipelines
Shivam Handa, Konstantinos Kallas, Nikos Vasilakis, and Martin C. Rinard
(Massachusetts Institute of Technology, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p20-p doi:10.1145/3473570

Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
Glen Mével and Jacques-Henri Jourdan
(Inria, France; University of Paris-Saclay, France; CNRS, France; ENS Paris-Saclay, France; LMF, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p23-p doi:10.1145/3473571

Modular, Compositional, and Executable Formal Semantics for LLVM IR
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic
(Inria, France; University of Pennsylvania, USA; Taras Shevchenko National University of Kyiv, Ukraine; Carnegie Mellon University, USA; Digamma.ai, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p43-p doi:10.1145/3473572

How to Evaluate Blame for Gradual Types
Lukas Lazarek, Ben Greenman, Matthias Felleisen, and Christos Dimoulas
(Northwestern University, USA; Northeastern University, USA)

Publisher's Version Article: icfp21main-p45-p doi:10.1145/3473573

A Theory of Higher-Order Subtyping with Type Intervals
Sandro Stucki and Paolo G. Giarrusso
(Chalmers University of Technology, Sweden; BedRock Systems, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p46-p doi:10.1145/3473574

Of JavaScript AOT Compilation Performance
Manuel Serrano
(Inria, France; University of Côte d'Azur, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p48-p doi:10.1145/3473575

Generalized Evidence Passing for Effect Handlers: Efficient Compilation of Effect Handlers to C
Ningning Xie and Daan Leijen
(University of Hong Kong, China; Microsoft Research, USA)

Publisher's Version Artifacts Functional Article: icfp21main-p50-p doi:10.1145/3473576

Algebras for Weighted Search
Donnacha Oisín Kidney and Nicolas Wu
(Imperial College London, UK)

Publisher's Version Artifacts Functional Article: icfp21main-p57-p doi:10.1145/3473577

Reasoning about Effect Interaction by Fusion
Zhixuan Yang and Nicolas Wu
(Imperial College London, UK)

Publisher's Version Article: icfp21main-p61-p doi:10.1145/3473578

Deriving Efficient Program Transformations from Rewrite Rules
John M. Li and Andrew W. Appel
(Princeton University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p68-p doi:10.1145/3473579

Contextual Modal Types for Algebraic Effects and Handlers
Nikita Zyuzin and Aleksandar Nanevski
(IMDEA Software Institute, Spain; Universidad Politécnica de Madrid, Spain)

Publisher's Version Article: icfp21main-p78-p doi:10.1145/3473580

Automatic Amortized Resource Analysis with the Quantum Physicist’s Method
David M. Kahn and Jan Hoffmann
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p81-p doi:10.1145/3473581

Catala: A Programming Language for the Law
Denis Merigoux, Nicolas Chataing, and Jonathan Protzenko
(Inria, France; ENS, France; Microsoft Research, USA)

Publisher's Version Artifacts Functional Article: icfp21main-p84-p doi:10.1145/3473582

Symbolic and Automatic Differentiation of Languages
Conal Elliott

Publisher's Version Article: icfp21main-p87-p doi:10.1145/3473583

Propositions-as-Types and Shared State
Pedro Rocha and Luís Caires
(Nova University of Lisbon, Portugal)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p97-p doi:10.1145/3473584

Reasoning about the Garden of Forking Paths
Yao Li, Li-yao Xia, and Stephanie Weirich
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p99-p doi:10.1145/3473585

Theorems for Free from Separation Logic Specifications
Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos
(Aarhus University, Denmark; Concordium, Denmark; University of Nantes, France; Uber, Denmark; Queen Mary University of London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p101-p doi:10.1145/3473586

Calculating Dependently-Typed Compilers (Functional Pearl)
Mitchell Pickard and Graham Hutton
(University of Nottingham, UK)

Publisher's Version Published Artifact Artifacts Available Article: icfp21main-p109-p doi:10.1145/3473587

Grafs: Declarative Graph Analytics
Farzin Houshmand, Mohsen Lesani, and Keval Vora
(University of California at Riverside, USA; Simon Fraser University, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p119-p doi:10.1145/3473588

Certifying the Synthesis of Heap-Manipulating Programs
Yasunari Watanabe, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova, and Ilya Sergey
(Yale-NUS College, Singapore; National University of Singapore, Singapore; University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p124-p doi:10.1145/3473589

Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Martínez, Denis Merigoux, and Tahina Ramananandro
(Carnegie Mellon University, USA; Microsoft Research, India; Microsoft Research, USA; CIFASIS-CONICET, Argentina; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p127-p doi:10.1145/3473590

Compositional Optimizations for CertiCoq
Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel
(Northeastern University, USA; Princeton University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p128-p doi:10.1145/3473591

On Continuation-Passing Transformations and Expected Cost Analysis
Martin Avanzini, Gilles Barthe, and Ugo Dal Lago
(Inria, France; MPI-SP, Germany; University of Bologna, Italy)

Publisher's Version Article: icfp21main-p133-p doi:10.1145/3473592

Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array Programming
Adam Paszke, Daniel D. Johnson, David Duvenaud, Dimitrios Vytiniotis, Alexey Radul, Matthew J. Johnson, Jonathan Ragan-Kelley, and Dougal Maclaurin
(Google Research, Poland; Google Research, Canada; University of Toronto, Canada; DeepMind, UK; Google Research, USA; Massachusetts Institute of Technology, USA)

Publisher's Version Article: icfp21main-p136-p doi:10.1145/3473593

Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)
Xuejing Huang and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p138-p doi:10.1145/3473594

ProbNV: Probabilistic Verification of Network Control Planes
Nick Giannarakis, Alexandra Silva, and David Walker
(University of Wisconsin-Madison, USA; University College London, UK; Cornell University, USA; Princeton University, USA)

Publisher's Version Artifacts Functional Article: icfp21main-p154-p doi:10.1145/3473595

Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations
Chaitanya Koparkar, Mike Rainey, Michael Vollmer, Milind Kulkarni, and Ryan R. Newton
(Indiana University, USA; Carnegie Mellon University, USA; University of Kent, UK; Purdue University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p158-p doi:10.1145/3473596

GhostCell: Separating Permissions from Data in Rust
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer
(MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p176-p doi:10.1145/3473597

Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, and Tetsuya Sato
(Aarhus University, Denmark; MPI-SP, Germany; IMDEA Software Institute, Spain; Boston University, USA; MPI-SWS, Germany; National Institute of Informatics, Japan; Tokyo Institute of Technology, Japan)

Publisher's Version Article: icfp21main-p187-p doi:10.1145/3473598

Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)
Adam Chlipala
(Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: icfp21main-p232-p doi:10.1145/3473599

CPS Transformation with Affine Types for Call-By-Value Implicit Polymorphism
Taro Sekiyama and Takeshi Tsukada
(National Institute of Informatics, Japan; Chiba University, Japan)

Publisher's Version Article: icfp21main-p236-p doi:10.1145/3473600

Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap Fragments
Kimball Germane and Jay McCarthy
(Brigham Young University, USA; University of Massachusetts at Lowell, USA)

Publisher's Version Article: icfp21main-p265-p doi:10.1145/3473601