ML 2019
Sun 18 - Fri 23 August 2019
Berlin, Germany
co-located with
ICFP 2019
Toggle navigation
Attending
Venue: Hotel Scandic Berlin Potsdamer Platz
Program
Complete Program
Your Program
Sun 18 Aug
Mon 19 Aug
Tue 20 Aug
Wed 21 Aug
Thu 22 Aug
Fri 23 Aug
Track/Call
Organization
ML 2019 Committees
Track Committees
Organizing Committee
Program Committee
Contributors
People Index
Search
Series
Series
ML 2024
Higher-order, Typed, Inferred, Strict: ML Family Workshop 2023
ML 2022
ML 2021
ML 2020
ML 2019
ML 2018
ML 2017
ML 2016
Sign in
Sign up
ICFP 2019
(
series
) /
ML 2019 (
series
) /
Hotel Scandic Berlin Potsdamer Platz
/
Room information: Aurora Borealis
Venue
Hotel Scandic Berlin Potsdamer Platz
Room name
Aurora Borealis
Floor
0
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
.
Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-06:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+04:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
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 Applications
TyDe
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
10:50 - 12:10
Dependently Typed Programming
TyDe
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
Liam O'Connor
UNSW
Link to publication
13:40 - 14:50
Invited Talk and Metatheory
TyDe
at
Aurora Borealis
Chair(s):
Jeremy Gibbons
Department of Computer Science, University of Oxford
13:40
50m
Talk
Cubes, Cats, Effects
TyDe
Conor McBride
14:30
20m
Talk
Inductive types deconstructed
TyDe
Stefan Monnier
Université de Montréal
Link to publication
15:20 - 16:40
Generic Programming and Synthesis
TyDe
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
Effects
TyDe
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 Keynote
ICFP Keynotes and Reports
at
Aurora Borealis
Chair(s):
Derek Dreyer
MPI-SWS
09:00
60m
Talk
Blockchains are functional
ICFP Keynotes and Reports
Manuel Chakravarty
Tweag I/O & IOHK
10:30 - 12:00
Compilation & Parallelism
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Michael D. Adams
University of Michigan
10:30
22m
Talk
Rebuilding Racket on Chez Scheme (Experience Report)
ICFP 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.
ICFP 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
ICFP Research Papers
Akimasa Morihata
University of Tokyo
11:37
22m
Talk
Fairness in Responsive Parallelism
ICFP Research Papers
Stefan K. Muller
Carnegie Mellon University
,
Sam Westrick
Carnegie Mellon University
,
Umut A. Acar
Carnegie Mellon University
13:30 - 15:00
Verified Compilation
ICFP Research 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
ICFP 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
ICFP 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
ICFP 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.
ICFP Research Papers
Daniel Patterson
Northeastern University
,
Amal Ahmed
Northeastern University, USA
15:20 - 16:30
Type Theory
ICFP Research 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
ICFP Research Papers
Matthieu Sozeau
Inria
,
Cyprien Mangin
15:43
23m
Talk
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Distinguished Paper
ICFP 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
ICFP 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
Types
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Richard A. Eisenberg
Bryn Mawr College, USA
16:50
23m
Talk
Simple Noninterference from Parametricity
ICFP Research Papers
Maximilian Algehed
Chalmers University of Technology, Sweden
,
Jean-Philippe Bernardy
University of Gothenburg
17:13
23m
Talk
Selective Applicative Functors
ICFP 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
ICFP 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 Keynote
ICFP Keynotes and Reports
at
Aurora Borealis
Chair(s):
François Pottier
Inria, France
09:00
60m
Talk
Solver-Aided Programming for All
ICFP Keynotes and Reports
Emina Torlak
University of Washington
10:30 - 12:00
Program Analysis & Synthesis
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Daniel Winograd-Cort
Target Corp
10:30
22m
Talk
Relational Cost Analysis for Functional-Imperative Programs
ICFP 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
ICFP 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
ICFP Research Papers
Calvin Smith
University of Wisconsin - Madison
,
Aws Albarghouthi
University of Wisconsin-Madison
11:37
22m
Talk
Synthesizing Symmetric Lenses
ICFP 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 World
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Robert Atkey
University of Strathclyde
13:30
22m
Talk
Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
ICFP 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
ICFP 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
ICFP 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 continuity
Distinguished Paper
ICFP 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 Haskell
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Joachim Breitner
DFINITY Foundation
15:20
23m
Talk
Dependently Typed Haskell in Industry (Experience Report)
ICFP 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
ICFP 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
ICFP 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
Tuesday Report
ICFP Keynotes and Reports
/
ICFP Student Research Competition
at
Aurora Borealis
16:50
40m
Talk
SRC Finalist Presentation
ICFP Student Research Competition
17:30
15m
Awards
SIGPLAN Awards
ICFP Keynotes and Reports
17:45
30m
Awards
Programming Contest Report
ICFP 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 Keynote
ICFP Keynotes and Reports
at
Aurora Borealis
Chair(s):
François Pottier
Inria, France
09:00
60m
Talk
Derivations as computations
ICFP Keynotes and Reports
Andrej Bauer
University of Ljubljana
10:30 - 12:00
Program Verification
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Adam Chlipala
Massachusetts Institute of Technology
10:30
22m
Talk
A predicate transformer semantics for effects (Functional Pearl)
ICFP Research Papers
Wouter Swierstra
Utrecht University, Netherlands
,
Tim Baanen
Utrecht University
10:52
22m
Talk
Dijkstra Monads for All
ICFP 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
ICFP Research Papers
Amin Timany
imec-Distrinet KU-Leuven
,
Lars Birkedal
Aarhus University
11:37
22m
Talk
Sequential Programming for Replicated Data Stores
ICFP 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 Types
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Dominique Devriese
Vrije Universiteit Brussel
13:30
22m
Talk
Implementing a Modal Dependent Type Theory
Distinguished Paper
ICFP Research Papers
Daniel Gratzer
Aarhus University
,
Jonathan Sterling
Carnegie Mellon University
,
Lars Birkedal
Aarhus University
13:52
22m
Talk
A Reasonably Exceptional Type Theory
ICFP 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
ICFP 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
ICFP 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
Types
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Zoe Paraskevopoulou
Princeton University
15:20
23m
Talk
Mixed Linear and Non-linear Recursive Types
ICFP 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 Inference
Distinguished Paper
ICFP 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
ICFP Research Papers
Victor Cacciari Miraldo
Utrecht University, Netherlands
,
Wouter Swierstra
Utrecht University, Netherlands
16:50 - 18:00
Lambda-Calculus & Teaching
ICFP Research Papers
at
Aurora Borealis
Chair(s):
Jonathan Protzenko
Microsoft Research, Redmond
16:50
23m
Talk
Call-By-Need is Clairvoyant Call-By-Value
ICFP 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)
ICFP Research Papers
Aliya Hameer
McGill University
,
Brigitte Pientka
McGill University
17:36
23m
Talk
Lambda: the Ultimate Sublanguage (Experience Report)
ICFP Research Papers
Jeremy Yallop
University of Cambridge, UK
,
Leo White
Jane Street
DOI
Pre-print
18:00 - 18:30
Wednesday Report
ICFP Keynotes and Reports
/
ICFP Student Research Competition
at
Aurora Borealis
18:00
10m
Awards
SRC Awards Presentation
ICFP Student Research Competition
18:10
15m
Talk
Program Chair's Report
ICFP Keynotes and Reports
François Pottier
Inria, France
18:25
5m
Talk
ICFP 2020 Announcement
ICFP Keynotes and Reports
Thu 22 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
09:00 - 10:00
Keynote
Haskell
at
Aurora Borealis
Chair(s):
Richard A. Eisenberg
Bryn Mawr College, USA
09:00
60m
Talk
Gender equality in academia: meeting the challenge
Haskell
Mary Sheeran
File Attached
10:30 - 12:00
Paper Session 1: Classes & Instances
Haskell
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: Verification
Haskell
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
Zubin Duggal
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 & Arity
Haskell
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: Metaprogramming
Haskell
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
Keynote
Haskell
at
Aurora Borealis
Chair(s):
Niki Vazou
IMDEA Software Institute
09:00
60m
Talk
Haskell Use and Abuse at Scale
Haskell
Satnam Singh
Google Research
,
Lennart Augustsson
10:30 - 12:00
Paper Session 5: FRP
Haskell
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: Effects
Haskell
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
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Aurora Borealis
TyDe
Interaction and Applications
TyDe
Dependently Typed Programming
TyDe
Invited Talk and Metatheory
TyDe
Generic Programming and Synthesis
TyDe
Effects
Mon 19 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Aurora Borealis
ICFP Keynotes and Reports
Monday Keynote
ICFP Research Papers
Compilation & Parallelism
ICFP Research Papers
Verified Compilation
ICFP Research Papers
Type Theory
ICFP Research Papers
Types
Tue 20 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Aurora Borealis
ICFP Keynotes and Reports
Tuesday Keynote
ICFP Research Papers
Program Analysis & Synthesis
ICFP Research Papers
The Real World
ICFP Research Papers
Dependent Types in Haskell
ICFP Keynotes and Reports + ICFP Student Research Competition
Tuesday Report
Wed 21 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Aurora Borealis
ICFP Keynotes and Reports
Wednesday Keynote
ICFP Research Papers
Program Verification
ICFP Research Papers
Modal Types
ICFP Research Papers
Types
ICFP Research Papers
Lambda-Calculus & Teaching
ICFP Keynotes and Reports + ICFP Student Research Competition
Wednesday Report
Thu 22 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
Aurora Borealis
Haskell
Keynote
Haskell
Paper Session 1: Classes & Instances
Haskell
Paper Session 2: Verification
Haskell
Paper Session 3: SMT & Arity
Haskell
Paper Session 4: Metaprogramming
Fri 23 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Aurora Borealis
Haskell
Keynote
Haskell
Paper Session 5: FRP
Haskell
Paper Session 6: Effects
Haskell
Haskell
Sun 18 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Aurora Borealis
TyDe
Flexible Structure Editing of Well-Typed Expressions
09:00 - 09:20
TyDe
Livelits: Filling Typed Holes with Live GUIs
09:20 - 09:40
TyDe
Formal Investigation of the Extended UTxO Model
09:40 - 10:00
TyDe
An Algebra of Sequential Decision Problems
10:00 - 10:20
TyDe
Syntax with Shifted Names
10:50 - 11:10
TyDe
Tic Tac Types (Functional Pearl)
11:10 - 11:30
TyDe
Monadic typed tactic programming by reflection
11:30 - 11:50
TyDe
Deferring the Details and Deriving Programs
11:50 - 12:10
TyDe
Cubes, Cats, Effects
13:40 - 14:30
TyDe
Inductive types deconstructed
14:30 - 14:50
TyDe
Generic Enumerators
15:20 - 15:40
TyDe
Generic Level Polymorphic N-ary Functions
15:40 - 16:00
TyDe
Augmenting Type Signatures for Program Synthesis
16:00 - 16:20
TyDe
Constraint-based Type-directed Program Synthesis
16:20 - 16:40
TyDe
Reasoning about Effect Parametricity Using Dependent Types
17:10 - 17:30
TyDe
How to do proofs? Practically proving properties about effectful progra ...
17:30 - 17:50
Mon 19 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Aurora Borealis
ICFP Keynotes and Reports
Blockchains are functional
09:00 - 10:00
ICFP Research Papers
Rebuilding Racket on Chez Scheme (Experience Report)
10:30 - 10:52
ICFP Research Papers
Compiling with Continuations, or without? Whatever.
10:52 - 11:15
ICFP Research Papers
Lambda Calculus with Algebraic Simplification for Reduction Paralleliza ...
11:15 - 11:37
ICFP Research Papers
Fairness in Responsive Parallelism
11:37 - 12:00
ICFP Research Papers
Narcissus: Correct-By-Construction Derivation of Decoders and Encoders ...
13:30 - 13:52
ICFP Research Papers
Closure Conversion is Safe for Space
13:52 - 14:15
ICFP Research Papers
Linear capabilities for fully abstract compilation of separation-logic- ...
14:15 - 14:37
ICFP Research Papers
The Next 700 Compiler Correctness Theorems. A Functional Pearl.
14:37 - 15:00
ICFP Research Papers
Equations Reloaded: High-Level Dependently-Typed Functional Programming ...
15:20 - 15:43
ICFP Research Papers
Distinguished Paper
Cubical Agda: A Dependently Typed Programming Language with Univalence ...
15:43 - 16:06
ICFP Research Papers
Approximate Normalization for Gradual Dependent Types
16:06 - 16:30
ICFP Research Papers
Simple Noninterference from Parametricity
16:50 - 17:13
ICFP Research Papers
Selective Applicative Functors
17:13 - 17:36
ICFP Research Papers
Coherence of Type Class Resolution
17:36 - 18:00
Tue 20 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
Aurora Borealis
ICFP Keynotes and Reports
Solver-Aided Programming for All
09:00 - 10:00
ICFP Research Papers
Relational Cost Analysis for Functional-Imperative Programs
10:30 - 10:52
ICFP Research Papers
Fuzzi: A Three-Level Logic for Differential Privacy
10:52 - 11:15
ICFP Research Papers
Synthesizing Differentially Private Programs
11:15 - 11:37
ICFP Research Papers
Synthesizing Symmetric Lenses
11:37 - 12:00
ICFP Research Papers
Demystifying Differentiable Programming: Shift/Reset the Penultimate Ba ...
13:30 - 13:52
ICFP Research Papers
Efficient Differentiable Programming in a Functional Array-Processing L ...
13:52 - 14:15
ICFP Research Papers
From high-level inference algorithms to efficient code
14:15 - 14:37
ICFP Research Papers
Distinguished Paper
Sound and robust solid modeling via exact real arithmetic and continuity
14:37 - 15:00
ICFP Research Papers
Dependently Typed Haskell in Industry (Experience Report)
15:20 - 15:43
ICFP Research Papers
A Role for Dependent Types in Haskell
15:43 - 16:06
ICFP Research Papers
Higher-order Type-level Programming in Haskell
16:06 - 16:30
ICFP Student Research Competition
SRC Finalist Presentation
16:50 - 17:30
ICFP Keynotes and Reports
SIGPLAN Awards
17:30 - 17:45
ICFP Keynotes and Reports
Programming Contest Report
17:45 - 18:15
Wed 21 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
Aurora Borealis
ICFP Keynotes and Reports
Derivations as computations
09:00 - 10:00
ICFP Research Papers
A predicate transformer semantics for effects (Functional Pearl)
10:30 - 10:52
ICFP Research Papers
Dijkstra Monads for All
10:52 - 11:15
ICFP Research Papers
Mechanized Relational Verification of Concurrent Programs with Continua ...
11:15 - 11:37
ICFP Research Papers
Sequential Programming for Replicated Data Stores
11:37 - 12:00
ICFP Research Papers
Distinguished Paper
Implementing a Modal Dependent Type Theory
13:30 - 13:52
ICFP Research Papers
A Reasonably Exceptional Type Theory
13:52 - 14:15
ICFP Research Papers
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming With ...
14:15 - 14:37
ICFP Research Papers
Quantitative program reasoning with graded modal types
14:37 - 15:00
ICFP Research Papers
Mixed Linear and Non-linear Recursive Types
15:20 - 15:43
ICFP Research Papers
Distinguished Paper
A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference
15:43 - 16:06
ICFP Research Papers
An Efficient Algorithm for Type-Safe Structural Diffing
16:06 - 16:30
ICFP Research Papers
Call-By-Need is Clairvoyant Call-By-Value
16:50 - 17:13
ICFP Research Papers
Teaching the Art of Functional Programming Using Automated Grading (Exp ...
17:13 - 17:36
ICFP Research Papers
Lambda: the Ultimate Sublanguage (Experience Report)
17:36 - 18:00
ICFP Student Research Competition
SRC Awards Presentation
18:00 - 18:10
ICFP Keynotes and Reports
Program Chair's Report
18:10 - 18:25
ICFP Keynotes and Reports
ICFP 2020 Announcement
18:25 - 18:30
Thu 22 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Aurora Borealis
Haskell
Gender equality in academia: meeting the challenge
09:00 - 10:00
Haskell
Bidirectional Type Class Instances
10:30 - 11:00
Haskell
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Inst ...
11:00 - 11:30
Haskell
Modular effects in Haskell through effect polymorphism and explicit dic ...
11:30 - 12:00
Haskell
Verifying Effectful Haskell Programs in Coq
13:30 - 14:00
Haskell
Solving Haskell equality constraints using Coq
14:00 - 14:30
Haskell
Formal Verification of Spacecraft Control Programs: An Experience Report
14:30 - 15:00
Haskell
G2Q: Haskell Constraint Solving
15:20 - 15:50
Haskell
Making a Faster Curry with Extensional Types
15:50 - 16:20
Haskell
Multi-Stage Programs in Context
16:50 - 17:20
Haskell
Working with Source Plugins
17:20 - 17:50
Haskell
PC Chair Report
17:50 - 18:00
Fri 23 Aug
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
Aurora Borealis
Haskell
Haskell Use and Abuse at Scale
09:00 - 10:00
Haskell
STCLang: State Thread Composition as a Foundation for Monadic Dataflow ...
10:30 - 11:00
Haskell
Synthesizing Functional Reactive Programs
11:00 - 11:30
Haskell
The essence of live coding: Change the program, keep the state!
11:30 - 12:00
Haskell
Monad Transformers and Modular Algebraic Effects: What Binds Them Together
13:30 - 14:00
Haskell
Scoping Monadic Relational Database Queries
14:00 - 14:30
x
Fri 29 Mar 16:32