ICFP 2019

39 papers

1. A mechanical formalization of higher-ranked polymorphic type inference · Jinxu Zhao, Bruno C. d. S. Oliveira, Tom Schrijvers
2. A predicate transformer semantics for effects (functional pearl) · Wouter Swierstra, Tim Baanen
3. A reasonably exceptional type theory · Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, Éric Tanter
4. A role for dependent types in Haskell · Stephanie Weirich, Pritam Choudhury, Antoine Voizard, Richard A. Eisenberg
5. An efficient algorithm for type-safe structural diffing · Victor Cacciari Miraldo, Wouter Swierstra
6. Approximate normalization for gradual dependent types · Joseph Eremondi, Éric Tanter, Ronald Garcia
7. Call-by-need is clairvoyant call-by-value · Jennifer Hackett, Graham Hutton
8. Closure conversion is safe for space · Zoe Paraskevopoulou, Andrew W. Appel
9. Coherence of type class resolution · Gert-Jan Bottu, Ningning Xie, Koar Marntirosian, Tom Schrijvers
10. Compiling with continuations, or without? whatever · Youyou Cong, Leo Osvald, Grégory M. Essertel, Tiark Rompf
11. Cubical agda: a dependently typed programming language with univalence and higher inductive types · Andrea Vezzosi, Anders Mörtberg, Andreas Abel
12. Demystifying differentiable programming: shift/reset the penultimate backpropagator · Fei Wang, Daniel Zheng, James M. Decker, Xilun Wu, Grégory M. Essertel, Tiark Rompf
13. Dependently typed Haskell in industry (experience report) · David Thrane Christiansen, Iavor S. Diatchki, Robert Dockins, Joe Hendrix, Tristan Ravitch
14. Dijkstra monads for all · Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas + 1 more
15. Efficient differentiable programming in a functional array-processing language · Amir Shaikhha, Andrew W. Fitzgibbon, Dimitrios Vytiniotis, Simon Peyton Jones
16. Equations reloaded: high-level dependently-typed functional programming and proving in Coq · Matthieu Sozeau, Cyprien Mangin
17. Fairness in responsive parallelism · Stefan K. Muller, Sam Westrick, Umut A. Acar
18. From high-level inference algorithms to efficient code · Rajan Walia, Praveen Narayanan, Jacques Carette, Sam Tobin-Hochstadt, Chung-chieh Shan
19. Fuzzi: a three-level logic for differential privacy · Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, Aaron Roth
20. Higher-order type-level programming in Haskell · Csongor Kiss, Tony Field, Susan Eisenbach, Simon Peyton Jones
21. Implementing a modal dependent type theory · Daniel Gratzer, Jonathan Sterling, Lars Birkedal
22. Lambda calculus with algebraic simplification for reduction parallelization by equational reasoning · Akimasa Morihata
23. Lambda: the ultimate sublanguage (experience report) · Jeremy Yallop, Leo White
24. Linear capabilities for fully abstract compilation of separation-logic-verified code · Thomas Van Strydonck, Frank Piessens, Dominique Devriese
25. Mechanized relational verification of concurrent programs with continuations · Amin Timany, Lars Birkedal
26. Mixed linear and non-linear recursive types · Bert Lindenhovius, Michael W. Mislove, Vladimir Zamdzhiev
27. Narcissus: correct-by-construction derivation of decoders and encoders from binary formats · Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala
28. Quantitative program reasoning with graded modal types · Dominic Orchard, Vilem-Benjamin Liepelt, Harley Eades III
29. Rebuilding racket on chez scheme (experience report) · Matthew Flatt, Caner Derici, R. Kent Dybvig, Andrew W. Keep, Gustavo E. Massaccesi, Sarah Spall + 2 more
30. Relational cost analysis for functional-imperative programs · Weihao Qu, Marco Gaboardi, Deepak Garg
31. Selective applicative functors · Andrey Mokhov, Georgy Lukyanov, Simon Marlow, Jerémie Dimino
32. Sequential programming for replicated data stores · Nicholas V. Lewchenko, Arjun Radhakrishna, Akash Gaonkar, Pavol Cerný
33. Simple noninterference from parametricity · Maximilian Algehed, Jean-Philippe Bernardy
34. Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks · Patrick Bahr, Christian Graulund, Rasmus Ejlers Møgelberg
35. Sound and robust solid modeling via exact real arithmetic and continuity · Benjamin Sherman, Jesse Michel, Michael Carbin
36. Synthesizing differentially private programs · Calvin Smith, Aws Albarghouthi
37. Synthesizing symmetric lenses · Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
38. Teaching the art of functional programming using automated grading (experience report) · Aliya Hameer, Brigitte Pientka
39. The next 700 compiler correctness theorems (functional pearl) · Daniel Patterson, Amal Ahmed