Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 18 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:20
Interaction and ApplicationsTyDe at Aurora Borealis
Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford
09:00
20m
Talk
Flexible Structure Editing of Well-Typed Expressions
TyDe
David Moon , Cyrus Omar University of Chicago, R. Benjamin Shapiro University of Colorado, Boulder
Pre-print
09:20
20m
Talk
Livelits: Filling Typed Holes with Live GUIs
TyDe
Cyrus Omar University of Chicago, Nick Collins University of Chicago, David Moon , Ian Voysey Carnegie Mellon University, Ravi Chugh University of Chicago
Pre-print
09:40
20m
Talk
Formal Investigation of the Extended UTxO Model
TyDe
Orestis Melkonian Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag I/O & IOHK
Pre-print
10:00
20m
Talk
An Algebra of Sequential Decision Problems
TyDe
Robert Krook Chalmers University of Technology, Patrik Jansson Chalmers University of Technology
Pre-print
09:00 - 10:20
Morning KeynoteScheme at Birch
09:00
60m
Talk
Morning Keynote
Scheme
Edwin Brady University of St. Andrews, UK
09:00 - 10:20
AccelerateFHPNC at Reindeer
Chair(s): Dominic Steinitz Tweag I/O
09:00
60m
Talk
Keynote
FHPNC
Trevor L. McDonell Utrecht University
10:00
10m
Talk
GSoC Student Report 1
FHPNC
10:10
10m
Talk
GSoC Student Report 2
FHPNC
Jesse Sigal University of Edinburgh
09:00 - 10:20
09:00
10m
Day opening
Welcome
PLMW @ ICFP
David Van Horn University of Maryland, USA
09:10
35m
Talk
Effect handler oriented programming
PLMW @ ICFP
Sam Lindley The University of Edinburgh and Imperial College London
09:45
35m
Talk
Types and verification
PLMW @ ICFP
Niki Vazou IMDEA Software Institute
09:00 - 10:20
Session 1Erlang at Yew
09:00
20m
Day opening
Opening
Erlang
Viktória Fördős Cisco Systems, Adrian Francalanza University of Malta
09:20
60m
Talk
Introduction to the Erlang Ecosystem Foundation
Erlang
Peer Stritzinger Peer Stritzinger GmbH
10:50 - 12:10
Dependently Typed ProgrammingTyDe at Aurora Borealis
Chair(s): William J. Bowman University of British Columbia
10:50
20m
Talk
Syntax with Shifted Names
TyDe
Stephen Dolan , Leo White Jane Street
Pre-print
11:10
20m
Talk
Tic Tac Types (Functional Pearl)
TyDe
Sean Innes University of Bristol, Nicolas Wu Imperial College London
Link to publication
11:30
20m
Talk
Monadic typed tactic programming by reflection
TyDe
Liang-Ting Chen Swansea University
Pre-print
11:50
20m
Talk
Deferring the Details and Deriving Programs
TyDe
Link to publication
10:50 - 12:10
Research Session 1Scheme at Birch
10:30
30m
Talk
Syntax Templates In Racket
Scheme
Ryan Culpepper Czech Technical University
11:00
30m
Talk
Visualizing Abstract Abstract Machines
Scheme
Kyle Headley The University of Alabama at Birmingham
11:30
30m
Talk
gLua: A modern Lua transpiler in Scheme
Scheme
10:50 - 12:10
Orthogonal BasesFHPNC at Reindeer
Chair(s): Gabriele Keller Utrecht University
10:50
26m
Talk
Generating Efficient FFT GPU Code with Lift
FHPNC
Bastian Köpcke University of Münster, Michel Steuwer University of Glasgow, Sergei Gorlatch
Link to publication DOI Pre-print File Attached
11:16
26m
Talk
Lazy Evaluation in Infinite-Dimensional Function Spaces with Wavelet Basis
FHPNC
Olivier Verdier , Justus Sagemüller Western Norway University of Applied Sciences
Link to publication Pre-print
11:43
26m
Talk
Functional Approach to Acceleration of Monte Carlo Simulation for American Option Pricing (extended abstract)
FHPNC
Wojciech Michal Pawlak University of Copenhagen, Denmark, Martin Elsman University of Copenhagen, Denmark, Cosmin Oancea University of Copenhagen, Denmark
Link to publication
10:50 - 12:10
10:50
40m
Talk
Managing your research, your advisor, your PhD
PLMW @ ICFP
Amal Ahmed Northeastern University, USA
11:30
40m
Talk
Time management, family, and quality of life
PLMW @ ICFP
Kathleen Fisher Tufts University, USA
10:50 - 12:10
Session 2Erlang at Yew
10:50
40m
Full-paper
Gaining Trust by Tracing Security Protocols
Erlang
Lars-Ake Fredlund , Thomas Arts Quviq, Clara Benac Earle Universidad Politécnica de Madrid, Hans Svensson Quviq AB
11:30
40m
Full-paper
Runtime Type Safety for Erlang/OTP Behaviours
Erlang
Joseph Harrison University of Kent, UK
12:00 - 13:30
12:00
90m
Lunch
Lunch
Catering

13:40 - 14:50
Invited Talk and MetatheoryTyDe at Aurora Borealis
Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford
13:40
50m
Talk
Cubes, Cats, Effects
TyDe
14:30
20m
Talk
Inductive types deconstructed
TyDe
Stefan Monnier Université de Montréal
Link to publication
13:40 - 14:50
Research Session 2Scheme at Birch
14:00
20m
Talk
Lightning talk: Commanding Emacs from Coq
Scheme
Joomy Korkut Princeton University, USA
14:20
20m
Talk
Reigniting Fuse, an Online Partial Evaluator for Scheme
Scheme
Paulette Koronkevich University of British Columbia
14:40
20m
Talk
SRFI-167, SRFI-168 and the functional store
Scheme
13:40 - 14:50
Machine LearningFHPNC at Reindeer
Chair(s): Dominic Steinitz Tweag I/O
13:40
23m
Talk
Compositional Deep Learning in Futhark
FHPNC
Duc Minh Tran DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Denmark, Martin Elsman University of Copenhagen, Denmark
Link to publication
14:03
23m
Talk
Towards Hasktorch 1.0: Automated Generation of C++ Libtorch Bindings (extended abstract)
FHPNC
Junji Hashimoto GREE, Inc., Autsin Huang , Sam Stites Sentenai
14:26
23m
Talk
Hailstorm : A statically typed functional language for systems programming (extended abstract)
FHPNC
Abhiroop Sarkar Chalmers University of Technology, Mary Sheeran
13:40 - 14:50
13:40
35m
Talk
Functional Programming is Everywhere
PLMW @ ICFP
Ilya Sergey Yale-NUS College and National University of Singapore
14:15
35m
Talk
How to give talks that people can follow
PLMW @ ICFP
Derek Dreyer MPI-SWS
13:40 - 14:50
Session 3Erlang at Yew
13:40
23m
Short-paper
Lux - an expect like test tool written in Erlang
Erlang
Håkan Mattsson , Cons T Åhs Cisco Sweden AB
14:03
23m
Short-paper
Towards Online Profiling of Erlang Systems
Erlang
Michal Slaski Erlang Solutions Ltd., Wojciech Turek AGH University of Science and Technology
14:26
24m
Short-paper
Tools supporting green computing in Erlang
Erlang
Gergely Nagy Eötvös Lóránd University, Áron Attila Mészáros Eötvös Lóránd University, István Bozó Eötvös Loránd University, Melinda Tóth Eötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd.
15:20 - 16:40
Generic Programming and SynthesisTyDe at Aurora Borealis
Chair(s): Edwin Brady University of St. Andrews, UK
15:20
20m
Talk
Generic Enumerators
TyDe
Cas van der Rest Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag I/O & IOHK
Pre-print
15:40
20m
Talk
Generic Level Polymorphic N-ary Functions
TyDe
Guillaume Allais University of Strathclyde
Link to publication
16:00
20m
Talk
Augmenting Type Signatures for Program Synthesis
TyDe
Bruce Collie University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh
Pre-print
16:20
20m
Talk
Constraint-based Type-directed Program Synthesis
TyDe
Peter-Michael Osera Grinnell College
Link to publication
15:20 - 16:40
Research Session 3Scheme at Birch
15:30
30m
Talk
Scheme Macros for Non-linear Pattern Matching with Backtracking for Non-free Data Types
Scheme
Satoshi Egi Rakuten Institute of Technology
16:00
30m
Talk
Stack-Liberated Abstract Garbage Collection
Scheme
Kimball Germane University of Utah, Michael D. Adams University of Michigan
15:20 - 16:40
ArraysFHPNC at Reindeer
Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital
15:20
25m
Talk
Compiling Generalised Histograms for GPU (extended abstract)
FHPNC
Sune Hellfritzsch University of Copenhagen, Niels G. W. Serup DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Denmark, Cosmin Oancea University of Copenhagen, Denmark
15:46
26m
Talk
Position-Dependent Arrays and Their Applicationfor High Performance Code Generation
FHPNC
Federico Pizzuti University of Edinburgh, Michel Steuwer University of Glasgow, Christophe Dubach University of Edinburgh
Link to publication DOI Pre-print File Attached
16:14
26m
Talk
Safety at speed: In-place array algorithms from pure functional programs by safely re-using storage
FHPNC
Markus Aronsson , Koen Claessen Chalmers University of Technology, Mary Sheeran , Nicholas Smallbone Chalmers University of Technology, Sweden
15:20 - 16:40
15:20
80m
Talk
Social activity
PLMW @ ICFP
Niki Vazou IMDEA Software Institute, Joachim Breitner DFINITY Foundation
15:20 - 16:40
Session 4Erlang at Yew
15:20
40m
Full-paper
Erlang as an enabling technology for resilient general-purpose applications on edge IoT networks
Erlang
Igor Kopestenski Université Catholique de Louvain, Peter Van Roy Université catholique de Louvain
16:00
40m
Full-paper
Intro to Web Prolog for Erlangers
Erlang
Torbjörn Lager Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg
17:10 - 18:10
EffectsTyDe at Aurora Borealis
Chair(s): David Darais University of Vermont
17:10
20m
Talk
Reasoning about Effect Parametricity Using Dependent Types
TyDe
Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel
Pre-print
17:30
20m
Talk
How to do proofs? Practically proving properties about effectful programs' results (functional pearl)
TyDe
Koen Jacobs KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel
Link to publication
17:10 - 18:10
Afternoon KeynoteScheme at Birch
17:10
60m
Talk
Afternoon Keynote
Scheme
Andy Keep Cisco Systems, Inc
17:10 - 18:10
VerificationFHPNC at Reindeer
Chair(s): Gabriele Keller Utrecht University
17:10
60m
Talk
Formal Verification of Scientific Computing Programs
FHPNC
Micaela Mayero LIPN, Université Paris 13
17:10 - 18:10
17:10
60m
Talk
Panel Discussion: Research in Functional Programming
PLMW @ ICFP
Simon Peyton Jones Microsoft, UK, Satnam Singh Google Research, Zoe Paraskevopoulou Princeton University, Jeremy Gibbons Department of Computer Science, University of Oxford, Andrey Mokhov Newcastle University, UK, Amal Ahmed Northeastern University, USA
17:10 - 18:10
Session 5Erlang at Yew
17:10
40m
Full-paper
Scaling Erlang Distribution
Erlang
Adam Lindberg Peer Stritzinger GmbH, Sébastien Merle Peer Stritzinger GmbH, Peer Stritzinger Peer Stritzinger GmbH
17:50
20m
Day closing
Closing
Erlang
Viktória Fördős Cisco Systems, Adrian Francalanza University of Malta
18:10 - 19:10
Happy HourCatering at Restaurant
18:10
60m
Social Event
Happy Hour
Catering

Mon 19 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Monday KeynoteKeynotes and Reports at Aurora Borealis
Chair(s): Derek Dreyer MPI-SWS
09:00
60m
Talk
Blockchains are functional
Keynotes and Reports
Manuel Chakravarty Tweag I/O & IOHK
10:30 - 12:00
Compilation & ParallelismResearch Papers at Aurora Borealis
Chair(s): Michael D. Adams University of Michigan
10:30
22m
Talk
Rebuilding Racket on Chez Scheme (Experience Report)
Research Papers
Matthew Flatt University of Utah, Caner Derici Indiana University, R. Kent Dybvig Cisco Systems, Inc, Andy Keep Cisco Systems, Inc, Gustavo E. Massaccesi Universidad de Buenos Aires, Sarah Spall Indiana University, Sam Tobin-Hochstadt Indiana University, Jon Zeppieri
Link to publication DOI
10:52
22m
Talk
Compiling with Continuations, or without? Whatever.
Research Papers
Youyou Cong Tokyo Institute of Technology, Leo Osvald Purdue University, USA, Gregory Essertel Purdue University, Tiark Rompf Purdue University
11:15
22m
Talk
Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning
Research Papers
Akimasa Morihata University of Tokyo
11:37
22m
Talk
Fairness in Responsive Parallelism
Research Papers
Stefan K. Muller Carnegie Mellon University, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
12:00 - 13:30
13:30 - 15:00
Verified CompilationResearch Papers at Aurora Borealis
Chair(s): Ralf Jung MPI-SWS
13:30
22m
Talk
Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats
Research Papers
Benjamin Delaware Purdue University, Sorawit Suriyakarn , Clément Pit-Claudel MIT CSAIL, Qianchuan Ye Purdue University, Adam Chlipala Massachusetts Institute of Technology
Link to publication DOI Authorizer link
13:52
22m
Talk
Closure Conversion is Safe for Space
Research Papers
Zoe Paraskevopoulou Princeton University, Andrew W. Appel Princeton
14:15
22m
Talk
Linear capabilities for fully abstract compilation of separation-logic-verified code
Research Papers
Thomas Van Strydonck KULeuven, Frank Piessens KU Leuven, Dominique Devriese Vrije Universiteit Brussel
14:37
22m
Talk
The Next 700 Compiler Correctness Theorems. A Functional Pearl.
Research Papers
Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA
15:20 - 16:30
Type TheoryResearch Papers at Aurora Borealis
Chair(s): Jennifer Paykin Galois, Inc.
15:20
23m
Talk
Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq
Research Papers
15:43
23m
Talk
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive TypesDistinguished Paper
Research Papers
Andrea Vezzosi Chalmers University of Technology, Anders Mörtberg Department of Mathematics, Stockholm University, Andreas Abel Gothenburg University
16:06
23m
Talk
Approximate Normalization for Gradual Dependent Types
Research Papers
Joseph Eremondi University of British Columbia, Éric Tanter University of Chile & Inria Paris, Ronald Garcia University of British Columbia
Pre-print
16:50 - 18:00
TypesResearch Papers at Aurora Borealis
Chair(s): Richard A. Eisenberg Bryn Mawr College, USA
16:50
23m
Talk
Simple Noninterference from Parametricity
Research Papers
Maximilian Algehed Chalmers University of Technology, Sweden, Jean-Philippe Bernardy University of Gothenburg
17:13
23m
Talk
Selective Applicative Functors
Research Papers
Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Simon Marlow Facebook, Jeremie Dimino Jane Street Europe
Link to publication
17:36
23m
Talk
Coherence of Type Class Resolution
Research Papers
Gert-Jan Bottu KU Leuven, Ningning Xie University of Toronto, Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven
18:00 - 20:00
18:00
2h
Poster
SRC Poster Session
Student Research Competition

Tue 20 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Tuesday KeynoteKeynotes and Reports at Aurora Borealis
Chair(s): François Pottier Inria, France
09:00
60m
Talk
Solver-Aided Programming for All
Keynotes and Reports
Emina Torlak University of Washington
10:30 - 12:00
Program Analysis & SynthesisResearch Papers at Aurora Borealis
Chair(s): Daniel Winograd-Cort Target Corp
10:30
22m
Talk
Relational Cost Analysis for Functional-Imperative Programs
Research Papers
Weihao Qu University at Buffalo, SUNY, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems
10:52
22m
Talk
Fuzzi: A Three-Level Logic for Differential Privacy
Research Papers
Hengchu Zhang University of Pennsylvania, Edo Roth University of Pennsylvania, Andreas Haeberlen University of Pennsylvania, USA, Benjamin C. Pierce University of Pennsylvania, Aaron Roth University of Pennsylvania, USA
11:15
22m
Talk
Synthesizing Differentially Private Programs
Research Papers
Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison
11:37
22m
Talk
Synthesizing Symmetric Lenses
Research Papers
Anders Miltner Princeton University, Solomon Maina University of Pennsylvania, Kathleen Fisher Tufts University, USA, Benjamin C. Pierce University of Pennsylvania, David Walker Princeton University, Steve Zdancewic University of Pennsylvania
Pre-print
12:00 - 13:30
13:30 - 15:00
The Real WorldResearch Papers at Aurora Borealis
Chair(s): Robert Atkey University of Strathclyde
13:30
22m
Talk
Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
Research Papers
Fei Wang , Dan Zheng Purdue University, Google Brain, James Decker , Xilun Wu Purdue University, Gregory Essertel Purdue University, Tiark Rompf Purdue University
Pre-print
13:52
22m
Talk
Efficient Differentiable Programming in a Functional Array-Processing Language
Research Papers
Amir Shaikhha University of Oxford, Andrew Fitzgibbon Microsoft Research, Cambridge, Dimitrios Vytiniotis DeepMind, Simon Peyton Jones Microsoft, UK
14:15
22m
Talk
From high-level inference algorithms to efficient code
Research Papers
Rajan Walia Indiana University, Praveen Narayanan Indiana University, USA, Jacques Carette McMaster University, Sam Tobin-Hochstadt Indiana University, Chung-chieh Shan Indiana University, USA
Pre-print
14:37
22m
Talk
Sound and robust solid modeling via exact real arithmetic and continuityDistinguished Paper
Research Papers
Benjamin Sherman Massachusetts Institute of Technology, USA, Jesse Michel Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
DOI Pre-print Media Attached
15:20 - 16:30
Dependent Types in HaskellResearch Papers at Aurora Borealis
Chair(s): Joachim Breitner DFINITY Foundation
15:20
23m
Talk
Dependently Typed Haskell in Industry (Experience Report)
Research Papers
David Thrane Christiansen Galois, USA, Iavor Diatchki Galois, Inc., Robert Dockins Galois, Inc., Joe Hendrix Galois, Inc., Tristan Ravitch Galois, Inc.
15:43
23m
Talk
A Role for Dependent Types in Haskell
Research Papers
Stephanie Weirich University of Pennsylvania, USA, Pritam Choudhury University of Pennsylvania, Antoine Voizard University of Pennsylvannia, Richard A. Eisenberg Bryn Mawr College, USA
16:06
23m
Talk
Higher-order Type-level Programming in Haskell
Research Papers
Csongor Kiss Imperial College London, Tony Field Imperial College London, Susan Eisenbach Imperial College London, Simon Peyton Jones Microsoft, UK
16:50 - 18:15
16:50
40m
Talk
SRC Finalist Presentation
Student Research Competition

17:30
15m
Awards
SIGPLAN Awards
Keynotes and Reports

17:45
30m
Awards
Programming Contest Report
Keynotes and Reports
Ilya Sergey Yale-NUS College and National University of Singapore
18:15 - 19:15
Happy HourCatering at Restaurant

Wed 21 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Wednesday KeynoteKeynotes and Reports at Aurora Borealis
Chair(s): François Pottier Inria, France
09:00
60m
Talk
Derivations as computations
Keynotes and Reports
Andrej Bauer University of Ljubljana
10:30 - 12:00
Program VerificationResearch Papers at Aurora Borealis
Chair(s): Adam Chlipala Massachusetts Institute of Technology
10:30
22m
Talk
A predicate transformer semantics for effects (Functional Pearl)
Research Papers
Wouter Swierstra Utrecht University, Netherlands, Tim Baanen Utrecht University
10:52
22m
Talk
Dijkstra Monads for All
Research Papers
Kenji Maillard Inria Paris and ENS Paris, Danel Ahman University of Ljubljana, Robert Atkey University of Strathclyde, Guido Martínez CIFASIS-CONICET, Argentina, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Éric Tanter University of Chile & Inria Paris
Pre-print
11:15
22m
Talk
Mechanized Relational Verification of Concurrent Programs with Continuations
Research Papers
Amin Timany imec-Distrinet KU-Leuven, Lars Birkedal Aarhus University
11:37
22m
Talk
Sequential Programming for Replicated Data Stores
Research Papers
Nicholas V. Lewchenko University of Colorado Boulder, Arjun Radhakrishna Microsoft, Akash Gaonkar , Pavol Cerny University of Colorado Boulder
DOI Pre-print
12:00 - 13:30
13:30 - 15:00
Modal TypesResearch Papers at Aurora Borealis
Chair(s): Dominique Devriese Vrije Universiteit Brussel
13:30
22m
Talk
Implementing a Modal Dependent Type TheoryDistinguished Paper
Research Papers
Daniel Gratzer Aarhus University, Jonathan Sterling Carnegie Mellon University, Lars Birkedal Aarhus University
13:52
22m
Talk
A Reasonably Exceptional Type Theory
Research Papers
Pierre-Marie Pédrot INRIA, Nicolas Tabareau Inria, Hans Fehrmann University of Chile, Éric Tanter University of Chile & Inria Paris
14:15
22m
Talk
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks
Research Papers
Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
14:37
22m
Talk
Quantitative program reasoning with graded modal types
Research Papers
Dominic Orchard University of Kent, UK, Vilem-Benjamin Liepelt University of Kent, UK, Harley D. Eades III Augusta University
Pre-print
15:20 - 16:30
TypesResearch Papers at Aurora Borealis
Chair(s): Zoe Paraskevopoulou Princeton University
15:20
23m
Talk
Mixed Linear and Non-linear Recursive Types
Research Papers
Bert Lindenhovius Tulane University, Michael Mislove Tulane, Vladimir Zamdzhiev Inria Nancy
15:43
23m
Talk
A Mechanical Formalization of Higher-Ranked Polymorphic Type InferenceDistinguished Paper
Research Papers
Zhao Jinxu , Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven
16:06
23m
Talk
An Efficient Algorithm for Type-Safe Structural Diffing
Research Papers
Victor Cacciari Miraldo Utrecht University, Netherlands, Wouter Swierstra Utrecht University, Netherlands
16:50 - 18:00
Lambda-Calculus & TeachingResearch Papers at Aurora Borealis
Chair(s): Jonathan Protzenko Microsoft Research, Redmond
16:50
23m
Talk
Call-By-Need is Clairvoyant Call-By-Value
Research Papers
Jennifer Hackett University of Nottingham, UK, Graham Hutton University of Nottingham, UK
17:13
23m
Talk
Teaching the Art of Functional Programming Using Automated Grading (Experience Report)
Research Papers
Aliya Hameer McGill University, Brigitte Pientka McGill University
17:36
23m
Talk
Lambda: the Ultimate Sublanguage (Experience Report)
Research Papers
Jeremy Yallop University of Cambridge, UK, Leo White Jane Street
DOI Pre-print
18:00 - 18:30
18:00
10m
Awards
SRC Awards Presentation
Student Research Competition

18:10
15m
Talk
Program Chair's Report
Keynotes and Reports
François Pottier Inria, France
18:25
5m
Talk
ICFP 2020 Announcement
Keynotes and Reports

18:30 - 19:30
Happy HourCatering at Restaurant

Thu 22 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 12:00
Tutorials B1Tutorials at Birch
09:00
3h
Tutorial
Fine-grained program reasoning using linear and graded modal types
Tutorials
Harley D. Eades III Augusta University, Dominic Orchard University of Kent, UK, Vilem-Benjamin Liepelt University of Kent, UK
09:00 - 10:00
Session 1miniKanren at Elk
09:00
60m
Tutorial
Tutorial on miniKanren
miniKanren
William E. Byrd University of Alabama at Birmingham, USA
09:00 - 10:00
Session 1ML at Pine
Chair(s): KC Sivaramakrishnan IIT Madras
09:00
60m
Talk
Keynote: An Introduction to the Imandra Automated Reasoning System
ML
I: Grant Passmore Imandra Inc.
09:00 - 12:00
Tutorials R1Tutorials at Reindeer
09:00
3h
Tutorial
Verifying Imperative Programs with SAW
Tutorials
David Thrane Christiansen Galois, USA, Iavor Diatchki Galois, Inc.
09:00 - 12:00
Tutorials Y1Tutorials at Yew
09:00
3h
Tutorial
Functional Software Architecture
Tutorials
Michael Sperber Active Group GmbH
10:30 - 12:00
Paper Session 1: Classes & InstancesHaskell at Aurora Borealis
Chair(s): Jose Calderon Galois, Inc.
10:30
30m
Research paper
Bidirectional Type Class Instances
Haskell
Koen Pauwels KU Leuven, Georgios Karachalias KU Leuven, Belgium, Michiel Derhaeg Guardsquare, Tom Schrijvers KU Leuven
11:00
30m
Research paper
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances
Haskell
Ryan Scott Indiana University at Bloomington, USA, Ryan R. Newton Indiana University
Pre-print File Attached
11:30
30m
Research paper
Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the μVeriFast verifier as a case study
Haskell
Dominique Devriese Vrije Universiteit Brussel
File Attached
10:30 - 12:00
Session 2miniKanren at Elk
Chair(s): Lisa Zhang University of Toronto
10:30
45m
Full-paper
Relational Interpreters for Search Problems
miniKanren
Petr Lozov Sain Petersburg State University, SPbGU, Ekaterina Verbitskaia Saint Petersburg State University, Russia, Dmitri Boulytchev
Link to publication
11:15
45m
Full-paper
Relational Processing for Fun and Diversity: Simulating a CPU relationally with miniKanren
miniKanren
Gilmore R. Lundquist , Utsav Bhatt , Kevin Hamlen University of Texas at Dallas, USA
Link to publication
10:30 - 12:00
Session 2ML at Pine
Chair(s): Andreas Rossberg Dfinity Stiftung
10:30
25m
Talk
A right-to-left type system for value recursion
ML
Alban Reynaud ENS Lyon, Gabriel Scherer INRIA Saclay, Jeremy Yallop University of Cambridge, UK
Pre-print
10:55
25m
Talk
let (rec) insertion without effects, lights or magic
ML
Oleg Kiselyov , Jeremy Yallop University of Cambridge, UK
Pre-print
11:20
25m
Talk
(TyDe Presentation) FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
ML
Frank Emrich The University of Edinburgh, Sam Lindley The University of Edinburgh and Imperial College London, Jan Stolarek University of Edinburgh, UK, James Cheney University of Edinburgh, UK
11:20 - 11:45
Presented at ML WorkshopTyDe at Pine
11:20
25m
Talk
FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
TyDe
Frank Emrich The University of Edinburgh, Sam Lindley The University of Edinburgh and Imperial College London, Jan Stolarek University of Edinburgh, UK, James Cheney University of Edinburgh, UK
Pre-print
12:00 - 13:30
13:30 - 15:00
Paper Session 2: VerificationHaskell at Aurora Borealis
Chair(s): Ningning Xie University of Toronto
13:30
30m
Research paper
Verifying Effectful Haskell Programs in Coq
Haskell
Jan Christiansen Flensburg University of Applied Sciences, Germany, Sandra Dylus University of Kiel, Germany, Niels Bunkenburg University of Kiel, Germany
14:00
30m
Talk
Solving Haskell equality constraints using Coq
Haskell
File Attached
14:30
30m
Experience report
Formal Verification of Spacecraft Control Programs: An Experience Report
Haskell
Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Jakob Lechner RUAG Space Austria GmbH
13:30 - 15:00
Session 3ML at Pine
Chair(s): Zoe Paraskevopoulou Princeton University
13:30
25m
Talk
Transparent Synchronous Dataflow
ML
Steven Cheung University of Birmingham, UK
File Attached
13:55
25m
Talk
Programming with Rational Coinductive Streams
ML
Jean-Baptiste Jeannin University of Michigan, USA
File Attached
14:20
25m
Talk
Efficient Deconstruction with Typed Pointer Reversal
ML
Pre-print
13:30 - 16:30
Tutorials R2Tutorials at Reindeer
13:30
3h
Tutorial
Verifying Imperative Programs with SAW
Tutorials
David Thrane Christiansen Galois, USA, Iavor Diatchki Galois, Inc.
13:30 - 16:30
Tutorials Y2Tutorials at Yew
13:30
3h
Tutorial
Teaching functional programming
Tutorials
Michael Sperber Active Group GmbH
15:20 - 16:30
Paper Session 3: SMT & ArityHaskell at Aurora Borealis
Chair(s): Eric Seidel Bloomberg LP
15:20
30m
Research paper
G2Q: Haskell Constraint Solving
Haskell
William T. Hallahan Yale University, Anton Xue Yale University, Ruzica Piskac Yale University, USA
15:50
30m
Talk
Making a Faster Curry with Extensional Types
Haskell
Paul Downen University of Oregon, USA, Zachary Sullivan , Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK
15:20 - 16:30
Session 4miniKanren at Elk
Chair(s): Dmitri Boulytchev
15:20
35m
Full-paper
First-order miniKanren representation: Great for tooling and search
miniKanren
Gregory Rosenblatt , Lisa Zhang University of Toronto, William E. Byrd University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School
Link to publication
15:55
35m
Full-paper
Towards a miniKanren with fair search strategies
miniKanren
Kuang-Chen Lu Indiana University, USA, Weixi Ma , Daniel P. Friedman Indiana University, USA
Link to publication
15:20 - 16:30
Session 4ML at Pine
Chair(s): Gabriel Scherer INRIA Saclay
15:20
25m
Talk
An Idris Foreign Function Interface to OCaml
ML
Robert Atkey University of Strathclyde, Ioan Luca University of Strathclyde
File Attached
15:45
25m
Talk
Necro: Animating Skeletons
ML
Nathanaël Courant INRIA, Enzo Crance INSA Rennes, Alan Schmitt Inria
File Attached
16:50 - 18:15
Paper Session 4: MetaprogrammingHaskell at Aurora Borealis
Chair(s): Christiaan Baaij QBayLogic B.V.
16:50
30m
Research paper
Multi-Stage Programs in Context
Haskell
Matthew Pickering University of Bristol, Nicolas Wu Imperial College London, Csongor Kiss Imperial College London
17:20
30m
Research paper
Working with Source Plugins
Haskell
Matthew Pickering University of Bristol, Nicolas Wu Imperial College London, Boldizsár Németh Eötvös Loránd University
17:50
10m
Other
PC Chair Report
Haskell
Richard A. Eisenberg Bryn Mawr College, USA
16:50 - 18:15
Session 5miniKanren at Elk
16:50
85m
Social Event
Q&A with audience
miniKanren

16:50 - 18:15
Session 5ML at Pine
Chair(s): Edwin Brady University of St. Andrews, UK
16:50
25m
Talk
Compiling Successor ML Pattern Guards
ML
John Reppy University of Chicago, Mona Zahir University of Chicago
Pre-print
17:15
25m
Talk
A Key-Value store for OCaml
ML
Tom Ridge University of Leicester, UK
File Attached
17:40
25m
Talk
Towards Machine Learning Induction in Poly/ML
ML
Yutaka Nagashima Data61, Australia
File Attached
18:15 - 20:15
Industrial ReceptionCatering at Restaurant
18:15
2h
Social Event
Industrial Reception
Catering

Fri 23 Aug

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
KeynoteHaskell at Aurora Borealis
Chair(s): Niki Vazou IMDEA Software Institute
09:00
60m
Talk
Haskell Use and Abuse at Scale
Haskell
09:00 - 12:00
Tutorials B3Tutorials at Birch
09:00
3h
Tutorial
Folding/Unfolding with Scala
Tutorials
09:00 - 10:00
KeynoteHIW at Elk
09:00
60m
Talk
Haskell Use and Abuse at Scale
HIW
09:00 - 10:00
EcosystemOCaml at Pine
Chair(s): David Allsopp University of Cambridge
09:00
5m
Day opening
Welcome
OCaml
David Allsopp University of Cambridge
09:05
25m
Talk
Invited Talk
OCaml
Xavier Leroy Collège de France
09:30
30m
Talk
The OCaml Platform in 2019
OCaml
Anil Madhavapeddy OCaml Labs, Gemma Gordon University of Cambridge
09:00 - 12:00
Tutorials R3Tutorials at Reindeer
09:00
3h
Tutorial
Programming Language Foundations in Agda
Tutorials
Philip Wadler University of Edinburgh, UK
09:00 - 10:00
SoundFARM at Stockholm
Chair(s): Youyou Cong Tokyo Institute of Technology
09:10
30m
Talk
Csound-expression: Haskell framework for computer music
FARM
09:40
30m
Talk
Screaming in the IO monad
FARM
David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University
09:00 - 12:00
Tutorials Y3Tutorials at Yew
09:00
3h
Tutorial
Building C++ project with Shake
Tutorials
10:30 - 12:00
Paper Session 5: FRPHaskell at Aurora Borealis
Chair(s): Christine Rizkallah UNSW Sydney
10:30
30m
Research paper
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism
Haskell
Sebastian Ertel , Justus Adam Technische Universität Dresden, Norman A. Rink TU Dresden, Germany, Andrés Goens , Jeronimo Castrillon TU Dresden, Germany
11:00
30m
Research paper
Synthesizing Functional Reactive Programs
Haskell
Bernd Finkbeiner , Felix Klein Saarland University, Ruzica Piskac Yale University, USA, Mark Santolucito Yale University, USA
11:30
30m
Talk
The essence of live coding: Change the program, keep the state!
Haskell
Manuel Bärenz sonnen eServices GmbH
File Attached
10:30 - 12:00
MetadataHIW at Elk
Chair(s): Ningning Xie University of Toronto
10:30
23m
Talk
Configuration, but without CPP
HIW
Matthew Pickering University of Bristol, John Ericson Obsidian Systems
10:53
23m
Talk
HIE files in GHC 8.8
HIW
Zubin Duggal , Matthew Pickering University of Bristol
11:16
24m
Talk
Tagging Tags: Inferring the presence of pointer tags at compile time.
HIW
11:40
20m
Talk
Lightning talks Slot #1
HIW

10:30 - 12:00
ApplicationsOCaml at Pine
Chair(s): Igor Pikovets
10:30
25m
Talk
OwlDE: making ODEs first-class Owl citizens
OCaml
Marcello Seri Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen, Ta-Chu Kao Computational and Biological Learning Lab, Department of Engineering, University of Cambridge
10:55
25m
Talk
CausalRPC: traceable distributed computation
OCaml
11:20
25m
Talk
Executing Owl Computation on GPU and TPU
OCaml
Jianxin Zhao University of Cambridge
10:30 - 12:00
Music GenerationFARM at Stockholm
Chair(s): David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University
10:30
30m
Talk
Music as Language: Putting Probabilistic Temporal Graph Grammars to Good Use
FARM
Orestis Melkonian Utrecht University
11:00
30m
Talk
A Functional Model of Jazz Improvisation
FARM
Donya Quick Stevens Institute of Technology, Kelland Thomas Stevens Institute of Technology
11:30
30m
Talk
Demo: Counterpoint by Construction
FARM
Youyou Cong Tokyo Institute of Technology, John Leo Halfaya Research
12:00 - 13:30
13:30 - 15:00
Paper Session 6: EffectsHaskell at Aurora Borealis
Chair(s): Ki Yung Ahn Hannam University
13:30
30m
Research paper
Monad Transformers and Modular Algebraic Effects: What Binds Them Together
Haskell
Tom Schrijvers KU Leuven, Maciej Piróg University of Wrocław, Nicolas Wu Imperial College London, Mauro Jaskelioff CONICET, Argentina
14:00
30m
Research paper
Scoping Monadic Relational Database Queries
Haskell
Anton Ekblad Chalmers University of Technology
13:30 - 15:00
CompilersHIW at Elk
Chair(s): Jose Calderon Galois, Inc.
13:30
23m
Talk
Status Update on the Helium for Haskell compiler
HIW
Jurriaan Hage Utrecht University, Netherlands
13:53
23m
Talk
The Gibbon Compiler: Accelerating a small subset of Haskell
HIW
Ryan R. Newton Indiana University, Michael Vollmer Indiana University, USA, Chaitanya S. Koparkar Indiana University
14:16
24m
Talk
Copilot 3.0: a Haskell runtime verification framework for UAVs
HIW
Frank Dedden Royal Netherlands Aerospace Center, Alwyn Goodloe NASA Langley Research Center, Ivan Perez NIA / NASA Formal Methods
14:40
20m
Talk
Lightning talks Slot #2
HIW

13:30 - 16:30
Tutorials R4Tutorials at Reindeer
13:30
3h
Tutorial
Programming Language Foundations in Agda
Tutorials
Philip Wadler University of Edinburgh, UK
13:30 - 15:00
Games and GraphicsFARM at Stockholm
Chair(s): April Gonçalves Roskilde University, Denmark
13:30
30m
Talk
Fun with Interfaces (SVG Interfaces for Musical Expression)
FARM
Benedict R. Gaster University of the West of England, Nathan Renney University of West of England, Carinna Parraman University of West of England
14:00
30m
Talk
Mobile Game Programming in Haskell
FARM
Christina Zeller Keera Studios Ltd, Ivan Perez NIA / NASA Formal Methods
14:30
30m
Talk
Demo: Kaleidogen
FARM
Joachim Breitner DFINITY Foundation
15:20 - 16:30
GHCHIW at Elk
Chair(s): Brent Yorgey Hendrix College
15:20
23m
Talk
HoleFitPlugins and the future of interactive development in GHC
HIW
Matthías Páll Gissurarson Chalmers University of Technology, Sweden
15:43
23m
Talk
Explicit Dictionary Applications - From Theory to Practice?
HIW
Dominique Devriese Vrije Universiteit Brussel
File Attached
16:06
23m
Talk
Visible dependent quantification
HIW
Ryan Scott Indiana University at Bloomington, USA
File Attached
15:20 - 16:30
Live-CodingFARM at Stockholm
Chair(s): Donya Quick Stevens Institute of Technology
15:30
30m
Demonstration
Demo: Functors and Music
FARM
Heinrich Apfelmus independent
DOI
16:00
30m
Talk
The sound of lambda
FARM
Felipe Ignacio Noriega Robot Theater Electronics, Anne Veinberg anne veinberg
16:50 - 18:00
CommunityHIW at Elk
16:50
2m
Day closing
HiW'19 report
HIW
Niki Vazou IMDEA Software Institute
16:52
23m
Talk
GHC status report
HIW
Simon Peyton Jones Microsoft, UK
17:15
45m
Other
Panel Discussion
HIW

16:50 - 18:00
Musical PatternsFARM at Stockholm
Chair(s): Daniel Winograd-Cort Target Corp
16:50
30m
Talk
Analyzing Music with Prefix Trees
FARM
Yan Han University of Cambridge, Nada Amin Harvard University, Neel Krishnaswami Computer Laboratory, University of Cambridge
17:20
30m
Talk
What Constitutes a Musical Pattern?
FARM
Orestis Melkonian Utrecht University, Iris Yuping Ren Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Anja Volk Utrecht University