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 Article Search
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 Article Search 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 Article Search
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 Article Search 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 Article Search 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 Article Search 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 Article Search
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 Article Search Artifacts Available Artifacts Functional
Of JavaScript AOT Compilation Performance
Manuel SerranoORCID logo
(Inria, France; University of Côte d'Azur, France)
Publisher's Version Article Search 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 Article Search Artifacts Functional
Algebras for Weighted Search
Donnacha Oisín KidneyORCID logo and Nicolas WuORCID logo
(Imperial College London, UK)
Publisher's Version Article Search Artifacts Functional
Reasoning about Effect Interaction by Fusion
Zhixuan YangORCID logo and Nicolas WuORCID logo
(Imperial College London, UK)
Publisher's Version Article Search
Deriving Efficient Program Transformations from Rewrite Rules
John M. Li ORCID logo and Andrew W. Appel ORCID logo
(Princeton University, USA)
Publisher's Version Article Search 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 Article Search
Automatic Amortized Resource Analysis with the Quantum Physicist’s Method
David M. Kahn and Jan Hoffmann
(Carnegie Mellon University, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Catala: A Programming Language for the Law
Denis Merigoux ORCID logo, Nicolas Chataing, and Jonathan Protzenko
(Inria, France; ENS, France; Microsoft Research, USA)
Publisher's Version Article Search Info Artifacts Functional
Symbolic and Automatic Differentiation of Languages
Conal ElliottORCID logo
Publisher's Version Article Search
Propositions-as-Types and Shared State
Pedro Rocha and Luís CairesORCID logo
(Nova University of Lisbon, Portugal)
Publisher's Version Article Search 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 Article Search 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 Article Search Artifacts Available Artifacts Functional
Calculating Dependently-Typed Compilers (Functional Pearl)
Mitchell Pickard and Graham Hutton
(University of Nottingham, UK)
Publisher's Version Article Search 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 Article Search Artifacts Available Artifacts Functional
Certifying the Synthesis of Heap-Manipulating Programs
Yasunari Watanabe, Kiran Gopinathan, 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 Article Search 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 ORCID logo, and Tahina Ramananandro
(Carnegie Mellon University, USA; Microsoft Research, India; Microsoft Research, USA; CIFASIS-CONICET, Argentina; Inria, France)
Publisher's Version Article Search 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 Article Search Artifacts Available Artifacts Functional
On Continuation-Passing Transformations and Expected Cost Analysis
Martin Avanzini, Gilles Barthe ORCID logo, and Ugo Dal LagoORCID logo
(Inria, France; MPI-SP, Germany; University of Bologna, Italy)
Publisher's Version Article Search
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 Search
Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)
Xuejing Huang ORCID logo and Bruno C. d. S. Oliveira
(University of Hong Kong, China)
Publisher's Version Article Search Artifacts Available Artifacts Functional
ProbNV: Probabilistic Verification of Network Control Planes
Nick Giannarakis, Alexandra Silva ORCID logo, and David Walker
(University of Wisconsin-Madison, USA; University College London, UK; Cornell University, USA; Princeton University, USA)
Publisher's Version Article Search Artifacts Functional
Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations
Chaitanya Koparkar, Mike Rainey, 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 Article Search 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 Article Search 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, Deepak Garg ORCID 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 Article Search
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)
Adam ChlipalaORCID logo
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search 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 Article Search
Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap Fragments
Kimball GermaneORCID logo and Jay McCarthy
(Brigham Young University, USA; University of Massachusetts at Lowell, USA)
Publisher's Version Article Search

proc time: 6.65