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)
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)
Article Search 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)
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)
Article Search Info 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)
Article Search 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)
Article Search Info Artifacts Functional
How to Evaluate Blame for Gradual Types
Lukas Lazarek, Ben Greenman, Matthias Felleisen, and Christos Dimoulas
(Northwestern University, USA; Brown University, USA; Northeastern University, USA)
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)
Article Search Archive submitted (940 kB) Artifacts Functional
Of JavaScript AOT Compilation Performance
Manuel SerranoORCID logo
Article Search 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)
Article Search Artifacts Functional
Algebras for Weighted Search
Donnacha Oisín KidneyORCID logo and Nicolas WuORCID logo
(Imperial College London, UK)
Article Search Artifacts Functional
Reasoning about Effect Interaction by Fusion
Zhixuan YangORCID logo and Nicolas WuORCID logo
(Imperial College London, UK)
Preprint Archive submitted (1.5 MB)
Deriving Efficient Program Transformations from Rewrite Rules
John M. Li ORCID logo and Andrew W. Appel ORCID logo
(Princeton University, USA)
Article Search Artifacts Functional
Contextual Modal Types for Algebraic Effects and Handlers
Nikita Zyuzin ORCID logo and Aleksandar Nanevski ORCID logo
(Universidad Politécnica de Madrid, Spain; IMDEA Software Institute, Spain)
Article Search
Automatic Amortized Resource Analysis with the Quantum Physicist’s Method
David M. Kahn and Jan Hoffmann
(Carnegie Mellon University, USA)
Article Search 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)
Preprint Info Artifacts Functional
Symbolic and Automatic Differentiation of Languages
Conal ElliottORCID logo
Article Search
Propositions-as-Types and Shared State
Pedro Rocha and Luís CairesORCID logo
(Nova University of Lisbon, Portugal)
Article Search 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)
Preprint 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, UK; University of Nantes, France; Uber, n.n.; Queen Mary University of London, UK)
Preprint Artifacts Functional
Calculating Dependently-Typed Compilers (Functional Pearl)
Mitchell Pickard and Graham Hutton
(University of Nottingham, UK)
Article Search
Grafs: Declarative Graph Analytics
Farzin Houshmand, Mohsen Lesani, and Keval Vora
(University of California at Riverside, USA; Simon Fraser University, Canada)
Article Search 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)
Preprint Info 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)
Article Search Artifacts Functional
Compositional Optimizations for CertiCoq
Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel
(Northeastern University, USA; Princeton University, USA)
Article Search Artifacts Functional
On Continuation-Passing Transformations and Expected Cost Analysis
Martin Avanzini, Gilles Barthe, and Ugo Dal LagoORCID logo
(Inria, France; MPI-SP, Germany; IMDEA Software Institute, Spain; University of Bologna, Italy)
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)
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)
Article Search 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; Princeton University, USA)
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)
Article Search Artifacts Functional
GhostCell: Separating Permissions from Data in Rust
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer
(MPI-SWS, Germany)
Preprint Info Artifacts Functional
Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics
Alejandro Aguirre ORCID logo, Gilles Barthe, Marco Gaboardi, Deepak Garg ORCID logo, Shin-ya Katsumata ORCID logo, 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)
Article Search
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)
Adam ChlipalaORCID logo
(Massachusetts Institute of Technology, USA)
Article Search Info 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)
Article Search Archive submitted (660 kB)
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)
Article Search

proc time: 12.8