ICFP 2021
Proceedings of the ACM on Programming Languages, Volume 5, Number ICFP
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 5, Number ICFP, August 22–27, 2021, Virtual Event, Republic of Korea

ICFP – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

Client-Server Sessions in Linear Logic
Zesen Qian, G. A. Kavvos, and Lars BirkedalORCID logo
(Aarhus University, Denmark; University of Bristol, UK)
Publisher's Version Distinguished Paper
Persistent Software Transactional Memory in Haskell
Nicolas Krauter ORCID logo, Patrick RaafORCID logo, Peter Braam, Reza SalkhordehORCID logo, Sebastian ErdwegORCID logo, 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. EisenbergORCID logo, Guillaume Duboc, Stephanie Weirich ORCID logo, 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 KallasORCID logo, 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évelORCID logo 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 ZakowskiORCID logo, Calvin Beck ORCID logo, Irene YoonORCID logo, Ilia Zaichuk ORCID logo, Vadim Zaliva ORCID logo, and Steve ZdancewicORCID logo
(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 ORCID logo, Ben Greenman, Matthias Felleisen ORCID logo, and Christos Dimoulas ORCID logo
(Northwestern University, USA; Northeastern University, USA)
Publisher's Version
A Theory of Higher-Order Subtyping with Type Intervals
Sandro StuckiORCID logo 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 SerranoORCID logo
(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 LeijenORCID logo
(University of Hong Kong, China; Microsoft Research, USA)
Publisher's Version Artifacts Functional
Algebras for Weighted Search
Donnacha Oisín KidneyORCID logo and Nicolas WuORCID logo
(Imperial College London, UK)
Publisher's Version Artifacts Functional
Reasoning about Effect Interaction by Fusion
Zhixuan YangORCID logo and Nicolas WuORCID logo
(Imperial College London, UK)
Publisher's Version
Deriving Efficient Program Transformations from Rewrite Rules
John M. Li ORCID logo and Andrew W. Appel ORCID logo
(Princeton University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Contextual Modal Types for Algebraic Effects and Handlers
Nikita Zyuzin ORCID logo and Aleksandar Nanevski ORCID logo
(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 ORCID logo
(Carnegie Mellon University, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Catala: A Programming Language for the Law
Denis Merigoux ORCID logo, Nicolas Chataing, and Jonathan ProtzenkoORCID logo
(Inria, France; ENS, France; Microsoft Research, USA)
Publisher's Version Info Artifacts Functional
Symbolic and Automatic Differentiation of Languages
Conal ElliottORCID logo
Publisher's Version
Propositions-as-Types and Shared State
Pedro Rocha and Luís CairesORCID logo
(Nova University of Lisbon, Portugal)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Reasoning about the Garden of Forking Paths
Yao LiORCID logo, Li-yao Xia ORCID logo, and Stephanie Weirich ORCID logo
(University of Pennsylvania, USA)
Publisher's Version Published Artifact Artifacts Available Artifacts Functional
Theorems for Free from Separation Logic Specifications
Lars BirkedalORCID logo, Thomas Dinsdale-Young, Armaël GuéneauORCID logo, 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 ORCID logo
(University of Nottingham, UK)
Publisher's Version Published Artifact Artifacts Available
Grafs: Declarative Graph Analytics
Farzin Houshmand ORCID logo, Mohsen Lesani ORCID logo, 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 GopinathanORCID logo, George Pîrlea, Nadia PolikarpovaORCID logo, and Ilya SergeyORCID logo
(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 ORCID logo, Nikhil Swamy ORCID logo, Sydney Gibson, Guido Martínez, Denis Merigoux ORCID logo, and Tahina Ramananandro ORCID logo
(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. AppelORCID logo
(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 ORCID logo, Gilles Barthe ORCID logo, and Ugo Dal LagoORCID logo
(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 ORCID logo, Daniel D. Johnson, David Duvenaud, Dimitrios Vytiniotis, Alexey Radul ORCID logo, Matthew J. Johnson ORCID logo, Jonathan Ragan-KelleyORCID logo, and Dougal Maclaurin ORCID logo
(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 ORCID logo and Bruno C. d. S. OliveiraORCID logo
(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 ORCID logo, and David Walker ORCID logo
(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 ORCID logo, Michael Vollmer, Milind KulkarniORCID logo, 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 ORCID logo, Ralf JungORCID logo, and Derek DreyerORCID logo
(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 ORCID logo, Gilles Barthe ORCID logo, Marco Gaboardi ORCID logo, Deepak GargORCID logo, Shin-ya Katsumata ORCID logo, and Tetsuya Sato ORCID logo
(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 ChlipalaORCID logo
(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 ORCID logo and Takeshi Tsukada ORCID logo
(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 GermaneORCID logo and Jay McCarthy ORCID logo
(Brigham Young University, USA; University of Massachusetts at Lowell, USA)
Publisher's Version

proc time: 7.93