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, 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 Article Search Info Artifacts Available Artifacts Functional
Compiling with Continuations, or without? Whatever.
Youyou Cong, Leo Osvald, Grégory M. Essertel, and Tiark Rompf
(Tokyo Institute of Technology, Japan; Purdue University, USA)
Publisher's Version Article Search
Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning
Akimasa Morihata
(University of Tokyo, Japan)
Publisher's Version Article Search
Fairness in Responsive Parallelism
Stefan K. Muller, Sam Westrick, and Umut A. Acar
(Carnegie Mellon University, USA; Inria, France)
Publisher's Version Article Search

Verified Compilation

Narcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formats
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala
(Purdue University, USA; Band Protocol, Thailand; Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Closure Conversion Is Safe for Space
Zoe Paraskevopoulou and Andrew W. Appel
(Princeton University, USA)
Publisher's Version Article Search Artifacts Functional
Linear Capabilities for Fully Abstract Compilation of Separation-Logic-Verified Code
Thomas Van Strydonck, Frank Piessens, and Dominique Devriese
(KU Leuven, Belgium; Vrije Universiteit Brussel, Belgium)
Publisher's Version Article Search Artifacts Available
The Next 700 Compiler Correctness Theorems (Functional Pearl)
Daniel Patterson and Amal Ahmed
(Northeastern University, USA)
Publisher's Version Article Search 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 Article Search Info Artifacts Available Artifacts Functional
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Andrea Vezzosi, Anders Mörtberg, and Andreas Abel
(IT University of Copenhagen, Denmark; Stockholm University, Sweden; Carnegie Mellon University, USA; Chalmers University of Technology, Sweden; University of Gothenburg, Sweden)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Approximate Normalization for Gradual Dependent Types
Joseph Eremondi, Éric Tanter, and Ronald Garcia
(University of British Columbia, Canada; University of Chile, Chile; Inria, France)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Types 1

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

Program Analysis and Synthesis

Relational Cost Analysis for Functional-Imperative Programs
Weihao Qu, Marco Gaboardi, and Deepak Garg
(SUNY Buffalo, USA; MPI-SWS, Germany)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Fuzzi: A Three-Level Logic for Differential Privacy
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth
(University of Pennsylvania, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Synthesizing Differentially Private Programs
Calvin Smith and Aws Albarghouthi
(University of Wisconsin-Madison, USA)
Publisher's Version Article Search
Synthesizing Symmetric Lenses
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic
(Princeton University, USA; University of Pennsylvania, USA; Tufts University, USA)
Publisher's Version Article Search Artifacts Available 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
(Purdue University, USA)
Publisher's Version Article Search
Efficient Differentiable Programming in a Functional Array-Processing Language
Amir Shaikhha, Andrew Fitzgibbon, Dimitrios Vytiniotis, and Simon Peyton Jones
(University of Oxford, UK; Microsoft Research, UK; DeepMind, UK)
Publisher's Version Article Search
From High-Level Inference Algorithms to Efficient Code
Rajan Walia, Praveen Narayanan, Jacques Carette, Sam Tobin-Hochstadt, and Chung-chieh Shan
(Indiana University, USA; McMaster University, Canada)
Publisher's Version Article Search Artifacts Available
Sound and Robust Solid Modeling via Exact Real Arithmetic and Continuity
Benjamin Sherman, Jesse Michel, and Michael Carbin
(Massachusetts Institute of Technology, USA)
Publisher's Version Article Search Artifacts Available 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 Article Search
A Role for Dependent Types in Haskell
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg
(University of Pennsylvania, USA; Bryn Mawr College, USA)
Publisher's Version Article Search Artifacts Available Artifacts Functional
Higher-Order Type-Level Programming in Haskell
Csongor Kiss, Tony Field, Susan Eisenbach, and Simon Peyton Jones
(Imperial College London, UK; Microsoft Research, UK)
Publisher's Version Article Search Artifacts Available Artifacts Functional

Program Verification

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

Modal Types

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

Types 2

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

Lambda-Calculus and Teaching

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

proc time: 0.71