Skip to content


Folders and files

Last commit message
Last commit date

Latest commit



32 Commits

Repository files navigation

ICFP 2019

Similar pages for older ICFP (2012, 2013, 2014, 2015, 2016, 2017), POPL (2013, 2014, 2015, 2016), and PLDI 2014.

ICFP 2018 (open access):

A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference
Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers

A Reasonably Exceptional Type Theory
Pierre-Marie Pédrot, Nicolas Tabareau, Hans Fehrmann, Éric Tanter

A Role for Dependent Types in Haskell
Stephanie Weirich, Pritam Choudhury, Antoine Voizard, Richard A. Eisenberg

A predicate transformer semantics for effects (Functional Pearl)
Wouter Swierstra, Tim Baanen

An Efficient Algorithm for Type-Safe Structural Diffing
Victor Cacciari Miraldo, Wouter Swierstra

Approximate Normalization for Gradual Dependent Types
Joseph Eremondi, Éric Tanter, Ronald Garcia

Call-By-Need is Clairvoyant Call-By-Value
Jennifer Hackett, Graham Hutton

Closure Conversion is Safe for Space
Zoe Paraskevopoulou, Andrew Appel

Coherence of Type Class Resolution
Gert-Jan Bottu, Ningning Xie, Klara Mardirosian, Tom Schrijvers

Compiling with Continuations, or without? Whatever.
Youyou Cong, Leo Osvald, Gregory Essertel, Tiark Rompf

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Andrea Vezzosi, Anders Mörtberg, Andreas Abel
(preprint code)

Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
Fei Wang, Daniel Zheng, James Decker, Xilun Wu, Gregory Essertel, Tiark Rompf

Dependently Typed Haskell in Industry (Experience Report)
David Thrane Christiansen, Iavor Diatchki, Robert Dockins, Joe Hendrix, Tristan Ravitch

Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hriţcu, Exequiel Rivas, Éric Tanter

Efficient Differentiable Programming in a Functional Array-Processing Language
Amir Shaikhha, Andrew Fitzgibbon, Dimitrios Vytiniotis, Simon Peyton Jones
(2018 paper)

Equations Reloaded
Matthieu Sozeau, Cyprien Mangin

Fairness in Responsive Parallelism
Stefan K. Muller, Sam Westrick, Umut Acar

From high-level inference algorithms to efficient code
Rajan Walia, Praveen Narayanan, Jacques Carette, Sam Tobin-Hochstadt, Chung-chieh Shan

Fuzzi: A Three-Level Logic for Differential Privacy
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, Aaron Roth

Higher-order Type-level Programming in Haskell
Csongor Kiss, Tony Field, Susan Eisenbach, Simon Peyton Jones

Implementing a Modal Dependent Type Theory
Daniel Gratzer, Jonathan Sterling, Lars Birkedal

Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning
Akimasa Morihata

Lambda: the Ultimate Sublanguage (Experience Report)
Jeremy Yallop, Leo White

Linear capabilities for fully abstract compilation of separation-logic-verified code
Thomas Van Strydonck, Frank Piessens, Dominique Devriese

Mechanized Relational Verification of Concurrent Programs with Continuations
Amin Timany, Lars Birkedal
(2018 paper)

Mixed Linear and Non-linear Recursive Types
Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev

Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
(preprint) (code)

Quantitative program reasoning with graded modal types
Dominic Orchard, Vilem-Benjamin Liepelt, Harley D. Eades III

Rebuilding Racket on Chez Scheme (Experience Report)
Matthew Flatt, Caner Derici, R. Kent Dybvig, Andy Keep, Gustavo E. Massaccesi, Sarah Spall, Sam Tobin-Hochstadt, Jon Zeppieri
(2018(?) paper)

Relational Cost Analysis for Functional-Imperative Programs
Weihao Qu, Marco Gaboardi, Deepak Garg

Robust and sound solid modeling via exact real arithmetic and continuity
Benjamin Sherman, Jesse Michel, Michael Carbin

Selective Applicative Functors
Andrey Mokhov, Georgy Lukyanov, Simon Marlow, Jeremie Dimino
(paper) (slides)

Sequential Programming for Replicated Data Stores
Nicholas V. Lewchenko, Arjun Radhakrishna, Akash Gaonkar, Pavol Cerny

Simple Noninterference from Parametricity
Maximilian Algehed, Jean-Philippe Bernardy

Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks
Patrick Bahr, Christian Uldal Graulund, Rasmus Ejlers Møgelberg

Synthesizing Differentially Private Programs
Calvin Smith, Aws Albarghouthi

Synthesizing Symmetric Lenses
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
(2018 paper)

Teaching the Art of Functional Programming Using Automated Grading (Experience Report)
Aliya Hameer, Brigitte Pientka

The Next 700 Compiler Correctness Theorems (Functional Pearl)
Daniel Patterson, Amal Ahmed


ICFP 2019 preprints/papers






No releases published


No packages published