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

Title Page

Editorial Message

Sponsors

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

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

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

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 Info Artifacts Available Artifacts Functional

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

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 Info Artifacts Available Artifacts Functional

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

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

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

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

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

Publisher's Version Artifacts Functional

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

Publisher's Version

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

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

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

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

Publisher's Version Info Artifacts Functional

Symbolic and Automatic Differentiation of Languages
Conal Elliott 

Publisher's Version

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

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

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

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

Publisher's Version Published Artifact Artifacts Available

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

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 Info Artifacts Available Artifacts Functional

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

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

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

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

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

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

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

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 Info Artifacts Available Artifacts Functional

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

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 Info Artifacts Available Artifacts Functional

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

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