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

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

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

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

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

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

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

Conference Day
Sun 18 Aug

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

Conference Day
Mon 19 Aug

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

Conference Day
Tue 20 Aug

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

Conference Day
Wed 21 Aug

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

Conference Day
Thu 22 Aug

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

Conference Day
Fri 23 Aug

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

Conference Day
Mon 19 Aug

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

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