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

Proceedings of the ACM on Programming Languages, Volume 3, Number ICFP, August 18–23, 2019, Berlin, Germany

ICFP – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Sponsors

Compilation and Parallelism

Rebuilding Racket on Chez Scheme (Experience Report)
Matthew Flatt ORCID logo, Caner Derici, R. Kent Dybvig, Andrew W. Keep, Gustavo E. Massaccesi, Sarah Spall, Sam Tobin-Hochstadt, and Jon Zeppieri
(University of Utah, USA; Indiana University, USA; Cisco Systems, USA; University of Buenos Aires, Argentina)
Publisher's Version Info Artifacts Functional
Compiling with Continuations, or without? Whatever.
Youyou CongORCID logo, Leo Osvald, Grégory M. Essertel, and Tiark Rompf ORCID logo
(Tokyo Institute of Technology, Japan; Purdue University, USA)
Publisher's Version
Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning
Akimasa MorihataORCID logo
(University of Tokyo, Japan)
Publisher's Version
Fairness in Responsive Parallelism
Stefan K. Muller, Sam WestrickORCID logo, and Umut A. Acar ORCID logo
(Carnegie Mellon University, USA; Inria, France)
Publisher's Version

Verified Compilation

Narcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formats
Benjamin DelawareORCID logo, Sorawit Suriyakarn, Clément Pit-ClaudelORCID logo, Qianchuan Ye ORCID logo, and Adam ChlipalaORCID logo
(Purdue University, USA; Band Protocol, Thailand; Massachusetts Institute of Technology, USA)
Publisher's Version Artifacts Functional
Closure Conversion Is Safe for Space
Zoe Paraskevopoulou and Andrew W. AppelORCID logo
(Princeton University, USA)
Publisher's Version Artifacts Functional
Linear Capabilities for Fully Abstract Compilation of Separation-Logic-Verified Code
Thomas Van Strydonck, Frank Piessens, and Dominique Devriese ORCID logo
(KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version
The Next 700 Compiler Correctness Theorems (Functional Pearl)
Daniel Patterson and Amal AhmedORCID logo
(Northeastern University, USA)
Publisher's Version Info

Type Theory

Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq
Matthieu Sozeau and Cyprien Mangin
(Inria, France; IRIF, France; University of Paris Diderot, France)
Publisher's Version Info Artifacts Functional
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Andrea Vezzosi, Anders MörtbergORCID logo, and Andreas Abel ORCID logo
(IT University of Copenhagen, Denmark; Stockholm University, Sweden; Carnegie Mellon University, USA; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Publisher's Version Artifacts Functional
Approximate Normalization for Gradual Dependent Types
Joseph Eremondi ORCID logo, Éric TanterORCID logo, and Ronald GarciaORCID logo
(University of British Columbia, Canada; University of Chile, Chile; Inria, France)
Publisher's Version Artifacts Functional

Types 1

Simple Noninterference from Parametricity
Maximilian Algehed and Jean-Philippe Bernardy ORCID logo
(Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Publisher's Version
Selective Applicative Functors
Andrey Mokhov, Georgy Lukyanov, Simon Marlow, and Jeremie Dimino
(Newcastle University, UK; Facebook, UK; Jane Street, UK)
Publisher's Version Artifacts Functional
Coherence of Type Class Resolution
Gert-Jan BottuORCID logo, Ningning Xie, Koar Marntirosian, and Tom Schrijvers ORCID logo
(KU Leuven, Belgium; University of Hong Kong, China)
Publisher's Version

Program Analysis and Synthesis

Relational Cost Analysis for Functional-Imperative Programs
Weihao Qu, Marco Gaboardi, and Deepak GargORCID logo
(SUNY Buffalo, USA; MPI-SWS, Germany)
Publisher's Version Artifacts Functional
Fuzzi: A Three-Level Logic for Differential Privacy
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. PierceORCID logo, and Aaron Roth
(University of Pennsylvania, USA)
Publisher's Version Artifacts Functional
Synthesizing Differentially Private Programs
Calvin Smith and Aws Albarghouthi ORCID logo
(University of Wisconsin-Madison, USA)
Publisher's Version
Synthesizing Symmetric Lenses
Anders Miltner, Solomon Maina, Kathleen Fisher ORCID logo, Benjamin C. PierceORCID logo, David Walker ORCID logo, and Steve ZdancewicORCID logo
(Princeton University, USA; University of Pennsylvania, USA; Tufts University, USA)
Publisher's Version Artifacts Functional

The Real World

Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
Fei Wang, Daniel Zheng, James Decker, Xilun Wu, Grégory M. Essertel, and Tiark Rompf ORCID logo
(Purdue University, USA)
Publisher's Version
Efficient Differentiable Programming in a Functional Array-Processing Language
Amir Shaikhha, Andrew Fitzgibbon ORCID logo, Dimitrios Vytiniotis, and Simon Peyton Jones
(University of Oxford, UK; Microsoft Research, UK; DeepMind, UK)
Publisher's Version
From High-Level Inference Algorithms to Efficient Code
Rajan Walia, Praveen Narayanan, Jacques Carette ORCID logo, Sam Tobin-Hochstadt, and Chung-chieh Shan ORCID logo
(Indiana University, USA; McMaster University, Canada)
Publisher's Version
Sound and Robust Solid Modeling via Exact Real Arithmetic and Continuity
Benjamin Sherman, Jesse Michel, and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA)
Publisher's Version Artifacts Functional

Dependent Types in Haskell

Dependently Typed Haskell in Industry (Experience Report)
David Thrane Christiansen, Iavor S. Diatchki, Robert Dockins, Joe Hendrix, and Tristan Ravitch
(Galois, USA)
Publisher's Version
A Role for Dependent Types in Haskell
Stephanie Weirich ORCID logo, Pritam Choudhury ORCID logo, Antoine Voizard, and Richard A. Eisenberg
(University of Pennsylvania, USA; Bryn Mawr College, USA)
Publisher's Version Artifacts Functional
Higher-Order Type-Level Programming in Haskell
Csongor Kiss, Tony Field, Susan Eisenbach ORCID logo, and Simon Peyton Jones
(Imperial College London, UK; Microsoft Research, UK)
Publisher's Version Artifacts Functional

Program Verification

A Predicate Transformer Semantics for Effects (Functional Pearl)
Wouter SwierstraORCID logo and Tim Baanen
(Utrecht University, Netherlands)
Publisher's Version Artifacts Functional
Dijkstra Monads for All
Kenji Maillard ORCID logo, Danel Ahman ORCID logo, Robert AtkeyORCID logo, Guido Martínez, Cătălin Hriţcu, Exequiel Rivas, and Éric TanterORCID logo
(Inria, France; ENS, France; University of Ljubljana, Slovenia; University of Strathclyde, UK; CIFASIS-CONICET, Argentina; University of Chile, Chile)
Publisher's Version Artifacts Functional
Mechanized Relational Verification of Concurrent Programs with Continuations
Amin Timany and Lars BirkedalORCID logo
(KU Leuven, Belgium; Aarhus University, Denmark)
Publisher's Version Artifacts Functional
Sequential Programming for Replicated Data Stores
Nicholas V. Lewchenko, Arjun Radhakrishna ORCID logo, Akash Gaonkar, and Pavol Černý
(University of Colorado Boulder, USA; Microsoft, USA)
Publisher's Version

Modal Types

Implementing a Modal Dependent Type Theory
Daniel Gratzer, Jonathan Sterling, and Lars BirkedalORCID logo
(Aarhus University, Denmark; Carnegie Mellon University, USA)
Publisher's Version Artifacts Functional
A Reasonably Exceptional Type Theory
Pierre-Marie Pédrot ORCID logo, Nicolas TabareauORCID logo, Hans Jacob Fehrmann, and Éric TanterORCID logo
(Inria, France; University of Chile, Chile)
Publisher's Version Artifacts Functional
Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks
Patrick BahrORCID logo, Christian Uldal Graulund, and Rasmus Ejlers MøgelbergORCID logo
(IT University of Copenhagen, Denmark)
Publisher's Version Artifacts Functional
Quantitative Program Reasoning with Graded Modal Types
Dominic Orchard ORCID logo, Vilem-Benjamin Liepelt, and Harley Eades III ORCID logo
(University of Kent, UK; Augusta University, USA)
Publisher's Version Artifacts Functional

Types 2

Mixed Linear and Non-linear Recursive Types
Bert Lindenhovius, Michael Mislove ORCID logo, and Vladimir Zamdzhiev
(Tulane University, USA; University of Lorraine, France; CNRS, France; Inria, France; LORIA, France)
Publisher's Version
A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference
Jinxu Zhao, Bruno C. d. S. OliveiraORCID logo, and Tom Schrijvers ORCID logo
(University of Hong Kong, China; KU Leuven, Belgium)
Publisher's Version Info Artifacts Functional
An Efficient Algorithm for Type-Safe Structural Diffing
Victor Cacciari Miraldo and Wouter SwierstraORCID logo
(Utrecht University, Netherlands)
Publisher's Version

Lambda-Calculus and Teaching

Call-by-Need Is Clairvoyant Call-by-Value
Jennifer Hackett and Graham Hutton ORCID logo
(University of Nottingham, UK)
Publisher's Version
Teaching the Art of Functional Programming using Automated Grading (Experience Report)
Aliya Hameer and Brigitte PientkaORCID logo
(McGill University, Canada)
Publisher's Version Info Artifacts Functional
Lambda: The Ultimate Sublanguage (Experience Report)
Jeremy YallopORCID logo and Leo White
(University of Cambridge, UK; Jane Street, UK)
Publisher's Version

proc time: 5.98