L1 - ICFP 2017

VenueMathematical Institute

Room nameL1

Floor0

Capacity360

Room InformationNo extra information available

Program

Time Zone

The program is currently displayed in (GMT+01:00) Belfast.

Use conference time zone: (GMT+01:00) BelfastSelect 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 3 Sep
Displayed time zone: Belfast change

09:00 - 09:10	WelcomePLMW at L1 Chair(s): Brigitte Pientka McGill University

09:00 10m Talk		Welcome PLMW Brigitte Pientka McGill University, Neel Krishnaswami Computer Laboratory, University of Cambridge, Daniel R. Licata Wesleyan University

09:10 - 10:00	KeynotePLMW at L1 Chair(s): Neel Krishnaswami Computer Laboratory, University of Cambridge

09:10 50m Talk		Keynote PLMW Chris Martens North Carolina State University

10:30 - 11:30	Session 1PLMW at L1

10:30 30m Talk		A Few Frank Remarks PLMW Conor McBride
11:00 30m Talk		Compositional Compiler Correctness PLMW Amal Ahmed Northeastern University, USA File Attached

12:00 - 12:30	Session 2PLMW at L1

12:00 30m Talk		Not How To Do Your PhD PLMW Gabriel Scherer Northeastern University File Attached

14:00 - 15:00	Session 3PLMW at L1

14:00 30m Talk		Gradual Typing PLMW Ronald Garcia University of British Columbia File Attached
14:30 30m Talk		Scala: Types in Theory & Practice PLMW Nada Amin University of Cambridge File Attached

15:30 - 16:30	Session 4PLMW at L1

15:30 60m Talk		How to Write Papers and Give Talks That People Can Follow PLMW Derek Dreyer MPI-SWS Media Attached

16:50 - 17:40	Session 5PLMW at L1

16:50 50m Talk		Panel Discussion: Careers in Programming Languages PLMW Sam Staton University of Oxford, Richard A. Eisenberg Bryn Mawr College, USA, Andreas Rossberg Google, Daan Leijen , Amal Ahmed Northeastern University, USA

Mon 4 Sep
Displayed time zone: Belfast change

09:00 - 10:00	Monday KeynoteKeynotes and Reports at L1 Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford

09:00 60m Talk		Compositional creativity: some principles for talking to computersKeynote Keynotes and Reports K: Chris Martens North Carolina State University

10:30 - 12:00	Art and EducationResearch Papers at L1 Chair(s): Kathryn E. Gray University of Cambridge

10:30 22m Talk		Super 8 Languages for Making Movies (Functional Pearl) Research Papers Leif Andersen Northeastern University, USA, Stephen Chang Northeastern University, USA, Matthias Felleisen Northeastern University, USA DOI
10:52 22m Talk		Testing and Debugging Functional Reactive Programming Research Papers Ivan Perez University of Nottingham, UK, Henrik Nilsson University of Nottingham, UK DOI
11:15 22m Talk		Lock-Step Simulation Is Child's Play (Experience Report) Research Papers Joachim Breitner University of Pennsylvania, Chris Smith Google, USA DOI
11:37 22m Talk		Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC Research Papers Benjamin Canou OCamlPro, n.n., Roberto Di Cosmo Inria, France / University of Paris Diderot, France, Grégoire Henry OCamlPro, n.n. DOI

13:00 - 14:30	Functional Programming TechniquesResearch Papers at L1 Chair(s): Graham Hutton University of Nottingham

13:00 22m Talk		Faster Coroutine Pipelines Research Papers Mike Spivey University of Oxford, UK DOI
13:22 22m Talk		A Pretty But Not Greedy Printer (Functional Pearl) Research Papers Jean-Philippe Bernardy University of Gothenburg DOI
13:45 22m Talk		Generic Functional Parallel Algorithms: Scan and FFT Research Papers Conal Elliott Target, USA DOI
14:07 22m Talk		A Unified Approach to Solving Seven Programming Problems (Functional Pearl) Research Papers William E. Byrd University of Utah, USA, Michael Ballantyne University of Utah, USA, Gregory Rosenblatt n.n., n.n., Matthew Might University of Utah, USA DOI

15:00 - 16:10	ApplicationsResearch Papers at L1 Chair(s): Alexandra Silva University College London

15:00 23m Talk		Prototyping a Query Compiler using Coq (Experience Report) Research Papers Joshua Auerbach IBM Research, Martin Hirzel IBM Research, Louis Mandel IBM Research, Avraham Shinnar IBM Research, Jerome Simeon IBM Research DOI
15:23 23m Talk		A Framework for Adaptive Differential Privacy Research Papers Daniel Winograd-Cort University of Pennsylvania, USA, Andreas Haeberlen University of Pennsylvania, USA, Aaron Roth University of Pennsylvania, USA, Benjamin C. Pierce University of Pennsylvania DOI
15:46 23m Talk		Symbolic Conditioning of Arrays in Probabilistic Programs Research Papers Praveen Narayanan Indiana University, USA, Chung-chieh Shan Indiana University, USA DOI

16:40 - 18:10	EffectsResearch Papers at L1 Chair(s): Ben Lippmeier Digital Asset / UNSW Australia

16:40 22m Talk		Abstracting Definitional Interpreters Research Papers David Darais University of Maryland, USA, Nicholas Labich University of Maryland, USA, Phúc C. Nguyễn University of Maryland, USA, David Van Horn University of Maryland, USA DOI
17:02 22m Talk		On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control Research Papers Yannick Forster Saarland University, Germany / University of Cambridge, UK, Ohad Kammar University of Oxford, UK, Sam Lindley University of Edinburgh, UK, Matija Pretnar University of Ljubljana, Slovenia DOI
17:25 22m Talk		Imperative Functional Programs That Explain Their Work Research Papers Wilmer Ricciotti University of Edinburgh, UK, Jan Stolarek University of Edinburgh, UK, Roly Perera University of Edinburgh, UK / University of Glasgow, UK, James Cheney University of Edinburgh, UK DOI
17:47 22m Talk		Effect-Driven QuickChecking of Compilers Research Papers Jan Midtgaard DTU, Denmark, Mathias Nygaard Justesen DTU, Denmark, Patrick Kasting DTU, Denmark, Flemming Nielson DTU, Denmark, Hanne Riis Nielson DTU, Denmark DOI

18:10 - 18:20	Monday Closing EventsKeynotes and Reports at L1 Chair(s): Peter Thiemann University of Freiburg, Germany

18:10 10m Day closing		Monday Announcements Keynotes and Reports

Tue 5 Sep
Displayed time zone: Belfast change

09:00 - 10:00	Tuesday KeynoteKeynotes and Reports at L1 Chair(s): Mark Jones Portland State University

09:00 60m Talk		Assuring AIKeynote Keynotes and Reports I: John Launchbury Galois, Inc.

10:30 - 12:00	Low-level and Systems ProgrammingResearch Papers at L1 Chair(s): Sam Tobin-Hochstadt Indiana University

10:30 22m Talk		Persistence for the Masses: RRB-Vectors in a Systems Language Research Papers Juan Pedro Bolívar Puente Independent Consultant, Sinusoidal Engineering DOI Pre-print
10:52 22m Talk		Verified Low-Level Programming Embedded in F* Research Papers Jonathan Protzenko Microsoft Research, n.n., Jean-Karim Zinzindohoué Inria, France, Aseem Rastogi Microsoft Research, Tahina Ramananandro Microsoft Research, n.n., Peng Wang Massachusetts Institute of Technology, USA, Santiago Zanella-Béguelin Microsoft Research, n.n., Antoine Delignat-Lavaud Microsoft Research, n.n., Cătălin Hriţcu Inria Paris, Karthikeyan Bhargavan Inria, France, Cédric Fournet Microsoft Research, n.n., Nikhil Swamy Microsoft Research, n.n. DOI
11:15 22m Talk		Verifying Efficient Function Calls in CakeML Research Papers Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan Carnegie Mellon University, USA DOI
11:37 22m Talk		Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols Research Papers Geoffrey Mainland Drexel University, USA DOI

13:00 - 14:30	Foundations of Higher-Order ProgrammingResearch Papers at L1 Chair(s): Gabriel Scherer Northeastern University

13:00 22m Talk		How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation Research Papers Makoto Hamana Gunma University, Japan DOI
13:22 22m Talk		A Relational Logic for Higher-Order Programs Research Papers Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Spain, Marco Gaboardi University at Buffalo, SUNY, USA, Deepak Garg MPI-SWS, Germany, Pierre-Yves Strub École Polytechnique, n.n. DOI
13:45 22m Talk		Foundations of Strong Call by Need Research Papers Thibaut Balabonski LRI, France / University of Paris-Sud, France, Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia Kesner Université de Paris, CNRS, IRIF, France DOI
14:07 22m Talk		No-Brainer CPS Conversion Research Papers Milo Davis Northeastern University, USA, William Meehan Northeastern University, USA, Olin Shivers Northeastern University, USA DOI

15:00 - 16:10	Tools for VerificationResearch Papers at L1 Chair(s): Nikhil Swamy Microsoft Research, n.n.

15:00 23m Talk		Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification Research Papers Joonwon Choi Massachusetts Institute of Technology, USA, Muralidaran Vijayaraghavan Massachusetts Institute of Technology, USA, Benjamin Sherman Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology, USA, A: Arvind Massachusetts Institute of Technology, USA DOI
15:23 23m Talk		SpaceSearch: A Library for Building and Verifying Solver-Aided Tools Research Papers Konstantin Weitz University of Washington, USA, Steven Lyubomirsky University of Washington, USA, Stefan Heule Stanford University, USA, Emina Torlak University of Washington, USA, Michael D. Ernst University of Washington, USA, Zachary Tatlock University of Washington, Seattle DOI
15:46 23m Talk		Local Refinement Typing Research Papers Benjamin Cosman University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA DOI

16:40 - 17:50	Program ConstructionResearch Papers at L1 Chair(s): John Hughes Chalmers University of Technology

16:40 23m Talk		Compiling to Categories Research Papers Conal Elliott Target, USA DOI
17:03 23m Talk		Visitors Unchained Research Papers François Pottier Inria, France DOI
17:26 23m Talk		Staged Generic Programming Research Papers Jeremy Yallop University of Cambridge, UK DOI Pre-print

17:50 - 18:20	Tuesday Closing EventsKeynotes and Reports at L1

17:50 30m Talk		Programming Contest Report Keynotes and Reports P: Sam Lindley University of Edinburgh, UK

Wed 6 Sep
Displayed time zone: Belfast change

09:00 - 09:37	SRC PresentationsStudent Research Competition at L1 Chair(s): Ilya Sergey University College London

09:00 37m Awards		Student Research Competition: Finalist Presentations Student Research Competition

09:37 - 10:00	Domain-Specific LanguagesResearch Papers at L1 Chair(s): Martin Erwig Oregon State University

09:37 23m Talk		Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) Research Papers Vincent St-Amour Northwestern University, USA, Daniel Feltey Northwestern University, USA, Spencer P. Florence Northwestern University, USA, Shu-Hung You Northwestern University, USA, Robert Bruce Findler Northwestern University, USA DOI

10:30 - 12:00	Dependently Typed ProgrammingResearch Papers at L1 Chair(s): Daniel R. Licata Wesleyan University

10:30 22m Talk		A Specification for Dependent Types in Haskell Research Papers Stephanie Weirich University of Pennsylvania, USA, Antoine Voizard University of Pennsylvania, USA, Pedro Henrique Azevedo de Amorim Ecole Polytechnique, n.n. / University of Campinas, Brazil, Richard A. Eisenberg Bryn Mawr College, USA DOI
10:52 22m Talk		Parametric Quantifiers for Dependent Type Theory Research Papers Andreas Nuyts KU Leuven, Belgium, Andrea Vezzosi Chalmers University of Technology, Sweden, Dominique Devriese KU Leuven, Belgium DOI
11:15 22m Talk		Normalization by Evaluation for Sized Dependent Types Research Papers Andreas Abel University of Gothenburg, Sweden, Andrea Vezzosi Chalmers University of Technology, Sweden, Théo Winterhalter ENS Paris-Saclay, France DOI
11:37 22m Talk		A Metaprogramming Framework for Formal Verification Research Papers Gabriel Ebner Vienna University of Technology, Austria, Sebastian Ullrich KIT, Germany, Jared Roesch University of Washington, USA, Jeremy Avigad Carnegie Mellon University, USA, Leonardo de Moura Microsoft Research, n.n. DOI

13:00 - 14:30	Contracts and SessionsResearch Papers at L1 Chair(s): Matthew Flatt University of Utah

13:00 22m Talk		Chaperone Contracts for Higher-Order Sessions Research Papers Hernan Melgratti University of Buenos Aires, Argentina, Luca Padovani University of Turin, Italy DOI
13:22 22m Talk		Whip: Higher-Order Contracts for Modern Services Research Papers Lucas Waye Harvard University, USA, Christos Dimoulas Harvard University, USA, Stephen Chong Harvard University, USA DOI
13:45 22m Talk		Manifest Sharing with Session Types Research Papers Stephanie Balzer Carnegie Mellon University, USA, Frank Pfenning Carnegie Mellon University, USA DOI
14:07 22m Talk		Gradual Session Types Research Papers Atsushi Igarashi Kyoto University, Japan, Peter Thiemann University of Freiburg, Germany, Vasco T. Vasconcelos University of Lisbon, Portugal, Philip Wadler University of Edinburgh, UK DOI

15:00 - 16:10	Integrating Static and Dynamic TypingResearch Papers at L1 Chair(s): Ronald Garcia University of British Columbia

15:00 23m Talk		Theorems for Free for Free: Parametricity, With and Without Types Research Papers Amal Ahmed Northeastern University, USA, Dustin Jamner Northeastern University, USA, Jeremy G. Siek Indiana University, USA, Philip Wadler University of Edinburgh, UK DOI
15:23 23m Talk		On Polymorphic Gradual Typing Research Papers Yuu Igarashi Kyoto University, Japan, Taro Sekiyama IBM Research, Japan, Atsushi Igarashi Kyoto University, Japan DOI
15:46 23m Talk		Gradual Typing with Union and Intersection Types Research Papers Giuseppe Castagna CNRS, France / University of Paris Diderot, France, Victor Lanvin ENS Cachan, France DOI

16:40 - 17:50	Inference and AnalysisResearch Papers at L1 Chair(s): Mark Jones Portland State University

16:40 23m Talk		Constrained Type Families Research Papers J. Garrett Morris University of Kansas, USA, Richard A. Eisenberg Bryn Mawr College, USA DOI
17:03 23m Talk		Automating Sized-Type Inference for Complexity Analysis Research Papers Martin Avanzini University of Innsbruck, Austria, Ugo Dal Lago University of Bologna, Italy / Inria, France DOI
17:26 23m Talk		Inferring Scope through Syntactic Sugar Research Papers Justin Pombrio Brown University, USA, Shriram Krishnamurthi Brown University, USA, Mitchell Wand Northeastern University, USA DOI

17:50 - 18:00	SRC AwardsStudent Research Competition at L1 Chair(s): Ilya Sergey University College London

17:50 10m Awards		Student Research Competition Awards Student Research Competition S: Ilya Sergey University College London

18:00 - 18:20	Wednesday Closing EventsKeynotes and Reports at L1

18:00 10m Talk		Program Chair's Report Keynotes and Reports P: Mark Jones Portland State University
18:10 10m Talk		ICFP 2018 Announcement Keynotes and Reports I: Robert Bruce Findler Northwestern University, USA

Thu 7 Sep
Displayed time zone: Belfast change

09:00 - 10:00	Day 1, Session 1Haskell at L1

09:00 60m Talk		Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (Invited Talk) Haskell Didier Rémy INRIA

10:30 - 11:30	Day 1, Session 2Haskell at L1

10:30 30m Talk		Algebraic Graphs with Class (Functional Pearl) Haskell Andrey Mokhov
11:00 30m Talk		Packrats Parse in Packs Haskell Mario Blažević , Jacques Légaré

12:00 - 12:30	Day 1, Session 3Haskell at L1

12:00 30m Talk		Ode on a Random Urn (Functional Pearl) Haskell Leonidas Lampropoulos University of Pennsylvania, Antal Spector-Zabusky , Kenneth Foner

14:00 - 15:00	Day 1, Session 4Haskell at L1

14:00 30m Demonstration		QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration) Haskell Maximilian Algehed Chalmers University of Technology, Sweden, Koen Claessen Chalmers University of Technology, Moa Johansson Chalmers University of Technology, Nicholas Smallbone
14:30 30m Talk		Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results Haskell Rudy Braquehais , Colin Runciman

15:30 - 16:30	Day 1, Session 5Haskell at L1

15:30 30m Talk		Using Coq to Write Fast and Correct Haskell Haskell John Wiegley , Benjamin Delaware Purdue University
16:00 30m Talk		A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq Haskell Niki Vazou University of Maryland, Leonidas Lampropoulos University of Pennsylvania, Jeff Polakow

16:50 - 17:50	Day 1, Session 6Haskell at L1

16:50 30m Talk		A Meta-EDSL for Distributed Web Applications Haskell Anton Ekblad Chalmers University of Technology
17:20 30m Talk		Composable Network Stacks and Remote Monads Haskell Justin Dawson , Mark Grebe , Andy Gill

Fri 8 Sep
Displayed time zone: Belfast change

09:00 - 10:00	Day 2, Session 1Haskell at L1

09:00 60m Talk		Algorithmic Music in Haskell (Invited Talk) Haskell Donya Quick Stevens Institute of Technology

10:30 - 11:30	Day 2, Session 2Haskell at L1

10:30 30m Talk		Well-Typed Music Does Not Sound Wrong (Experience Report) Haskell Dmitrij Szamozvancev , Michael Gale University of Warwick, UK
11:00 30m Talk		Back to the Future: Time Travel in FRP Haskell Ivan Perez University of Nottingham, UK

12:00 - 12:30	Day 2, Session 3Haskell at L1

12:00 30m Talk		The Linearity Monad Haskell Jennifer Paykin University of Pennsylvania, Steve Zdancewic University of Pennsylvania

14:00 - 15:00	Day 2, Session 4Haskell at L1

14:00 30m Talk		Elaboration on Functional Dependencies Haskell Georgios Karachalias KU Leuven, Belgium, Tom Schrijvers KU Leuven
14:30 30m Talk		Quantified Class Constraints Haskell Gert-Jan Bottu , Georgios Karachalias KU Leuven, Belgium, Tom Schrijvers KU Leuven, Bruno C. d. S. Oliveira University of Hong Kong, China, Philip Wadler University of Edinburgh, UK

15:30 - 16:30	Day 2, Session 5Haskell at L1

15:30 30m Talk		Hardware Software Co-Design in Haskell Haskell Markus Aronsson , Mary Sheeran
16:00 30m Talk		Streaming Irregular Arrays Haskell Robert Clifton-Everest , Trevor L. McDonell University of New South Wales, Australia, Manuel Chakravarty , Gabriele Keller Data61,CSIRO (formerly NICTA) and UNSW

16:50 - 17:50	Day 2, Session 6Haskell at L1

16:50 30m Talk		Improving STM Performance with Transactional Structs Haskell Ryan Yates , Michael Scott University of Rochester
17:20 30m Talk		Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping Haskell Chao-Hong Chen Indiana University, Vikraman Choudhury , Ryan R. Newton Indiana University

Sat 9 Sep
Displayed time zone: Belfast change

09:00 - 10:10	State of GHCHIW at L1 Chair(s): Richard A. Eisenberg Bryn Mawr College, USA

09:00 30m Talk		Progress on GHC HIW Simon Peyton Jones Microsoft Research, Cambridge
09:30 30m Talk		GHC Infrastructure Update and Discussion HIW Ben Gamari Well-Typed LLP
10:00 10m Talk		Getting Ready for Hadrian HIW Andrey Mokhov , Zhen Zhang University of Washington, Ben Gamari Well-Typed LLP, Neil Mitchell

10:30 - 11:30	Compiling to LLVMHIW at L1 Chair(s): Jan Stolarek University of Edinburgh, UK

10:30 25m Talk		Native Support for Explicit Stacks in LLVM HIW Kavon Farvardin University of Chicago, Simon Peyton Jones Microsoft Research, Cambridge
10:55 25m Talk		SimplexHC: Lowering High-Level Haskell to Imperative IR HIW Siddharth Bhat IIT Hyderabad
11:20 10m Talk		Lightning Talk Slot #1 HIW

12:00 - 12:25	ConstraintsHIW at L1 Chair(s): Ben Gamari Well-Typed LLP

12:00 25m Talk		On Unsatisfiability HIW J. Garrett Morris University of Kansas, USA

14:00 - 15:00	Working in CoreHIW at L1 Chair(s): Adam Gundry Well-Typed LLP

14:00 25m Talk		Why GHC Core and Linear Logic Should be Best Friends HIW Carter Schonwald , Joel Burget
14:25 25m Talk		Demand Analysis vs. Call Arity HIW Sebastian Graf Karlsruhe Institute of Technology
14:50 10m Talk		Lightning Talk Slot #2 HIW

15:30 - 16:30	Tool SupportHIW at L1 Chair(s): Wren Romano X

15:30 25m Talk		IDE Support in GHC HIW Alan Zimmerman
15:55 25m Talk		Tracking GHC Performance HIW Mathieu Boespflug Tweag I/O, Manuel Chakravarty
16:20 10m Talk		Lightning Talk Slot #3 HIW

16:50 - 17:50	All Broken UpHIW at L1 Chair(s): Bartosz Nitka Facebook

16:50 25m Talk		An Experiment in Fragment-Based Code Distribution HIW Philipp Schuster University of Tübingen
17:15 35m Talk		Lightning Talk Slot #4 HIW

Sun 3 Sep
Displayed time zone: Belfast 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
L1	PLMW Welcome		PLMW Keynote																PLMW Session 1																		PLMW Session 2																								PLMW Session 3																		PLMW Session 4																PLMW Session 5

Mon 4 Sep
Displayed time zone: Belfast 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
L1	Keynotes and Reports Monday Keynote																		Research Papers Art and Education																														Research Papers Functional Programming Techniques																								Research Papers Applications																				Research Papers Effects																		Keynotes and Reports Monday Closing Events

Tue 5 Sep
Displayed time zone: Belfast 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
L1	Keynotes and Reports Tuesday Keynote																		Research Papers Low-level and Systems Programming																														Research Papers Foundations of Higher-Order Programming																								Research Papers Tools for Verification																				Research Papers Program Construction														Keynotes and Reports Tuesday Closing Events

Wed 6 Sep
Displayed time zone: Belfast 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
L1	Student Research Competition SRC Presentations							Research Papers Domain-Specific Languages											Research Papers Dependently Typed Programming																														Research Papers Contracts and Sessions																								Research Papers Integrating Static and Dynamic Typing																				Research Papers Inference and Analysis														Student Research Competition SRC Awards		Keynotes and Reports Wednesday Closing Events Keynotes and Reports 18:10 - 18:20

Thu 7 Sep
Displayed time zone: Belfast 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
L1	Haskell Day 1, Session 1																		Haskell Day 1, Session 2																		Haskell Day 1, Session 3																								Haskell Day 1, Session 4																		Haskell Day 1, Session 5																Haskell Day 1, Session 6

Fri 8 Sep
Displayed time zone: Belfast 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
L1	Haskell Day 2, Session 1																		Haskell Day 2, Session 2																		Haskell Day 2, Session 3																								Haskell Day 2, Session 4																		Haskell Day 2, Session 5																Haskell Day 2, Session 6

Sat 9 Sep
Displayed time zone: Belfast 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
L1	HIW State of GHC																		HIW Compiling to LLVM																		HIW Constraints																								HIW Working in Core																		HIW Tool Support																HIW All Broken Up

Sun 3 Sep
Displayed time zone: Belfast 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
L1	PLMW Welcome 09:00 - 09:10		PLMW Keynote 09:10 - 10:00																PLMW A Few Frank Remarks 10:30 - 11:00						PLMW Compositional Compiler Correctness 11:00 - 11:30												PLMW Not How To Do Your PhD 12:00 - 12:30																								PLMW Gradual Typing 14:00 - 14:30						PLMW Scala: Types in Theory & Practice 14:30 - 15:00												PLMW How to Write Papers and Give Talks That People Can Follow 15:30 - 16:30																PLMW Panel Discussion: Careers in Programming Languages 16:50 - 17:40

Mon 4 Sep
Displayed time zone: Belfast 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
L1	ICFP Keynotes and ReportsKeynote Compositional creativity: some principles for talking to computers 09:00 - 10:00																		ICFP Research Papers Super 8 Languages for Making Movies (Functional Pearl) 10:30 - 10:52				ICFP Research Papers Testing and Debugging Functional Reactive Programming 10:52 - 11:15					ICFP Research Papers Lock-Step Simulation Is Child's Play (Experience Report) 11:15 - 11:37				ICFP Research Papers Scaling up Functional Programming Education: Under the Hood of the OCam ... 11:37 - 12:00																	ICFP Research Papers Faster Coroutine Pipelines 13:00 - 13:22				ICFP Research Papers A Pretty But Not Greedy Printer (Functional Pearl) 13:22 - 13:45					ICFP Research Papers Generic Functional Parallel Algorithms: Scan and FFT 13:45 - 14:07				ICFP Research Papers A Unified Approach to Solving Seven Programming Problems (Functional Pearl) 14:07 - 14:30											ICFP Research Papers Prototyping a Query Compiler using Coq (Experience Report) 15:00 - 15:23					ICFP Research Papers A Framework for Adaptive Differential Privacy 15:23 - 15:46				ICFP Research Papers Symbolic Conditioning of Arrays in Probabilistic Programs 15:46 - 16:10											ICFP Research Papers Abstracting Definitional Interpreters 16:40 - 17:02				ICFP Research Papers On the Expressive Power of User-Defined Effects: Effect Handlers, Monad ... 17:02 - 17:25					ICFP Research Papers Imperative Functional Programs That Explain Their Work 17:25 - 17:47				ICFP Research Papers Effect-Driven QuickChecking of Compilers 17:47 - 18:10					ICFP Keynotes and Reports Monday Announcements 18:10 - 18:20

Tue 5 Sep
Displayed time zone: Belfast 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
L1	ICFP Keynotes and ReportsKeynote Assuring AI 09:00 - 10:00																		ICFP Research Papers Persistence for the Masses: RRB-Vectors in a Systems Language 10:30 - 10:52				ICFP Research Papers Verified Low-Level Programming Embedded in F* 10:52 - 11:15					ICFP Research Papers Verifying Efficient Function Calls in CakeML 11:15 - 11:37				ICFP Research Papers Better Living through Operational Semantics: An Optimizing Compiler for ... 11:37 - 12:00																	ICFP Research Papers How to Prove Your Calculus Is Decidable: Practical Applications of Seco ... 13:00 - 13:22				ICFP Research Papers A Relational Logic for Higher-Order Programs 13:22 - 13:45					ICFP Research Papers Foundations of Strong Call by Need 13:45 - 14:07				ICFP Research Papers No-Brainer CPS Conversion 14:07 - 14:30											ICFP Research Papers Kami: A Platform for High-Level Parametric Hardware Specification and I ... 15:00 - 15:23					ICFP Research Papers SpaceSearch: A Library for Building and Verifying Solver-Aided Tools 15:23 - 15:46				ICFP Research Papers Local Refinement Typing 15:46 - 16:10											ICFP Research Papers Compiling to Categories 16:40 - 17:03					ICFP Research Papers Visitors Unchained 17:03 - 17:26				ICFP Research Papers Staged Generic Programming 17:26 - 17:50					ICFP Keynotes and Reports Programming Contest Report 17:50 - 18:20

Wed 6 Sep
Displayed time zone: Belfast 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
L1	ICFP Student Research Competition Student Research Competition: Finalist Presentations 09:00 - 09:37							ICFP Research Papers Herbarium Racketensis: A Stroll through the Woods (Functional Pearl) 09:37 - 10:00											ICFP Research Papers A Specification for Dependent Types in Haskell 10:30 - 10:52				ICFP Research Papers Parametric Quantifiers for Dependent Type Theory 10:52 - 11:15					ICFP Research Papers Normalization by Evaluation for Sized Dependent Types 11:15 - 11:37				ICFP Research Papers A Metaprogramming Framework for Formal Verification 11:37 - 12:00																	ICFP Research Papers Chaperone Contracts for Higher-Order Sessions 13:00 - 13:22				ICFP Research Papers Whip: Higher-Order Contracts for Modern Services 13:22 - 13:45					ICFP Research Papers Manifest Sharing with Session Types 13:45 - 14:07				ICFP Research Papers Gradual Session Types 14:07 - 14:30											ICFP Research Papers Theorems for Free for Free: Parametricity, With and Without Types 15:00 - 15:23					ICFP Research Papers On Polymorphic Gradual Typing 15:23 - 15:46				ICFP Research Papers Gradual Typing with Union and Intersection Types 15:46 - 16:10											ICFP Research Papers Constrained Type Families 16:40 - 17:03					ICFP Research Papers Automating Sized-Type Inference for Complexity Analysis 17:03 - 17:26				ICFP Research Papers Inferring Scope through Syntactic Sugar 17:26 - 17:50					ICFP Student Research Competition Student Research Competition Awards 17:50 - 18:00		ICFP Keynotes and Reports Program Chair's Report 18:00 - 18:10		ICFP Keynotes and Reports ICFP 2018 Announcement 18:10 - 18:20

Thu 7 Sep
Displayed time zone: Belfast 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
L1	Haskell Ornaments: exploiting parametricity for safer, more automated code refa ... 09:00 - 10:00																		Haskell Algebraic Graphs with Class (Functional Pearl) 10:30 - 11:00						Haskell Packrats Parse in Packs 11:00 - 11:30												Haskell Ode on a Random Urn (Functional Pearl) 12:00 - 12:30																								Haskell QuickSpec: A Lightweight Theory Exploration Tool for Programmers (Syste ... 14:00 - 14:30						Haskell Speculate: Discovering Conditional Equations and Inequalities about Bla ... 14:30 - 15:00												Haskell Using Coq to Write Fast and Correct Haskell 15:30 - 16:00						Haskell A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Has ... 16:00 - 16:30										Haskell A Meta-EDSL for Distributed Web Applications 16:50 - 17:20						Haskell Composable Network Stacks and Remote Monads 17:20 - 17:50

Fri 8 Sep
Displayed time zone: Belfast 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
L1	Haskell Algorithmic Music in Haskell (Invited Talk) 09:00 - 10:00																		Haskell Well-Typed Music Does Not Sound Wrong (Experience Report) 10:30 - 11:00						Haskell Back to the Future: Time Travel in FRP 11:00 - 11:30												Haskell The Linearity Monad 12:00 - 12:30																								Haskell Elaboration on Functional Dependencies 14:00 - 14:30						Haskell Quantified Class Constraints 14:30 - 15:00												Haskell Hardware Software Co-Design in Haskell 15:30 - 16:00						Haskell Streaming Irregular Arrays 16:00 - 16:30										Haskell Improving STM Performance with Transactional Structs 16:50 - 17:20						Haskell Adaptive Lock-Free Data Structures in Haskell: A General Method for Con ... 17:20 - 17:50

Sat 9 Sep
Displayed time zone: Belfast 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
L1	HIW Progress on GHC 09:00 - 09:30						HIW GHC Infrastructure Update and Discussion 09:30 - 10:00						HIW Getting Ready for Hadrian 10:00 - 10:10						HIW Native Support for Explicit Stacks in LLVM 10:30 - 10:55					HIW SimplexHC: Lowering High-Level Haskell to Imperative IR 10:55 - 11:20					HIW Lightning Talk Slot #1 11:20 - 11:30								HIW On Unsatisfiability 12:00 - 12:25																								HIW Why GHC Core and Linear Logic Should be Best Friends 14:00 - 14:25					HIW Demand Analysis vs. Call Arity 14:25 - 14:50					HIW Lightning Talk Slot #2 14:50 - 15:00								HIW IDE Support in GHC 15:30 - 15:55					HIW Tracking GHC Performance 15:55 - 16:20					HIW Lightning Talk Slot #3 16:20 - 16:30						HIW An Experiment in Fragment-Based Code Distribution 16:50 - 17:15					HIW Lightning Talk Slot #4 17:15 - 17:50

Room information: L1

Program Display Configuration

Sun 3 SepDisplayed time zone: Belfast change

Mon 4 SepDisplayed time zone: Belfast change

Tue 5 SepDisplayed time zone: Belfast change

Wed 6 SepDisplayed time zone: Belfast change

Thu 7 SepDisplayed time zone: Belfast change

Fri 8 SepDisplayed time zone: Belfast change

Sat 9 SepDisplayed time zone: Belfast change

Sun 3 SepDisplayed time zone: Belfast change

PLMW

PLMW

PLMW

PLMW

PLMW

PLMW

PLMW

Mon 4 SepDisplayed time zone: Belfast change

Keynotes and Reports

Research Papers

Research Papers

Research Papers

Research Papers

Keynotes and Reports

Tue 5 SepDisplayed time zone: Belfast change

Keynotes and Reports

Research Papers

Research Papers

Research Papers

Research Papers

Keynotes and Reports

Wed 6 SepDisplayed time zone: Belfast change

Student Research Competition

Research Papers

Research Papers

Research Papers

Research Papers

Research Papers

Student Research Competition

Keynotes and Reports

Keynotes and Reports

Thu 7 SepDisplayed time zone: Belfast change

Haskell

Haskell

Haskell

Haskell

Haskell

Haskell

Fri 8 SepDisplayed time zone: Belfast change

Haskell

Haskell

Haskell

Haskell

Haskell

Haskell

Sat 9 SepDisplayed time zone: Belfast change

HIW

HIW

HIW

HIW

HIW

HIW

Sun 3 SepDisplayed time zone: Belfast change

Mon 4 SepDisplayed time zone: Belfast change

Tue 5 SepDisplayed time zone: Belfast change

Wed 6 SepDisplayed time zone: Belfast change

Thu 7 SepDisplayed time zone: Belfast change

Fri 8 SepDisplayed time zone: Belfast change

Sat 9 SepDisplayed time zone: Belfast change

Sun 3 Sep
Displayed time zone: Belfast change

Mon 4 Sep
Displayed time zone: Belfast change

Tue 5 Sep
Displayed time zone: Belfast change

Wed 6 Sep
Displayed time zone: Belfast change

Thu 7 Sep
Displayed time zone: Belfast change

Fri 8 Sep
Displayed time zone: Belfast change

Sat 9 Sep
Displayed time zone: Belfast change

Sun 3 Sep
Displayed time zone: Belfast change

Mon 4 Sep
Displayed time zone: Belfast change

Tue 5 Sep
Displayed time zone: Belfast change

Wed 6 Sep
Displayed time zone: Belfast change

Thu 7 Sep
Displayed time zone: Belfast change

Fri 8 Sep
Displayed time zone: Belfast change

Sat 9 Sep
Displayed time zone: Belfast change

Sun 3 Sep
Displayed time zone: Belfast change

Mon 4 Sep
Displayed time zone: Belfast change

Tue 5 Sep
Displayed time zone: Belfast change

Wed 6 Sep
Displayed time zone: Belfast change

Thu 7 Sep
Displayed time zone: Belfast change

Fri 8 Sep
Displayed time zone: Belfast change

Sat 9 Sep
Displayed time zone: Belfast change