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

Proceedings of the ACM on Programming Languages, Volume 4, Number ICFP, August 23–28, 2020, Virtual Event, USA

ICFP – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

A General Approach to Define Binders using Matching Logic
Xiaohong Chen and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA)
Article Search
A Quick Look at Impredicativity
Alejandro Serrano, Jurriaan Hage, Simon Peyton Jones, and Dimitrios Vytiniotis
(47 Degrees, n.n.; Utrecht University, Netherlands; Microsoft Research, UK; DeepMind, UK)
Article Search Video
A Unified View of Modalities in Type Systems
Andreas Abel and Jean-Philippe Bernardy
(University of Gothenburg, Sweden)
Article Search Archive submitted (1 MB)
A Dependently Typed Calculus with Pattern Matching and Erasure Inference
Matúš Tejiščák
(University of St. Andrews, UK)
Article Search Info
Achieving High-Performance the Functional Way: A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; University of Glasgow, UK)
Article Search Artifacts Functional
Compiling Effect Handlers in Capability-Passing Style
Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann
(University of Tübingen, Germany)
Preprint
Composing and Decomposing Op-Based CRDTs with Semidirect Products
Matthew Weidner, Christopher Meiklejohn, and Heather Miller
(Carnegie Mellon University, USA)
Article Search
Computation Focusing
Nick Rioux and Steve Zdancewic
(University of Pennsylvania, USA)
Article Search
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)
Article Search Artifacts Functional
Denotational Recurrence Extraction for Amortized Analysis
Joseph Cutler, Daniel R. Licata, and Norman Danner
(Wesleyan University, USA)
Preprint
Duplo: A Framework for OCaml Post-Link Optimisation
Nandor Licker and Timothy M. Jones
(University of Cambridge, UK)
Preprint 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)
Article Search
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)
Article Search Artifacts Functional
Elaboration with First-Class Implicit Function Types
András Kovács
(Eötvös Loránd University, Hungary)
Article Search Artifacts Functional
Higher-Order Demand-Driven Symbolic Evaluation
Zachary Palmer, Theodore Park, Scott Smith, and Shiwei Weng
(Swarthmore College, n.n.; Hopkins, n.n.; Johns Hopkins University, USA)
Article Search Archive submitted (2 MB) Artifacts Functional
Kindly Bent to Free Us
Gabriel Radanne, Hannes Saffrich, and Peter Thiemann
(Inria, France; University of Freiburg, Germany)
Preprint Info 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)
Article Search
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)
Article Search 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)
Article Search Artifacts Functional
Lower Your Guards
Sebastian Graf, Simon Peyton Jones, and Ryan G. Scott
(KIT, Germany; Microsoft Research, UK; Indiana University, USA)
Article Search Archive submitted (1 MB) Artifacts Functional
Parsing with Zippers (Functional Pearl)
Pierce Darragh and Michael D. Adams
(University of Utah, USA; University of Michigan, USA)
Article Search 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)
Preprint Artifacts Functional
Raising Expectations: Automating Expected Cost Analysis with Types
Di Wang, David M. Kahn, and Jan Hoffmann
(Carnegie Mellon University, USA)
Article Search Artifacts Functional
Recovering Purity with Comonads and Capabilities
Vikraman Choudhury and Neel Krishnaswami
(Indiana University, USA; University of Cambridge, UK)
Article Search 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)
Article Search 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)
Preprint 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)
Preprint Info Artifacts Functional
Sealing Pointer-Based Optimizations Behind Pure Functions
Daniel Selsam, Simon Hudon, and Leonardo de Moura
(Microsoft Research, USA; Carnegie Mellon University, USA)
Preprint Archive submitted (6 MB)
Separation Logic for Sequential Programs (Functional Pearl)
Arthur Charguéraud
(Inria, France)
Article Search Info
Signature Restriction for Polymorphic Algebraic Effects
Taro Sekiyama, Takeshi Tsukada, and Atsushi Igarashi
(National Institute of Informatics, Japan; University of Tokyo, Japan; Kyoto University, Japan)
Preprint Archive submitted (0 MB) Artifacts Functional
Sparcl: A Language for Partially-Invertible Computation
Kazutaka Matsuda and Meng Wang
(Tohoku University, Japan; University of Bristol, UK)
Article Search Artifacts Functional
Stable Relations and Abstract Interpretation of Higher-Order Programs
Benoît Montagu and Thomas Jensen
(Inria, France)
Article Search Artifacts Functional
Staged Selective Parser Combinators
Jamie Willis, Nicolas Wu, and Matthew Pickering
(Imperial College London, UK; University of Bristol, UK)
Article Search
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)
Article Search 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)
Article Search
Temporal Logic of Composable Distributed Components
Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin
(University of California at Riverside, USA)
Article Search
The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
Lionel Parreaux
(EPFL, Switzerland)
Article Search Artifacts Functional

proc time: 13.13