Aurora Borealis - ICFP 2019

VenueHotel Scandic Berlin Potsdamer Platz

Room nameAurora Borealis

Floor0

Room InformationNo extra information available

Program

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, ViennaSelect other time zone

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 programSpecify 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 ApplicationsTyDe at Aurora Borealis Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford

09:00 20m Talk		Flexible Structure Editing of Well-Typed Expressions TyDe David Moon , Cyrus Omar University of Chicago, 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 ProgrammingTyDe at Aurora Borealis Chair(s): William J. Bowman University of British Columbia

10:50 20m Talk		Syntax with Shifted Names TyDe Stephen Dolan , Leo White Jane Street Pre-print
11:10 20m Talk		Tic Tac Types (Functional Pearl) TyDe Sean Innes University of Bristol, Nicolas Wu Imperial College London Link to publication
11:30 20m Talk		Monadic typed tactic programming by reflection TyDe Liang-Ting Chen Swansea University 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 MetatheoryTyDe 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 SynthesisTyDe at Aurora Borealis Chair(s): Edwin Brady University of St. Andrews, UK

15:20 20m Talk		Generic Enumerators TyDe Cas van der Rest Utrecht University, Wouter Swierstra Utrecht University, Netherlands, Manuel Chakravarty Tweag I/O & IOHK Pre-print
15:40 20m Talk		Generic Level Polymorphic N-ary Functions TyDe Guillaume Allais University of Strathclyde Link to publication
16:00 20m Talk		Augmenting Type Signatures for Program Synthesis TyDe Bruce Collie University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh Pre-print
16:20 20m Talk		Constraint-based Type-directed Program Synthesis TyDe Peter-Michael Osera Grinnell College Link to publication

17:10 - 18:10	EffectsTyDe at Aurora Borealis Chair(s): David Darais University of Vermont

17:10 20m Talk		Reasoning about Effect Parametricity Using Dependent Types TyDe Joris Ceulemans KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel Pre-print
17:30 20m Talk		How to do proofs? Practically proving properties about effectful programs' results (functional pearl) TyDe Koen Jacobs KU Leuven, Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel Link to publication

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

09:00 - 10:00	Monday KeynoteKeynotes and Reports at Aurora Borealis Chair(s): Derek Dreyer MPI-SWS

09:00 60m Talk		Blockchains are functional Keynotes and Reports Manuel Chakravarty Tweag I/O & IOHK

10:30 - 12:00	Compilation & ParallelismResearch Papers at Aurora Borealis Chair(s): Michael D. Adams University of Michigan

10:30 22m Talk		Rebuilding Racket on Chez Scheme (Experience Report) Research Papers Matthew Flatt University of Utah, Caner Derici Indiana University, R. Kent Dybvig Cisco Systems, Inc, Andy Keep Cisco Systems, Inc, Gustavo E. Massaccesi Universidad de Buenos Aires, Sarah Spall Indiana University, Sam Tobin-Hochstadt Indiana University, Jon Zeppieri Link to publication DOI
10:52 22m Talk		Compiling with Continuations, or without? Whatever. Research Papers Youyou Cong Tokyo Institute of Technology, Leo Osvald Purdue University, USA, Gregory Essertel Purdue University, Tiark Rompf Purdue University
11:15 22m Talk		Lambda Calculus with Algebraic Simplification for Reduction Parallelization by Equational Reasoning Research Papers Akimasa Morihata University of Tokyo
11:37 22m Talk		Fairness in Responsive Parallelism Research Papers Stefan K. Muller Carnegie Mellon University, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University

13:30 - 15:00	Verified CompilationResearch Papers at Aurora Borealis Chair(s): Ralf Jung MPI-SWS

13:30 22m Talk		Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats Research Papers Benjamin Delaware Purdue University, Sorawit Suriyakarn , Clément Pit-Claudel MIT CSAIL, Qianchuan Ye Purdue University, Adam Chlipala Massachusetts Institute of Technology Link to publication DOI Authorizer link
13:52 22m Talk		Closure Conversion is Safe for Space Research Papers Zoe Paraskevopoulou Princeton University, Andrew W. Appel Princeton
14:15 22m Talk		Linear capabilities for fully abstract compilation of separation-logic-verified code Research Papers Thomas Van Strydonck KULeuven, Frank Piessens KU Leuven, Dominique Devriese Vrije Universiteit Brussel
14:37 22m Talk		The Next 700 Compiler Correctness Theorems. A Functional Pearl. Research Papers Daniel Patterson Northeastern University, Amal Ahmed Northeastern University, USA

15:20 - 16:30	Type TheoryResearch Papers at Aurora Borealis Chair(s): Jennifer Paykin Galois, Inc.

15:20 23m Talk		Equations Reloaded: High-Level Dependently-Typed Functional Programming and Proving in Coq Research Papers Matthieu Sozeau Inria, Cyprien Mangin
15:43 23m Talk		Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive TypesDistinguished Paper Research Papers Andrea Vezzosi Chalmers University of Technology, Anders Mörtberg Department of Mathematics, Stockholm University, Andreas Abel Gothenburg University
16:06 23m Talk		Approximate Normalization for Gradual Dependent Types Research Papers Joseph Eremondi University of British Columbia, Éric Tanter University of Chile & Inria Paris, Ronald Garcia University of British Columbia Pre-print

16:50 - 18:00	TypesResearch Papers at Aurora Borealis Chair(s): Richard A. Eisenberg Bryn Mawr College, USA

16:50 23m Talk		Simple Noninterference from Parametricity Research Papers Maximilian Algehed Chalmers University of Technology, Sweden, Jean-Philippe Bernardy University of Gothenburg
17:13 23m Talk		Selective Applicative Functors Research Papers Andrey Mokhov Newcastle University, UK, Georgy Lukyanov Newcastle University, UK, Simon Marlow Facebook, Jeremie Dimino Jane Street Europe Link to publication
17:36 23m Talk		Coherence of Type Class Resolution Research Papers Gert-Jan Bottu KU Leuven, Ningning Xie University of Toronto, Koar Marntirosian KU Leuven, Tom Schrijvers KU Leuven

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

09:00 - 10:00	Tuesday KeynoteKeynotes and Reports at Aurora Borealis Chair(s): François Pottier Inria, France

09:00 60m Talk		Solver-Aided Programming for All Keynotes and Reports Emina Torlak University of Washington

10:30 - 12:00	Program Analysis & SynthesisResearch Papers at Aurora Borealis Chair(s): Daniel Winograd-Cort Target Corp

10:30 22m Talk		Relational Cost Analysis for Functional-Imperative Programs Research Papers Weihao Qu University at Buffalo, SUNY, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems
10:52 22m Talk		Fuzzi: A Three-Level Logic for Differential Privacy Research Papers Hengchu Zhang University of Pennsylvania, Edo Roth University of Pennsylvania, Andreas Haeberlen University of Pennsylvania, USA, Benjamin C. Pierce University of Pennsylvania, Aaron Roth University of Pennsylvania, USA
11:15 22m Talk		Synthesizing Differentially Private Programs Research Papers Calvin Smith University of Wisconsin - Madison, Aws Albarghouthi University of Wisconsin-Madison
11:37 22m Talk		Synthesizing Symmetric Lenses Research Papers Anders Miltner Princeton University, Solomon Maina University of Pennsylvania, Kathleen Fisher Tufts University, USA, Benjamin C. Pierce University of Pennsylvania, David Walker Princeton University, Steve Zdancewic University of Pennsylvania Pre-print

13:30 - 15:00	The Real WorldResearch Papers at Aurora Borealis Chair(s): Robert Atkey University of Strathclyde

13:30 22m Talk		Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator Research Papers Fei Wang , Dan Zheng Purdue University, Google Brain, James Decker , Xilun Wu Purdue University, Gregory Essertel Purdue University, Tiark Rompf Purdue University Pre-print
13:52 22m Talk		Efficient Differentiable Programming in a Functional Array-Processing Language Research Papers Amir Shaikhha University of Oxford, Andrew Fitzgibbon Microsoft Research, Cambridge, Dimitrios Vytiniotis DeepMind, Simon Peyton Jones Microsoft, UK
14:15 22m Talk		From high-level inference algorithms to efficient code Research Papers Rajan Walia Indiana University, Praveen Narayanan Indiana University, USA, Jacques Carette McMaster University, Sam Tobin-Hochstadt Indiana University, Chung-chieh Shan Indiana University, USA Pre-print
14:37 22m Talk		Sound and robust solid modeling via exact real arithmetic and continuityDistinguished Paper Research Papers Benjamin Sherman Massachusetts Institute of Technology, USA, Jesse Michel Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology DOI Pre-print Media Attached

15:20 - 16:30	Dependent Types in HaskellResearch Papers at Aurora Borealis Chair(s): Joachim Breitner DFINITY Foundation

15:20 23m Talk		Dependently Typed Haskell in Industry (Experience Report) Research Papers David Thrane Christiansen Galois, USA, Iavor Diatchki Galois, Inc., Robert Dockins Galois, Inc., Joe Hendrix Galois, Inc., Tristan Ravitch Galois, Inc.
15:43 23m Talk		A Role for Dependent Types in Haskell Research Papers Stephanie Weirich University of Pennsylvania, USA, Pritam Choudhury University of Pennsylvania, Antoine Voizard University of Pennsylvannia, Richard A. Eisenberg Bryn Mawr College, USA
16:06 23m Talk		Higher-order Type-level Programming in Haskell Research Papers Csongor Kiss Imperial College London, Tony Field Imperial College London, Susan Eisenbach Imperial College London, Simon Peyton Jones Microsoft, UK

16:50 - 18:15	Tuesday ReportKeynotes and Reports / Student Research Competition at Aurora Borealis

16:50 40m Talk		SRC Finalist Presentation Student Research Competition
17:30 15m Awards		SIGPLAN Awards Keynotes and Reports
17:45 30m Awards		Programming Contest Report Keynotes and Reports Ilya Sergey Yale-NUS College and National University of Singapore

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

09:00 - 10:00	Wednesday KeynoteKeynotes and Reports at Aurora Borealis Chair(s): François Pottier Inria, France

09:00 60m Talk		Derivations as computations Keynotes and Reports Andrej Bauer University of Ljubljana

10:30 - 12:00	Program VerificationResearch Papers at Aurora Borealis Chair(s): Adam Chlipala Massachusetts Institute of Technology

10:30 22m Talk		A predicate transformer semantics for effects (Functional Pearl) Research Papers Wouter Swierstra Utrecht University, Netherlands, Tim Baanen Utrecht University
10:52 22m Talk		Dijkstra Monads for All Research Papers Kenji Maillard Inria Paris and ENS Paris, Danel Ahman University of Ljubljana, Robert Atkey University of Strathclyde, Guido Martínez CIFASIS-CONICET, Argentina, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Éric Tanter University of Chile & Inria Paris Pre-print
11:15 22m Talk		Mechanized Relational Verification of Concurrent Programs with Continuations Research Papers Amin Timany imec-Distrinet KU-Leuven, Lars Birkedal Aarhus University
11:37 22m Talk		Sequential Programming for Replicated Data Stores Research Papers Nicholas V. Lewchenko University of Colorado Boulder, Arjun Radhakrishna Microsoft, Akash Gaonkar , Pavol Cerny University of Colorado Boulder DOI Pre-print

13:30 - 15:00	Modal TypesResearch Papers at Aurora Borealis Chair(s): Dominique Devriese Vrije Universiteit Brussel

13:30 22m Talk		Implementing a Modal Dependent Type TheoryDistinguished Paper Research Papers Daniel Gratzer Aarhus University, Jonathan Sterling Carnegie Mellon University, Lars Birkedal Aarhus University
13:52 22m Talk		A Reasonably Exceptional Type Theory Research Papers Pierre-Marie Pédrot INRIA, Nicolas Tabareau Inria, Hans Fehrmann University of Chile, Éric Tanter University of Chile & Inria Paris
14:15 22m Talk		Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks Research Papers Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
14:37 22m Talk		Quantitative program reasoning with graded modal types Research Papers Dominic Orchard University of Kent, UK, Vilem-Benjamin Liepelt University of Kent, UK, Harley D. Eades III Augusta University Pre-print

15:20 - 16:30	TypesResearch Papers at Aurora Borealis Chair(s): Zoe Paraskevopoulou Princeton University

15:20 23m Talk		Mixed Linear and Non-linear Recursive Types Research Papers Bert Lindenhovius Tulane University, Michael Mislove Tulane, Vladimir Zamdzhiev Inria Nancy
15:43 23m Talk		A Mechanical Formalization of Higher-Ranked Polymorphic Type InferenceDistinguished Paper Research Papers Zhao Jinxu , Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven
16:06 23m Talk		An Efficient Algorithm for Type-Safe Structural Diffing Research Papers Victor Cacciari Miraldo Utrecht University, Netherlands, Wouter Swierstra Utrecht University, Netherlands

16:50 - 18:00	Lambda-Calculus & TeachingResearch Papers at Aurora Borealis Chair(s): Jonathan Protzenko Microsoft Research, Redmond

16:50 23m Talk		Call-By-Need is Clairvoyant Call-By-Value Research Papers Jennifer Hackett University of Nottingham, UK, Graham Hutton University of Nottingham, UK
17:13 23m Talk		Teaching the Art of Functional Programming Using Automated Grading (Experience Report) Research Papers Aliya Hameer McGill University, Brigitte Pientka McGill University
17:36 23m Talk		Lambda: the Ultimate Sublanguage (Experience Report) Research Papers Jeremy Yallop University of Cambridge, UK, Leo White Jane Street DOI Pre-print

18:00 - 18:30	Wednesday ReportKeynotes and Reports / Student Research Competition at Aurora Borealis

18:00 10m Awards		SRC Awards Presentation Student Research Competition
18:10 15m Talk		Program Chair's Report Keynotes and Reports François Pottier Inria, France
18:25 5m Talk		ICFP 2020 Announcement Keynotes and Reports

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

09:00 - 10:00	KeynoteHaskell 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 & InstancesHaskell at Aurora Borealis Chair(s): Jose Calderon Galois, Inc.

10:30 30m Research paper		Bidirectional Type Class Instances Haskell Koen Pauwels KU Leuven, Georgios Karachalias KU Leuven, Belgium, Michiel Derhaeg Guardsquare, Tom Schrijvers KU Leuven
11:00 30m Research paper		Generic and Flexible Defaults for Verified, Law-Abiding Type-Class Instances Haskell Ryan Scott Indiana University at Bloomington, USA, Ryan R. Newton Indiana University Pre-print File Attached
11:30 30m Research paper		Modular effects in Haskell through effect polymorphism and explicit dictionary applications - A new approach and the μVeriFast verifier as a case study Haskell Dominique Devriese Vrije Universiteit Brussel File Attached

13:30 - 15:00	Paper Session 2: VerificationHaskell at Aurora Borealis Chair(s): Ningning Xie University of Toronto

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 & ArityHaskell at Aurora Borealis Chair(s): Eric Seidel Bloomberg LP

15:20 30m Research paper		G2Q: Haskell Constraint Solving Haskell William T. Hallahan Yale University, Anton Xue Yale University, Ruzica Piskac Yale University, USA
15:50 30m Talk		Making a Faster Curry with Extensional Types Haskell Paul Downen University of Oregon, USA, Zachary Sullivan , Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK

16:50 - 18:15	Paper Session 4: MetaprogrammingHaskell at Aurora Borealis Chair(s): Christiaan Baaij QBayLogic B.V.

16:50 30m Research paper		Multi-Stage Programs in Context Haskell Matthew Pickering University of Bristol, Nicolas Wu Imperial College London, Csongor Kiss Imperial College London
17:20 30m Research paper		Working with Source Plugins Haskell Matthew Pickering University of Bristol, Nicolas Wu Imperial College London, Boldizsár Németh Eötvös Loránd University
17:50 10m Other		PC Chair Report Haskell Richard A. Eisenberg Bryn Mawr College, USA

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

09:00 - 10:00	KeynoteHaskell at Aurora Borealis Chair(s): Niki Vazou IMDEA Software Institute

09:00 60m Talk		Haskell Use and Abuse at Scale Haskell Satnam Singh Google Research, Lennart Augustsson

10:30 - 12:00	Paper Session 5: FRPHaskell at Aurora Borealis Chair(s): Christine Rizkallah UNSW Sydney

10:30 30m Research paper		STCLang: State Thread Composition as a Foundation for Monadic Dataflow Parallelism Haskell Sebastian Ertel , Justus Adam Technische Universität Dresden, Norman A. Rink TU Dresden, Germany, Andrés Goens , Jeronimo Castrillon TU Dresden, Germany
11:00 30m Research paper		Synthesizing Functional Reactive Programs Haskell Bernd Finkbeiner , Felix Klein Saarland University, Ruzica Piskac Yale University, USA, Mark Santolucito Yale University, USA
11:30 30m Talk		The essence of live coding: Change the program, keep the state! Haskell Manuel Bärenz sonnen eServices GmbH File Attached

13:30 - 15:00	Paper Session 6: EffectsHaskell at Aurora Borealis Chair(s): Ki Yung Ahn Hannam University

13:30 30m Research paper		Monad Transformers and Modular Algebraic Effects: What Binds Them Together Haskell Tom Schrijvers KU Leuven, Maciej Piróg University of Wrocław, Nicolas Wu Imperial College London, Mauro Jaskelioff CONICET, Argentina
14:00 30m Research paper		Scoping Monadic Relational Database Queries Haskell Anton Ekblad Chalmers University of Technology

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


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	Keynotes and Reports Monday Keynote																		Research Papers Compilation & Parallelism																																				Research Papers Verified Compilation																						Research Papers Type Theory																		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	Keynotes and Reports Tuesday Keynote																		Research Papers Program Analysis & Synthesis																																				Research Papers The Real World																						Research Papers Dependent Types in Haskell																		Keynotes and Reports + 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	Keynotes and Reports Wednesday Keynote																		Research Papers Program Verification																																				Research Papers Modal Types																						Research Papers Types																		Research Papers Lambda-Calculus & Teaching														Keynotes and Reports + 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 PapersDistinguished 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 PapersDistinguished 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 PapersDistinguished 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 PapersDistinguished 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

Room information: Aurora Borealis

Program Display Configuration

Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 19 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 20 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 21 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 22 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 23 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

TyDe

TyDe

TyDe

TyDe

TyDe

Mon 19 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Keynotes and Reports

Research Papers

Research Papers

Research Papers

Research Papers

Tue 20 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Keynotes and Reports

Research Papers

Research Papers

Research Papers

Keynotes and Reports + Student Research Competition

Wed 21 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Keynotes and Reports

Research Papers

Research Papers

Research Papers

Research Papers

Keynotes and Reports + Student Research Competition

Thu 22 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Haskell

Haskell

Haskell

Haskell

Haskell

Fri 23 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Haskell

Haskell

Haskell

Haskell

Haskell

Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 19 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 20 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 21 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 22 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Fri 23 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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