ICFP 2020
Proceedings of the ACM on Programming Languages, Volume 4, Number ICFP

Title Page

Editorial Message

Sponsors

A General Approach to Define Binders using Matching Logic
Xiaohong Chen and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)

Publisher's Version

A Quick Look at Impredicativity
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis
(47 Degrees, Spain; Utrecht University, Netherlands; Microsoft Research, UK; DeepMind, UK)

Publisher's Version Video

A Unified View of Modalities in Type Systems
Andreas Abel and Jean-Philippe Bernardy
(University of Gothenburg, Sweden)

Publisher's Version

A Dependently Typed Calculus with Pattern Matching and Erasure Inference
Matúš Tejiščák
(University of St. Andrews, UK)

Publisher's Version Info

Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Kœhler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Compiling Effect Handlers in Capability-Passing Style
Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
(University of Tübingen, Germany)

Publisher's Version

Composing and Decomposing Op-Based CRDTs with Semidirect Products
Matthew Weidner, Heather Miller, and Christopher Meiklejohn
(Carnegie Mellon University, USA)

Publisher's Version

Computation Focusing
Nick Rioux and Steve Zdancewic
(University of Pennsylvania, USA)

Publisher's Version

Cosmo: A Concurrent Separation Logic for Multicore OCaml
Glen Mével, Jacques-Henri Jourdan, and François Pottier
(Inria, France; University of Paris-Saclay, France; CNRS, France; LRI, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Denotational Recurrence Extraction for Amortized Analysis
Joseph W. Cutler, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)

Publisher's Version

Duplo: A Framework for OCaml Post-Link Optimisation
Nandor Licker and Timothy M. Jones
(University of Cambridge, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Effect Handlers, Evidently
Ningning Xie, Jonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster, and Daan Leijen
(Microsoft Research, USA; University of Tübingen, Germany; University of Edinburgh, UK)

Publisher's Version

Effects for Efficiency: Asymptotic Speedup with First-Class Control
Daniel Hillerström, Sam Lindley, and John Longley
(University of Edinburgh, UK; Imperial College London, UK; Heriot-Watt University, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Elaboration with First-Class Implicit Function Types
András Kovács
(Eötvös Loránd University, Hungary)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng
(Swarthmore College, USA; Johns Hopkins University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Kindly Bent to Free Us
Gabriel Radanne, Hannes Saffrich, and Peter Thiemann
(Inria, France; University of Freiburg, Germany)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Kinds Are Calling Conventions
Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg
(University of Oregon, USA; Microsoft Research, UK; Bryn Mawr College, USA; Tweag I/O, USA)

Publisher's Version

Liquid Information Flow Control
Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama
(University of California at San Diego, USA; Carnegie Mellon University, USA; Technion, Israel; Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Liquid Resource Types
Tristan Knoth, Di Wang, Adam Reynolds, Jan Hoffmann, and Nadia Polikarpova
(University of California at San Diego, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Lower Your Guards: A Compositional Pattern-Match Coverage Checker
Sebastian Graf, Simon Peyton Jones, and Ryan G. Scott
(KIT, Germany; Microsoft Research, UK; Indiana University, USA)

Publisher's Version Published Artifact Video Info Artifacts Available Artifacts Functional

Parsing with Zippers (Functional Pearl)
Pierce Darragh and Michael D. Adams
(University of Utah, USA; University of Michigan, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Program Sketching with Live Bidirectional Evaluation
Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh
(University of Chicago, USA; University of Michigan, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M. Kahn, and Jan Hoffmann
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Recovering Purity with Comonads and Capabilities
Vikraman Choudhury and Neel Krishnaswami
(Indiana University, USA; University of Cambridge, UK)

Publisher's Version Info

Regular Language Type Inference with Term Rewriting
Timothée Haudebourg, Thomas Genet, and Thomas Jensen
(University of Rennes, France; Inria, France; CNRS, France; IRISA, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Retrofitting Parallelism onto OCaml
KC Sivaramakrishnan, Stephen Dolan, Leo White, Sadiq Jaffer, Tom Kelly, Anmol Sahoo, Sudha Parimala, Atul Dhiman, and Anil Madhavapeddy
(IIT Madras, India; OCaml Labs, UK; Jane Street, UK; Opsian, UK; University of Cambridge, UK)

Publisher's Version Info Artifacts Functional

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers
(Delft University of Technology, Netherlands; IRIF, France; University of Paris, France; CNRS, France; Aarhus University, Denmark)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional

Sealing Pointer-Based Optimizations behind Pure Functions
Daniel Selsam, Simon Hudon, and Leonardo de Moura
(Microsoft Research, USA; Carnegie Mellon University, USA)

Publisher's Version

Separation Logic for Sequential Programs (Functional Pearl)
Arthur Charguéraud
(Inria, France; University of Strasbourg, France; CNRS, France; ICube, France)

Publisher's Version Info

Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi
(National Institute of Informatics, Japan; SOKENDAI, Japan; University of Tokyo, Japan; Kyoto University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Sparcl: A Language for Partially-Invertible Computation
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Stable Relations and Abstract Interpretation of Higher-Order Programs
Benoît Montagu and Thomas Jensen
(Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Staged Selective Parser Combinators
Jamie Willis, Nicolas Wu, and Matthew Pickering
(Imperial College London, UK; University of Bristol, UK)

Publisher's Version

SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez
(Microsoft Research, USA; Microsoft Research, India; Carnegie Mellon University, USA; Inria, France; University of Ljubljana, Slovenia; CIFASIS-CONICET, Argentina)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Strong Functional Pearl: Harper’s Regular-Expression Matcher in Cedille
Aaron Stump, Christopher Jenkins, Stephan Spahn, and Colin McDonald
(University of Iowa, USA; University of Notre Dame, USA)

Publisher's Version

TLC: Temporal Logic of Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin
(University of California at Riverside, USA)

Publisher's Version

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
Lionel Parreaux
(EPFL, Switzerland)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional