Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany

Conference Dates
Conference Dates are in time zone (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Conference Day
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 GibbonsDepartment of Computer Science, University of Oxford
09:00
20m
Talk
Flexible Structure Editing of Well-Typed Expressions
TyDe
David Moon, Cyrus OmarUniversity of Chicago, Ben ShapiroUniversity of Colorado, Boulder
Pre-print
09:20
20m
Talk
Livelits: Filling Typed Holes with Live GUIs
TyDe
Cyrus OmarUniversity of Chicago, Nick CollinsUniversity of Chicago, David Moon, Ian VoyseyCarnegie Mellon University, Ravi ChughUniversity of Chicago
Pre-print
09:40
20m
Talk
Formal Investigation of the Extended UTxO Model
TyDe
Orestis MelkonianUtrecht University, Wouter SwierstraUtrecht University, Netherlands, Manuel ChakravartyTweag I/O & IOHK
Pre-print
10:00
20m
Talk
An Algebra of Sequential Decision Problems
TyDe
Robert KrookChalmers University of Technology, Patrik JanssonChalmers University of Technology
Pre-print
09:00 - 10:20
Morning KeynoteScheme at Birch
09:00
60m
Talk
Morning Keynote
Scheme
Edwin BradyUniversity of St. Andrews, UK
09:00 - 10:20
AccelerateFHPNC at Reindeer
Chair(s): Dominic SteinitzTweag I/O
09:00
60m
Talk
Keynote
FHPNC
Trevor L. McDonellUtrecht University
10:00
10m
Talk
GSoC Student Report 1
FHPNC
10:10
10m
Talk
GSoC Student Report 2
FHPNC
Jesse SigalUniversity of Edinburgh
09:00 - 10:20
09:00
10m
Day opening
Welcome
PLMW @ ICFP
David Van HornUniversity of Maryland, USA
09:10
35m
Talk
Effect handler oriented programming
PLMW @ ICFP
Sam LindleyThe University of Edinburgh and Imperial College London
09:45
35m
Talk
Types and verification
PLMW @ ICFP
Niki VazouIMDEA Software Institute
09:00 - 10:20
Session 1Erlang at Yew
09:00
20m
Day opening
Opening
Erlang
Viktória FördősCisco Systems, Adrian FrancalanzaUniversity of Malta
09:20
60m
Talk
Introduction to the Erlang Ecosystem Foundation
Erlang
Peer StritzingerPeer Stritzinger GmbH
10:50 - 12:10
Dependently Typed ProgrammingTyDe at Aurora Borealis
Chair(s): William J. BowmanUniversity of British Columbia
10:50
20m
Talk
Syntax with Shifted Names
TyDe
Pre-print
11:10
20m
Talk
Tic Tac Types (Functional Pearl)
TyDe
Sean InnesUniversity of Bristol, Nicolas WuImperial College London
Link to publication
11:30
20m
Talk
Monadic typed tactic programming by reflection
TyDe
Liang-Ting ChenSwansea University, UK
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 CulpepperCzech Technical University
11:00
30m
Talk
Visualizing Abstract Abstract Machines
Scheme
Kyle HeadleyThe University of Alabama at Birmingham
11:30
30m
Talk
gLua: A modern Lua transpiler in Scheme
Scheme
10:50 - 12:10
10:50
40m
Talk
Managing your research, your advisor, your PhD
PLMW @ ICFP
Amal AhmedNortheastern University, USA
11:30
40m
Talk
Time management, family, and quality of life
PLMW @ ICFP
Kathleen FisherTufts 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 ArtsQuviq, Clara Benac EarleUniversidad Politécnica de Madrid, Hans SvenssonQuviq AB
11:30
40m
Full-paper
Runtime Type Safety for Erlang/OTP Behaviours
Erlang
Joseph HarrisonUniversity 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 GibbonsDepartment of Computer Science, University of Oxford
13:40
50m
Talk
Cubes, Cats, Effects
TyDe
14:30
20m
Talk
Inductive types deconstructed
TyDe
Stefan MonnierUniversité 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 KorkutPrinceton University, USA
14:20
20m
Talk
Reigniting Fuse, an Online Partial Evaluator for Scheme
Scheme
Paulette KoronkevichUniversity 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 SteinitzTweag I/O
13:40
23m
Talk
Compositional Deep Learning in Futhark
FHPNC
Duc Minh TranDIKU, University of Copenhagen, Troels HenriksenUniversity of Copenhagen, Denmark, Martin ElsmanUniversity of Copenhagen, Denmark
Link to publication
14:03
23m
Talk
Towards Hasktorch 1.0: Automated Generation of C++ Libtorch Bindings (extended abstract)
FHPNC
14:26
23m
Talk
Hailstorm : A statically typed functional language for systems programming (extended abstract)
FHPNC
Abhiroop SarkarChalmers University of Technology, Mary Sheeran
13:40 - 14:50
13:40
35m
Talk
Functional Programming is Everywhere
PLMW @ ICFP
Ilya SergeyYale-NUS College and National University of Singapore
14:15
35m
Talk
How to give talks that people can follow
PLMW @ ICFP
13:40 - 14:50
Session 3Erlang at Yew
13:40
23m
Short-paper
Lux - an expect like test tool written in Erlang
Erlang
14:03
23m
Short-paper
Towards Online Profiling of Erlang Systems
Erlang
Michal SlaskiErlang Solutions Ltd., Wojciech TurekAGH University of Science and Technology
14:26
24m
Short-paper
Tools supporting green computing in Erlang
Erlang
Gergely NagyEötvös Lóránd University, Áron Attila MészárosEötvös Lóránd University, István BozóEötvös Loránd University, Melinda TóthEö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 BradyUniversity of St. Andrews, UK
15:20
20m
Talk
Generic Enumerators
TyDe
Cas van der RestUtrecht University, Wouter SwierstraUtrecht University, Netherlands, Manuel ChakravartyTweag I/O & IOHK
Pre-print
15:40
20m
Talk
Generic Level Polymorphic N-ary Functions
TyDe
Guillaume AllaisUniversity of Strathclyde
Link to publication
16:00
20m
Talk
Augmenting Type Signatures for Program Synthesis
TyDe
Bruce CollieUniversity of Edinburgh, Michael F. P. O'BoyleUniversity of Edinburgh
Pre-print
16:20
20m
Talk
Constraint-based Type-directed Program Synthesis
TyDe
Peter-Michael OseraGrinnell 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 EgiRakuten Institute of Technology
16:00
30m
Talk
Stack-Liberated Abstract Garbage Collection
Scheme
Kimball GermaneUniversity of Utah, Michael D. AdamsUniversity of Michigan
15:20 - 16:40
ArraysFHPNC at Reindeer
Chair(s): Fritz HengleinDepartment of Computer Science, University of Copenhagen (DIKU) and Deon Digital
15:20
25m
Talk
Compiling Generalised Histograms for GPU (extended abstract)
FHPNC
Sune HellfritzschUniversity of Copenhagen, Niels G. W. SerupDIKU, University of Copenhagen, Troels HenriksenUniversity of Copenhagen, Denmark, Cosmin OanceaUniversity of Copenhagen, Denmark
15:46
26m
Talk
Position-Dependent Arrays and Their Applicationfor High Performance Code Generation
FHPNC
Federico PizzutiUniversity of Edinburgh, Michel SteuwerUniversity of Glasgow, Christophe DubachUniversity 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 ClaessenChalmers University of Technology, Mary Sheeran, Nicholas SmallboneChalmers University of Technology, Sweden
15:20 - 16:40
15:20
80m
Talk
Social activity
PLMW @ ICFP
Niki VazouIMDEA Software Institute, Joachim BreitnerDFINITY 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 KopestenskiUniversité Catholique de Louvain, Peter Van RoyUniversité catholique de Louvain
16:00
40m
Full-paper
Intro to Web Prolog for Erlangers
Erlang
Torbjörn LagerDepartment of Philosophy, Linguistics and Theory of Science, University of Gothenburg
17:10 - 18:10
Afternoon KeynoteScheme at Birch
17:10
60m
Talk
Afternoon Keynote
Scheme
Andy KeepCisco Systems, Inc
17:10 - 18:10
VerificationFHPNC at Reindeer
Chair(s): Gabriele KellerUtrecht University
17:10
60m
Talk
Formal Verification of Scientific Computing Programs
FHPNC
Micaela MayeroLIPN, Université Paris 13
17:10 - 18:10
17:10
60m
Talk
Panel Discussion: Research in Functional Programming
PLMW @ ICFP
Simon Peyton JonesMicrosoft, UK, Satnam SinghGoogle Research, Zoe ParaskevopoulouPrinceton University, Jeremy GibbonsDepartment of Computer Science, University of Oxford, Andrey MokhovNewcastle University, UK, Amal AhmedNortheastern University, USA
17:10 - 18:10
Session 5Erlang at Yew
17:10
40m
Full-paper
Scaling Erlang Distribution
Erlang
Adam LindbergPeer Stritzinger GmbH, Sébastien MerlePeer Stritzinger GmbH, Peer StritzingerPeer Stritzinger GmbH
17:50
20m
Day closing
Closing
Erlang
Viktória FördősCisco Systems, Adrian FrancalanzaUniversity of Malta
18:10 - 19:10
Happy HourCatering at Restaurant
18:10
60m
Social Event
Happy Hour
Catering

Conference Day
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 DreyerMPI-SWS
09:00
60m
Talk
Blockchains are functional
Keynotes and Reports
Manuel ChakravartyTweag I/O & IOHK
10:30 - 12:00
Compilation & ParallelismResearch Papers at Aurora Borealis
Chair(s): Michael D. AdamsUniversity of Michigan
10:30
22m
Talk
Rebuilding Racket on Chez Scheme (Experience Report)
Research Papers
Matthew FlattUniversity of Utah, Caner DericiIndiana University, R. Kent DybvigCisco Systems, Inc, Andy KeepCisco Systems, Inc, Gustavo E. MassaccesiUniversidad de Buenos Aires, Sarah SpallIndiana University, Sam Tobin-HochstadtIndiana University, Jon Zeppieri
Link to publication DOI
10:52
22m
Talk
Compiling with Continuations, or without? Whatever.
Research Papers
Youyou CongTokyo Institute of Technology, Leo OsvaldPurdue University, USA, Gregory EssertelPurdue University, Tiark RompfPurdue University
11:15
22m
Talk
Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning
Research Papers
Akimasa MorihataUniversity of Tokyo
11:37
22m
Talk
Fairness in Responsive Parallelism
Research Papers
Stefan K. MullerCarnegie Mellon University, Sam WestrickCarnegie Mellon University, Umut A. AcarCarnegie Mellon University
12:00 - 13:30
13:30 - 15:00
Verified CompilationResearch Papers at Aurora Borealis
Chair(s): Ralf JungMPI-SWS
13:30
22m
Talk
Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats
Research Papers
Benjamin DelawarePurdue University, Sorawit Suriyakarn, Clément Pit-ClaudelMIT CSAIL, Qianchuan YePurdue University, Adam ChlipalaMassachusetts Institute of Technology
Link to publication DOI Authorizer link
13:52
22m
Talk
Closure Conversion is Safe for Space
Research Papers
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
14:15
22m
Talk
Linear capabilities for fully abstract compilation of separation-logic-verified code
Research Papers
Thomas Van StrydonckKULeuven, Frank PiessensKU Leuven, Dominique DevrieseVrije Universiteit Brussel
14:37
22m
Talk
The Next 700 Compiler Correctness Theorems. A Functional Pearl.
Research Papers
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
15:20 - 16:30
Type TheoryResearch Papers at Aurora Borealis
Chair(s): Jennifer PaykinGalois, 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 VezzosiChalmers University of Technology, Anders MörtbergDepartment of Mathematics, Stockholm University, Andreas AbelGothenburg University
16:06
23m
Talk
Approximate Normalization for Gradual Dependent Types
Research Papers
Joseph EremondiUniversity of British Columbia, Éric TanterUniversity of Chile & Inria Paris, Ronald GarciaUniversity of British Columbia
Pre-print
16:50 - 18:00
TypesResearch Papers at Aurora Borealis
Chair(s): Richard A. EisenbergBryn Mawr College, USA
16:50
23m
Talk
Simple Noninterference from Parametricity
Research Papers
Maximilian AlgehedChalmers University of Technology, Sweden, Jean-Philippe BernardyUniversity of Gothenburg
17:13
23m
Talk
Selective Applicative Functors
Research Papers
Andrey MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Simon MarlowFacebook, Jeremie DiminoJane Street Europe
Link to publication
17:36
23m
Talk
Coherence of Type Class Resolution
Research Papers
Gert-Jan BottuKU Leuven, Ningning XieThe University of Hong Kong, Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven
18:00 - 20:00
18:00
2h
Poster
SRC Poster Session
Student Research Competition

Conference Day
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 PottierInria, France
09:00
60m
Talk
Solver-Aided Programming for All
Keynotes and Reports
Emina TorlakUniversity of Washington
10:30 - 12:00
Program Analysis & SynthesisResearch Papers at Aurora Borealis
Chair(s): Daniel Winograd-CortTarget Corp
10:30
22m
Talk
Relational Cost Analysis for Functional-Imperative Programs
Research Papers
Weihao QuUniversity at Buffalo, SUNY, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems
10:52
22m
Talk
Fuzzi: A Three-Level Logic for Differential Privacy
Research Papers
Hengchu ZhangUniversity of Pennsylvania, Edo RothUniversity of Pennsylvania, Andreas HaeberlenUniversity of Pennsylvania, USA, Benjamin C. PierceUniversity of Pennsylvania, Aaron RothUniversity of Pennsylvania, USA
11:15
22m
Talk
Synthesizing Differentially Private Programs
Research Papers
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison
11:37
22m
Talk
Synthesizing Symmetric Lenses
Research Papers
Anders MiltnerPrinceton University, Solomon MainaUniversity of Pennsylvania, Kathleen FisherTufts University, USA, Benjamin C. PierceUniversity of Pennsylvania, David WalkerPrinceton University, Steve ZdancewicUniversity of Pennsylvania
Pre-print
12:00 - 13:30
13:30 - 15:00
The Real WorldResearch Papers at Aurora Borealis
Chair(s): Robert AtkeyUniversity of Strathclyde
13:30
22m
Talk
Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator
Research Papers
Fei Wang, Dan ZhengPurdue University, Google Brain, James Decker, Xilun WuPurdue University, Gregory EssertelPurdue University, Tiark RompfPurdue University
Pre-print
13:52
22m
Talk
Efficient Differentiable Programming in a Functional Array-Processing Language
Research Papers
Amir ShaikhhaUniversity of Oxford, Andrew FitzgibbonMicrosoft Research, Cambridge, Dimitrios VytiniotisDeepMind, Simon Peyton JonesMicrosoft, UK
14:15
22m
Talk
From high-level inference algorithms to efficient code
Research Papers
Rajan WaliaIndiana University, Praveen NarayananIndiana University, USA, Jacques CaretteMcMaster University, Sam Tobin-HochstadtIndiana University, Chung-chieh ShanIndiana University, USA
Pre-print
14:37
22m
Talk
Sound and robust solid modeling via exact real arithmetic and continuityDistinguished Paper
Research Papers
Benjamin ShermanMassachusetts Institute of Technology, USA, Jesse MichelMassachusetts Institute of Technology, Michael CarbinMassachusetts Institute of Technology
DOI Pre-print Media Attached
15:20 - 16:30
Dependent Types in HaskellResearch Papers at Aurora Borealis
Chair(s): Joachim BreitnerDFINITY Foundation
15:20
23m
Talk
Dependently Typed Haskell in Industry (Experience Report)
Research Papers
David Thrane ChristiansenGalois, USA, Iavor DiatchkiGalois, Inc., Robert DockinsGalois, Inc., Joe HendrixGalois, Inc., Tristan RavitchGalois, Inc.
15:43
23m
Talk
A Role for Dependent Types in Haskell
Research Papers
Stephanie WeirichUniversity of Pennsylvania, USA, Pritam ChoudhuryUniversity of Pennsylvania, Antoine VoizardUniversity of Pennsylvannia, Richard A. EisenbergBryn Mawr College, USA
16:06
23m
Talk
Higher-order Type-level Programming in Haskell
Research Papers
Csongor KissImperial College London, Tony FieldImperial College London, Susan EisenbachImperial College London, Simon Peyton JonesMicrosoft, 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 SergeyYale-NUS College and National University of Singapore
18:15 - 19:15
Happy HourCatering at Restaurant

Conference Day
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 PottierInria, France
09:00
60m
Talk
Derivations as computations
Keynotes and Reports
Andrej BauerUniversity of Ljubljana
10:30 - 12:00
Program VerificationResearch Papers at Aurora Borealis
Chair(s): Adam ChlipalaMassachusetts Institute of Technology
10:30
22m
Talk
A predicate transformer semantics for effects (Functional Pearl)
Research Papers
Wouter SwierstraUtrecht University, Netherlands, Tim BaanenUtrecht University
10:52
22m
Talk
Dijkstra Monads for All
Research Papers
Kenji MaillardInria Paris and ENS Paris, Danel AhmanUniversity of Ljubljana, Robert AtkeyUniversity of Strathclyde, Guido MartínezCIFASIS-CONICET, Argentina, Cătălin HriţcuInria Paris, Exequiel RivasInria Paris, Éric TanterUniversity of Chile & Inria Paris
Pre-print
11:15
22m
Talk
Mechanized Relational Verification of Concurrent Programs with Continuations
Research Papers
Amin Timanyimec-Distrinet KU-Leuven, Lars BirkedalAarhus University
11:37
22m
Talk
Sequential Programming for Replicated Data Stores
Research Papers
Nicholas V. LewchenkoUniversity of Colorado Boulder, Arjun RadhakrishnaMicrosoft, Akash Gaonkar, Pavol CernyUniversity of Colorado Boulder
DOI Pre-print
12:00 - 13:30
13:30 - 15:00
Modal TypesResearch Papers at Aurora Borealis
Chair(s): Dominique DevrieseVrije Universiteit Brussel
13:30
22m
Talk
Implementing a Modal Dependent Type TheoryDistinguished Paper
Research Papers
Daniel GratzerAarhus University, Jonathan SterlingCarnegie Mellon University, Lars BirkedalAarhus University
13:52
22m
Talk
A Reasonably Exceptional Type Theory
Research Papers
Pierre-Marie PédrotINRIA, Nicolas TabareauInria, Hans FehrmannUniversity of Chile, Éric TanterUniversity of Chile & Inria Paris
14:15
22m
Talk
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks
Research Papers
Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen
14:37
22m
Talk
Quantitative program reasoning with graded modal types
Research Papers
Dominic OrchardUniversity of Kent, UK, Vilem-Benjamin LiepeltUniversity of Kent, UK, Harley D. Eades IIIAugusta University
Pre-print
15:20 - 16:30
TypesResearch Papers at Aurora Borealis
Chair(s): Zoe ParaskevopoulouPrinceton University
15:20
23m
Talk
Mixed Linear and Non-linear Recursive Types
Research Papers
Bert LindenhoviusTulane University, Michael MisloveTulane, Vladimir ZamdzhievInria Nancy
15:43
23m
Talk
A Mechanical Formalization of Higher-Ranked Polymorphic Type InferenceDistinguished Paper
Research Papers
Zhao Jinxu, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Tom SchrijversKU Leuven
16:06
23m
Talk
An Efficient Algorithm for Type-Safe Structural Diffing
Research Papers
Victor Cacciari MiraldoUtrecht University, Netherlands, Wouter SwierstraUtrecht University, Netherlands
16:50 - 18:00
Lambda-Calculus & TeachingResearch Papers at Aurora Borealis
Chair(s): Jonathan ProtzenkoMicrosoft Research, Redmond
16:50
23m
Talk
Call-By-Need is Clairvoyant Call-By-Value
Research Papers
Jennifer HackettUniversity of Nottingham, UK, Graham HuttonUniversity of Nottingham, UK
17:13
23m
Talk
Teaching the Art of Functional Programming Using Automated Grading (Experience Report)
Research Papers
Aliya HameerMcGill University, Brigitte PientkaMcGill University
17:36
23m
Talk
Lambda: the Ultimate Sublanguage (Experience Report)
Research Papers
Jeremy YallopUniversity of Cambridge, UK, Leo WhiteJane 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 PottierInria, France
18:25
5m
Talk
ICFP 2020 Announcement
Keynotes and Reports

18:30 - 19:30
Happy HourCatering at Restaurant

Conference Day
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 IIIAugusta University, Dominic OrchardUniversity of Kent, UK, Vilem-Benjamin LiepeltUniversity of Kent, UK
09:00 - 10:00
Session 1miniKanren at Elk
09:00
60m
Tutorial
Tutorial on miniKanren
miniKanren
William E. ByrdUniversity of Alabama at Birmingham, USA
09:00 - 10:00
Session 1ML at Pine
Chair(s): KC SivaramakrishnanIIT Madras
09:00
60m
Talk
Keynote: An Introduction to the Imandra Automated Reasoning System
ML
I: Grant PassmoreImandra Inc.
09:00 - 12:00
Tutorials R1Tutorials at Reindeer
09:00
3h
Tutorial
Verifying Imperative Programs with SAW
Tutorials
09:00 - 12:00
Tutorials Y1Tutorials at Yew
09:00
3h
Tutorial
Functional Software Architecture
Tutorials
Michael SperberActive Group GmbH
10:30 - 12:00
Paper Session 1: Classes & InstancesHaskell at Aurora Borealis
Chair(s): Jose CalderonGalois, Inc.
10:30
30m
Research paper
Bidirectional Type Class Instances
Haskell
Koen PauwelsKU Leuven, Georgios KarachaliasKU Leuven, Belgium, Michiel DerhaegGuardsquare, Tom SchrijversKU Leuven
11:00
30m
Research paper
Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances
Haskell
Ryan ScottIndiana University at Bloomington, USA, Ryan R. NewtonIndiana 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 DevrieseVrije Universiteit Brussel
File Attached
10:30 - 12:00
Session 2miniKanren at Elk
Chair(s): Lisa ZhangUniversity of Toronto
10:30
45m
Full-paper
Relational Interpreters for Search Problems
miniKanren
Petr LozovSain Petersburg State University, SPbGU, Ekaterina VerbitskaiaSaint 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 HamlenUniversity of Texas at Dallas, USA
Link to publication
10:30 - 12:00
Session 2ML at Pine
Chair(s): Andreas RossbergDfinity Stiftung
10:30
25m
Talk
A right-to-left type system for value recursion
ML
Alban ReynaudENS Lyon, Gabriel SchererINRIA Saclay, Jeremy YallopUniversity of Cambridge, UK
Pre-print
10:55
25m
Talk
let (rec) insertion without effects, lights or magic
ML
Oleg Kiselyov, Jeremy YallopUniversity of Cambridge, UK
Pre-print
11:20
25m
Talk
(TyDe Presentation) FreezeML: Complete and Easy Type Inference for First-Class Polymorphism
ML
Frank EmrichThe University of Edinburgh, Sam LindleyThe University of Edinburgh and Imperial College London, Jan StolarekUniversity of Edinburgh, UK, James CheneyUniversity 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 EmrichThe University of Edinburgh, Sam LindleyThe University of Edinburgh and Imperial College London, Jan StolarekUniversity of Edinburgh, UK, James CheneyUniversity of Edinburgh, UK
Pre-print
12:00 - 13:30
13:30 - 15:00
Paper Session 2: VerificationHaskell at Aurora Borealis
Chair(s): Ningning XieThe University of Hong Kong
13:30
30m
Research paper
Verifying Effectful Haskell Programs in Coq
Haskell
Jan ChristiansenFlensburg University of Applied Sciences, Germany, Sandra DylusUniversity of Kiel, Germany, Niels BunkenburgUniversity 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 MokhovNewcastle University, UK, Georgy LukyanovNewcastle University, UK, Jakob LechnerRUAG Space Austria GmbH
13:30 - 16:30
Tutorials R2Tutorials at Reindeer
13:30
3h
Tutorial
Verifying Imperative Programs with SAW
Tutorials
13:30 - 16:30
Tutorials Y2Tutorials at Yew
13:30
3h
Tutorial
Teaching functional programming
Tutorials
Michael SperberActive Group GmbH
15:20 - 16:30
Paper Session 3: SMT & ArityHaskell at Aurora Borealis
Chair(s): Eric SeidelBloomberg LP
15:20
30m
Research paper
G2Q: Haskell Constraint Solving
Haskell
William T. HallahanYale University, Anton XueYale University, Ruzica PiskacYale University, USA
15:50
30m
Talk
Making a Faster Curry with Extensional Types
Haskell
Paul DownenUniversity of Oregon, USA, Zachary Sullivan, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, 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 ZhangUniversity of Toronto, William E. ByrdUniversity of Alabama at Birmingham, USA, Matthew MightUniversity 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 LuIndiana University, USA, Weixi Ma, Daniel P. FriedmanIndiana University, USA
Link to publication
15:20 - 16:30
Session 4ML at Pine
Chair(s): Gabriel SchererINRIA Saclay
15:20
25m
Talk
An Idris Foreign Function Interface to OCaml
ML
Robert AtkeyUniversity of Strathclyde, Ioan LucaUniversity of Strathclyde
File Attached
15:45
25m
Talk
Necro: Animating Skeletons
ML
File Attached
16:50 - 18:15
Paper Session 4: MetaprogrammingHaskell at Aurora Borealis
Chair(s): Christiaan BaaijQBayLogic B.V.
16:50
30m
Research paper
Multi-Stage Programs in Context
Haskell
Matthew PickeringUniversity of Bristol, Nicolas WuImperial College London, Csongor KissImperial College London
17:20
30m
Research paper
Working with Source Plugins
Haskell
Matthew PickeringUniversity of Bristol, Nicolas WuImperial College London, Boldizsár NémethEötvös Loránd University
17:50
10m
Other
PC Chair Report
Haskell
Richard A. EisenbergBryn 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 BradyUniversity of St. Andrews, UK
16:50
25m
Talk
Compiling Successor ML Pattern Guards
ML
John ReppyUniversity of Chicago, Mona ZahirUniversity of Chicago
Pre-print
17:15
25m
Talk
A Key-Value store for OCaml
ML
Tom RidgeUniversity of Leicester, UK
File Attached
17:40
25m
Talk
Towards Machine Learning Induction in Poly/ML
ML
Yutaka NagashimaData61, Australia
File Attached
18:15 - 20:15
Industrial ReceptionCatering at Restaurant
18:15
2h
Social Event
Industrial Reception
Catering

Conference Day
Fri 23 Aug

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

09:00 - 10:00
KeynoteHaskell at Aurora Borealis
Chair(s): Niki VazouIMDEA 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 AllsoppUniversity of Cambridge
09:00
5m
Day opening
Welcome
OCaml
David AllsoppUniversity of Cambridge
09:05
25m
Talk
Invited Talk
OCaml
Xavier LeroyCollège de France
09:30
30m
Talk
The OCaml Platform in 2019
OCaml
Anil MadhavapeddyOCaml Labs, Gemma GordonUniversity of Cambridge
09:00 - 12:00
Tutorials R3Tutorials at Reindeer
09:00
3h
Tutorial
Programming Language Foundations in Agda
Tutorials
Philip WadlerUniversity of Edinburgh, UK
09:00 - 10:00
SoundFARM at Stockholm
Chair(s): Youyou CongTokyo 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 JaninBordeaux 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 RizkallahUNSW Sydney
10:30
30m
Research paper
STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism
Haskell
Sebastian Ertel, Justus AdamTechnische Universität Dresden, Norman A. RinkTU Dresden, Germany, Andrés Goens, Jeronimo CastrillonTU Dresden, Germany
11:00
30m
Research paper
Synthesizing Functional Reactive Programs
Haskell
Bernd Finkbeiner, Felix KleinSaarland University, Ruzica PiskacYale University, USA, Mark SantolucitoYale University, USA
11:30
30m
Talk
The essence of live coding: Change the program, keep the state!
Haskell
Manuel Bärenzsonnen eServices GmbH
File Attached
10:30 - 12:00
MetadataHIW at Elk
Chair(s): Ningning XieThe University of Hong Kong
10:30
23m
Talk
Configuration, but without CPP
HIW
Matthew PickeringUniversity of Bristol, John EricsonObsidian Systems
10:53
23m
Talk
HIE files in GHC 8.8
HIW
Zubin Duggal, Matthew PickeringUniversity 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 SeriBernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen, Ta-Chu KaoComputational 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 ZhaoUniversity of Cambridge
10:30 - 12:00
Music GenerationFARM at Stockholm
Chair(s): David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
10:30
30m
Talk
Music as Language: Putting Probabilistic Temporal Graph Grammars to Good Use
FARM
Orestis MelkonianUtrecht University
11:00
30m
Talk
A Functional Model of Jazz Improvisation
FARM
Donya QuickStevens Institute of Technology, Kelland ThomasStevens Institute of Technology
11:30
30m
Talk
Demo: Counterpoint by Construction
FARM
Youyou CongTokyo Institute of Technology, John LeoHalfaya Research
12:00 - 13:30
13:30 - 15:00
Paper Session 6: EffectsHaskell at Aurora Borealis
Chair(s): Ki Yung AhnHannam University
13:30
30m
Research paper
Monad Transformers and Modular Algebraic Effects: What Binds Them Together
Haskell
Tom SchrijversKU Leuven, Maciej PirógUniversity of Wrocław, Nicolas WuImperial College London, Mauro JaskelioffCONICET, Argentina
14:00
30m
Research paper
Scoping Monadic Relational Database Queries
Haskell
Anton EkbladChalmers University of Technology
13:30 - 15:00
CompilersHIW at Elk
Chair(s): Jose CalderonGalois, Inc.
13:30
23m
Talk
Status Update on the Helium for Haskell compiler
HIW
Jurriaan HageUtrecht University, Netherlands
13:53
23m
Talk
The Gibbon Compiler: Accelerating a small subset of Haskell
HIW
Ryan R. NewtonIndiana University, Michael VollmerIndiana University, USA, Chaitanya KoparkarIndiana University
14:16
24m
Talk
Copilot 3.0: a Haskell runtime verification framework for UAVs
HIW
Frank DeddenRoyal Netherlands Aerospace Center, Alwyn GoodloeNASA Langley Research Center, Ivan PerezNIA / 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 WadlerUniversity of Edinburgh, UK
13:30 - 15:00
Games and GraphicsFARM at Stockholm
Chair(s): April GonçalvesRoskilde University, Denmark
13:30
30m
Talk
Fun with Interfaces (SVG Interfaces for Musical Expression)
FARM
Benedict R. GasterUniversity of the West of England, Nathan RenneyUniversity of West of England, Carinna ParramanUniversity of West of England
14:00
30m
Talk
Mobile Game Programming in Haskell
FARM
Christina ZellerKeera Studios Ltd, Ivan PerezNIA / NASA Formal Methods
14:30
30m
Talk
Demo: Kaleidogen
FARM
Joachim BreitnerDFINITY Foundation
15:20 - 16:30
GHCHIW at Elk
Chair(s): Brent YorgeyHendrix College
15:20
23m
Talk
HoleFitPlugins and the future of interactive development in GHC
HIW
Matthías Páll GissurarsonChalmers University of Technology, Sweden
15:43
23m
Talk
Explicit Dictionary Applications - From Theory to Practice?
HIW
Dominique DevrieseVrije Universiteit Brussel
File Attached
16:06
23m
Talk
Visible dependent quantification
HIW
Ryan ScottIndiana University at Bloomington, USA
File Attached
15:20 - 16:30
Live-CodingFARM at Stockholm
Chair(s): Donya QuickStevens Institute of Technology
15:30
30m
Demonstration
Demo: Functors and Music
FARM
DOI
16:00
30m
Talk
The sound of lambda
FARM
Felipe Ignacio NoriegaRobot Theater Electronics, Anne Veinberganne veinberg
16:50 - 18:00
CommunityHIW at Elk
16:50
2m
Day closing
HiW'19 report
HIW
Niki VazouIMDEA Software Institute
16:52
23m
Talk
GHC status report
HIW
Simon Peyton JonesMicrosoft, UK
17:15
45m
Other
Panel Discussion
HIW

16:50 - 18:00
Musical PatternsFARM at Stockholm
Chair(s): Daniel Winograd-CortTarget Corp
16:50
30m
Talk
Analyzing Music with Prefix Trees
FARM
Yan HanUniversity of Cambridge, Nada AminHarvard University, Neel KrishnaswamiComputer Laboratory, University of Cambridge
17:20
30m
Talk
What Constitutes a Musical Pattern?
FARM
Orestis MelkonianUtrecht University, Iris Yuping RenUtrecht University, Wouter SwierstraUtrecht University, Netherlands, Anja VolkUtrecht University