Write a Blog >>
ICFP 2019
Sun 18 - Fri 23 August 2019 Berlin, Germany
VenueHotel Scandic Berlin Potsdamer Platz
Room nameAurora Borealis
Floor0
Additional informationThere is no additional information of this room 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
Times are displayed in 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 - 09:20
Talk
Flexible Structure Editing of Well-Typed Expressions
TyDe
David Moon, Cyrus OmarUniversity of Chicago, Ben ShapiroUniversity of Colorado, Boulder
Pre-print
09:20 - 09:40
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 - 10:00
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 - 10:20
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 - 11:10
Talk
Syntax with Shifted Names
TyDe
Pre-print
11:10 - 11:30
Talk
Tic Tac Types (Functional Pearl)
TyDe
Sean InnesUniversity of Bristol, Nicolas WuImperial College London
Link to publication
11:30 - 11:50
Talk
Monadic typed tactic programming by reflection
TyDe
Liang-Ting ChenSwansea University, UK
Pre-print
11:50 - 12:10
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 - 14:30
Talk
Cubes, Cats, Effects
TyDe
14:30 - 14:50
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 - 15:40
Talk
Generic Enumerators
TyDe
Cas van der RestUtrecht University, Wouter SwierstraUtrecht University, Netherlands, Manuel ChakravartyTweag I/O & IOHK
Pre-print
15:40 - 16:00
Talk
Generic Level Polymorphic N-ary Functions
TyDe
Guillaume AllaisUniversity of Strathclyde
Link to publication
16:00 - 16:20
Talk
Augmenting Type Signatures for Program Synthesis
TyDe
Bruce CollieUniversity of Edinburgh, Michael F. P. O'BoyleUniversity of Edinburgh
Pre-print
16:20 - 16:40
Talk
Constraint-based Type-directed Program Synthesis
TyDe
Peter-Michael OseraGrinnell College
Link to publication
17:10 - 18:10: EffectsTyDe at Aurora Borealis
Chair(s): David DaraisUniversity of Vermont
17:10 - 17:30
Talk
Reasoning about Effect Parametricity Using Dependent Types
TyDe
Joris CeulemansKU Leuven, Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel
Pre-print
17:30 - 17:50
Talk
How to do proofs? Practically proving properties about effectful programs' results (functional pearl)
TyDe
Koen JacobsKU Leuven, Andreas NuytsKU Leuven, Belgium, Dominique DevrieseVrije Universiteit Brussel
Link to publication

Mon 19 Aug
Times are displayed in 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 - 10:00
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 - 10:52
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 - 11:15
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 - 11:37
Talk
Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning
Research Papers
Akimasa MorihataUniversity of Tokyo
11:37 - 12:00
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 - 13:52
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 - 14:15
Talk
Closure Conversion is Safe for Space
Research Papers
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
14:15 - 14:37
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 - 15:00
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 - 15:43
Talk
Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq
Research Papers
15:43 - 16:06
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 - 16:30
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 - 17:13
Talk
Simple Noninterference from Parametricity
Research Papers
Maximilian AlgehedChalmers University of Technology, Sweden, Jean-Philippe BernardyUniversity of Gothenburg
17:13 - 17:36
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 - 18:00
Talk
Coherence of Type Class Resolution
Research Papers
Gert-Jan BottuKU Leuven, Ningning XieThe University of Hong Kong, Koar MarntirosianKU Leuven, Tom SchrijversKU Leuven

Tue 20 Aug
Times are displayed in 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 - 10:00
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 - 10:52
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 - 11:15
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 - 11:37
Talk
Synthesizing Differentially Private Programs
Research Papers
Calvin SmithUniversity of Wisconsin - Madison, Aws AlbarghouthiUniversity of Wisconsin-Madison
11:37 - 12:00
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 - 13:52
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 - 14:15
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 - 14:37
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 - 15:00
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 - 15:43
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 - 16:06
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 - 16:30
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 - 17:30
Talk
SRC Finalist Presentation
Student Research Competition
17:30 - 17:45
Awards
SIGPLAN Awards
Keynotes and Reports
17:45 - 18:15
Awards
Programming Contest Report
Keynotes and Reports
Ilya SergeyYale-NUS College and National University of Singapore

Wed 21 Aug
Times are displayed in 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 - 10:00
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 - 10:52
Talk
A predicate transformer semantics for effects (Functional Pearl)
Research Papers
Wouter SwierstraUtrecht University, Netherlands, Tim BaanenUtrecht University
10:52 - 11:15
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 - 11:37
Talk
Mechanized Relational Verification of Concurrent Programs with Continuations
Research Papers
Amin Timanyimec-Distrinet KU-Leuven, Lars BirkedalAarhus University
11:37 - 12:00
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 - 13:52
Talk
Implementing a Modal Dependent Type TheoryDistinguished Paper
Research Papers
Daniel GratzerAarhus University, Jonathan SterlingCarnegie Mellon University, Lars BirkedalAarhus University
13:52 - 14:15
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 - 14:37
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 - 15:00
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 - 15:43
Talk
Mixed Linear and Non-linear Recursive Types
Research Papers
Bert LindenhoviusTulane University, Michael MisloveTulane, Vladimir ZamdzhievUniversity of Lorraine, CNRS, Inria, LORIA
15:43 - 16:06
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 - 16:30
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 - 17:13
Talk
Call-By-Need is Clairvoyant Call-By-Value
Research Papers
Jennifer HackettUniversity of Nottingham, UK, Graham HuttonUniversity of Nottingham, UK
17:13 - 17:36
Talk
Teaching the Art of Functional Programming Using Automated Grading (Experience Report)
Research Papers
Aliya HameerMcGill University, Brigitte PientkaMcGill University
17:36 - 18:00
Talk
Lambda: the Ultimate Sublanguage (Experience Report)
Research Papers
Jeremy YallopUniversity of Cambridge, UK, Leo WhiteJane Street
DOI Pre-print
18:00 - 18:10
Awards
SRC Awards Presentation
Student Research Competition
18:10 - 18:25
Talk
Program Chair's Report
Keynotes and Reports
François PottierInria, France
18:25 - 18:30
Talk
ICFP 2020 Announcement
Keynotes and Reports

Thu 22 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00: KeynoteHaskell at Aurora Borealis
Chair(s): Richard A. EisenbergBryn Mawr College, USA
09:00 - 10:00
Talk
Gender equality in academia: meeting the challenge
Haskell
File Attached
10:30 - 12:00: Paper Session 1: Classes & InstancesHaskell at Aurora Borealis
Chair(s): Jose CalderonGalois, Inc.
10:30 - 11:00
Research paper
Bidirectional Type Class Instances
Haskell
Koen PauwelsKU Leuven, Georgios KarachaliasKU Leuven, Belgium, Michiel DerhaegGuardsquare, Tom SchrijversKU Leuven
11:00 - 11:30
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 - 12:00
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 - 14:00
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 - 14:30
Talk
Solving Haskell equality constraints using Coq
Haskell
File Attached
14:30 - 15:00
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 - 15:50
Research paper
G2Q: Haskell Constraint Solving
Haskell
William T. HallahanYale University, Anton XueYale University, Ruzica PiskacYale University, USA
15:50 - 16:20
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 - 17:20
Research paper
Multi-Stage Programs in Context
Haskell
Matthew PickeringUniversity of Bristol, Nicolas WuImperial College London, Csongor KissImperial College London
17:20 - 17:50
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 - 18:00
Other
PC Chair Report
Haskell
Richard A. EisenbergBryn Mawr College, USA

Fri 23 Aug
Times are displayed in 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 - 10:00
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 - 11:00
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 - 11:30
Research paper
Synthesizing Functional Reactive Programs
Haskell
Bernd Finkbeiner, Felix KleinSaarland University, Ruzica PiskacYale University, USA, Mark SantolucitoYale University, USA
11:30 - 12:00
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 - 14:00
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 - 14:30
Research paper
Scoping Monadic Relational Database Queries
Haskell
Anton EkbladChalmers University of Technology

Sun 18 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 19 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 20 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 21 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 22 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 23 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 19 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 21 Aug
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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