Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
VenueHotel Scandic Berlin Potsdamer Platz
Room nameAurora Borealis
Floor0
Room InformationNo extra information available
Program

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, Ben 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
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, UK
Pre-print
11:50
20m
Talk
Deferring the Details and Deriving Programs
TyDe
Link to publication
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
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
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

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
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 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 The University of Hong Kong, Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven

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
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

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
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

Thu 22 Aug

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

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
13:30 - 15:00
Paper Session 2: VerificationHaskell at Aurora Borealis
Chair(s): Ningning Xie The University of Hong Kong
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
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
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

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
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
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

Sun 18 Aug

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

Mon 19 Aug

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

Thu 22 Aug

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

Fri 23 Aug

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

Mon 19 Aug

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

Wed 21 Aug

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
Aurora Borealis