Program - ICFP 2017

Sun 3 - Sat 9 September 2017 Oxford, United Kingdom

Filter

Sun 3 Sep

09:00 - 10:00: Tutorials - Morning tutorial session 1 at L5

09:00 - 10:00
Talk

Tutorial T1: Writing Verified Programs in CakeML

Ramana Kumar, Michael Norrish, Scott Owens, Magnus O. Myreen

09:00 - 09:10: Scheme 2017 - Session 0 at L4

09:00 - 09:10
Day opening

09:00 - 09:10: PLMW 2017 - Welcome at L1
Chair(s): Brigitte Pientka

09:00 - 09:10
Talk

Brigitte Pientka, Neelakantan R. Krishnaswami, Dan Licata

09:00 - 09:05: TyDe 2017 - Welcome at L2

09:00 - 09:05
Day opening

Sam Lindley, Brent Yorgey

09:00 - 09:10: HOPE 2017 - Welcome at L3

09:00 - 09:10
Day opening

François Pottier, Aleksandar Nanevski

09:05 - 10:00: TyDe 2017 - Invited talk at L2

09:05 - 10:00
Talk

Driving types into PHP

09:10 - 10:00: HOPE 2017 - Invited talk at L3

09:10 - 10:10
Talk

Invited Talk: Semantics of Effect Systems by Graded Monads

Shin-ya Katsumata

09:10 - 10:00: PLMW 2017 - Keynote at L1
Chair(s): Neelakantan R. Krishnaswami

09:10 - 10:00
Talk

09:10 - 10:10: Scheme 2017 - Session 1 at L4

09:10 - 10:10
Talk

Sam Tobin-Hochstadt

10:00 - 10:30: Catering - Sunday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Sunday coffee break 1

10:30 - 11:30: TyDe 2017 - Full papers 1 at L2

10:30 - 11:00
Talk

Generic packet descriptions: verified parsing and pretty printing of low-level data

Marcell van Geest, Wouter Swierstra

11:00 - 11:30
Talk

Structured asynchrony with algebraic effects

10:30 - 11:30: HOPE 2017 - Modular Semantics at L3

10:30 - 11:00
Talk

Higher-order Programming is an Effect

11:00 - 11:30
Talk

A monadic solution to the Cartwright-Felleisen-Wadler conjecture

Ohad Kammar, Dylan McDermott

10:30 - 11:30: Tutorials - Morning tutorial session 2 at L5

10:30 - 11:30
Talk

Tutorial T1: Writing Verified Programs in CakeML (part 2)

Ramana Kumar, Michael Norrish, Scott Owens, Magnus O. Myreen

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

10:30 - 11:00
Talk

A Few Frank Remarks

11:00 - 11:30
Talk

Compositional Compiler Correctness

10:30 - 11:30: Scheme 2017 - Session 2 at L4

10:30 - 11:15
Talk

Paper: Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation

11:15 - 11:30
Talk

Lightning Talk: Extending the LISP model from cons cells to triples, from trees to hypergraphs

Joe Corneli, Raymond Puzio

11:20 - 12:00: Catering - Sunday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Sunday coffee break 2

12:00 - 12:25: TyDe 2017 - Extended abstracts 1 at L2

12:00 - 12:25
Talk

Cogent⇑: giving systems engineers a stepping stone

12:00 - 12:30: Tutorials - Morning tutorial session 3 at L5

12:00 - 12:30
Talk

Tutorial T1: Writing Verified Programs in CakeML (part 3)

Ramana Kumar, Michael Norrish, Scott Owens, Magnus O. Myreen

12:00 - 12:30: HOPE 2017 - Rust at L3

12:00 - 12:30
Talk

RustBelt: Securing the Foundations of the Rust Programming Language

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer

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

12:00 - 12:30
Talk

Not How To Do Your PhD

Gabriel Scherer

12:00 - 12:30: Scheme 2017 - Session 3 at L4

12:00 - 12:30
Talk

Panel: Future of Scheme

François-René Rideau, Marc Feeley, Arthur Gleckler, Kathy Gray, Alaric Snell-Pym, Andy Wingo

12:25 - 14:00: Catering - Sunday lunch at Catering

12:25 - 14:00
Lunch

14:00 - 15:00: Tutorials - Afternoon tutorial session 1 at L5

14:00 - 15:00
Talk

Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL

Jasmin Blanchette, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

14:00 - 15:00: HOPE 2017 - Effects and Dependent Types at L3

14:00 - 14:30
Talk

Handling fibred algebraic effects

14:30 - 15:00
Talk

Only Control Effects and Dependent Types

Youyou Cong, William J. Bowman

14:00 - 15:00: TyDe 2017 - Full papers 2 at L2

14:00 - 14:30
Talk

Type safe Redis queries -- a case study of type-level programming in Haskell

Ting-Yan Lai, Tyng-Ruey Chuang, Shin-Cheng Mu

14:30 - 15:00
Talk

Type-directed diffing of structured data

Victor Cacciari Miraldo, Pierre-Evariste Dagand, Wouter Swierstra

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

14:00 - 14:30
Talk

14:30 - 15:00
Talk

Scala: Types in Theory & Practice

14:00 - 15:00: Scheme 2017 - Session 4 at L4

14:00 - 14:45
Talk

Paper: Toward Parallelizing Control-flow Analysis with Datalog

Thomas Gilray, Sidharth Kumar

14:45 - 15:00
Talk

Lightning: Gerbil on Gambit, as they say Racket on Chez

Dimitris Vyzovitis

14:50 - 15:30: Catering - Sunday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Sunday coffee break 3

15:30 - 16:20: Tutorials - Afternoon tutorial session 2 at L5

15:30 - 16:20
Talk

Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 2)

Jasmin Blanchette, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

15:30 - 16:30: HOPE 2017 - Effects at L3

15:30 - 16:00
Talk

Programming a Web Server with Algebraic Effects

16:00 - 16:30
Talk

Logical Relations for Algebraic Effects

Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, Filip Sieczkowski

15:30 - 16:20: TyDe 2017 - Extended abstracts 2 at L2

15:30 - 15:55
Talk

Kiko Fernandez-Reyes, Dave Clarke

15:55 - 16:20
Talk

On ringads and foldables

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

15:30 - 16:30
Talk

How to Write Papers and Give Talks That People Can Follow

15:30 - 16:30: Scheme 2017 - Session 5 at L4

15:30 - 16:15
Talk

Report: Status of the ongoing R7RS standardization process

Alaric Snell-Pym

16:15 - 16:30
Talk

Lightning: {lambda talk}

16:20 - 16:50: Catering - Sunday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Sunday coffee break 4

16:50 - 17:50: Tutorials - Afternoon tutorial session 3 at L5

16:50 - 17:50
Talk

Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 3)

Jasmin Blanchette, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel

16:50 - 17:40: TyDe 2017 - Extended abstracts 3 at L2

16:50 - 17:15
Talk

Type oriented programming for task based parallelism

Nick Brown, Ludovic Capelli, James Mark Bull

17:15 - 17:40
Talk

Type-directed reasoning for probabilistic, non-compositional resources

Edwin Brady, Kevin Hammond, Christopher Schwaab

16:50 - 17:40: HOPE 2017 - Monotonicity at L3

16:50 - 17:20
Talk

Recalling a Witness

Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy, Cédric Fournet

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

16:50 - 17:40
Talk

Panel Discussion: Careers in Programming Languages

Sam Staton, Richard A. Eisenberg, Andreas Rossberg, Daan Leijen, Amal Ahmed

16:50 - 17:50: Scheme 2017 - Session 6 at L4

16:50 - 17:40
Talk

17:40 - 17:50
Day closing

Mon 4 Sep

09:00 - 10:00: Keynotes and Reports - Monday Keynote at L1
Chair(s): Jeremy Gibbons

09:00 - 10:00
Talk

Compositional creativity: some principles for talking to computersKeynote

10:00 - 10:30: Catering - Monday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Monday coffee break 1

10:30 - 12:00: Research Papers - Art and Education at L1
Chair(s): Kathryn E. Gray

10:30 - 10:52
Talk

Super 8 Languages for Making Movies (Functional Pearl)

Leif Andersen, Stephen Chang, Matthias Felleisen

10:52 - 11:15
Talk

Testing and Debugging Functional Reactive Programming

Ivan Perez, Henrik Nilsson

11:15 - 11:37
Talk

Lock-Step Simulation Is Child's Play (Experience Report)

Joachim Breitner, Chris Smith

11:37 - 12:00
Talk

Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC

Benjamin Canou, Roberto Di Cosmo, Grégoire Henry

10:30 - 10:45: FSCD 2017 - Welcome at L2

10:30 - 10:45
Other

Welcome message

Sam Staton, Dale Miller

10:45 - 11:45: FSCD 2017 - Session 1 at L2

10:45 - 11:45
Talk

Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages

Alexandra Silva

12:00 - 13:00: Catering - Monday lunch at Catering

12:00 - 13:00
Lunch

13:00 - 14:30: Research Papers - Functional Programming Techniques at L1
Chair(s): Graham Hutton

13:00 - 13:22
Talk

Faster Coroutine Pipelines

13:22 - 13:45
Talk

A Pretty But Not Greedy Printer (Functional Pearl)

Jean-Philippe Bernardy

13:45 - 14:07
Talk

Generic Functional Parallel Algorithms: Scan and FFT

14:07 - 14:30
Talk

A Unified Approach to Solving Seven Programming Problems (Functional Pearl)

William E. Byrd, Michael Ballantyne, Gregory Rosenblatt, Matthew Might

13:00 - 14:30: FSCD 2017 - Session 2 at L2

13:00 - 13:30
Talk

Polynomial running times for polynomial-time oracle machines

Akitoshi Kawamura, Florian Steinberg

13:30 - 14:00
Talk

A Curry-Howard Approach to Church’s Synthesis

Colin Riba, Pierre Pradic

14:00 - 14:30
Talk

Streett Automata Model Checking of Higher-Order Recursion Schemes

Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada

14:30 - 15:00: Catering - Monday coffee break 2 at Catering

14:30 - 15:00
Coffee break

Monday coffee break 2

15:00 - 16:10: Research Papers - Applications at L1
Chair(s): Alexandra Silva

15:00 - 15:23
Talk

Prototyping a Query Compiler using Coq (Experience Report)

Joshua Auerbach, Martin Hirzel, Louis Mandel, Avraham Shinnar, Jerome Simeon

15:23 - 15:46
Talk

A Framework for Adaptive Differential Privacy

Daniel Winograd-Cort, Andreas Haeberlen, Aaron Roth, Benjamin C. Pierce

15:46 - 16:10
Talk

Symbolic Conditioning of Arrays in Probabilistic Programs

Praveen Narayanan, Chung-chieh Shan

15:00 - 16:00: FSCD 2017 - Session 3 at L2

15:00 - 15:30
Talk

Relating System F and λ2: A Case Study in Coq, Abella and Beluga

Jonas Kaiser, Brigitte Pientka, Gert Smolka

15:30 - 16:00
Talk

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL

Jasmin Blanchette, Mathias Fleury, Dmitriy Traytel

16:10 - 16:40: Catering - Monday coffee break 3 at Catering

16:10 - 16:40
Coffee break

Monday coffee break 3

16:40 - 18:10: Research Papers - Effects at L1
Chair(s): Ben Lippmeier

16:40 - 17:02
Talk

Abstracting Definitional Interpreters

David Darais, Nicholas Labich, Phúc C. Nguyễn, David Van Horn

17:02 - 17:25
Talk

On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control

Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar

17:25 - 17:47
Talk

Imperative Functional Programs That Explain Their Work

Wilmer Ricciotti, Jan Stolarek, Roly Perera, James Cheney

17:47 - 18:10
Talk

Effect-Driven QuickChecking of Compilers

Jan Midtgaard, Mathias Nygaard Justesen, Patrick Kasting, Flemming Nielson, Hanne Riis Nielson

16:40 - 18:10: FSCD 2017 - Session 4 at L2

16:40 - 17:10
Talk

A polynomial-time algorithm for the Lambek calculus with brackets of bounded order

Max Kanovich, Stepan Kuznetsov, Glyn Morrill, Andre Scedrov

17:10 - 17:40
Talk

A sequent calculus for semi-associativity

Noam Zeilberger

17:40 - 18:10
Talk

Combinatorial Flows and their Normalisation

Lutz Strassburger

18:10 - 18:20: Keynotes and Reports - Monday Closing Events at L1
Chair(s): Peter Thiemann

18:10 - 18:20
Day closing

Monday Announcements

18:30 - 20:30: Social Events - Welcome Reception at Foyer

18:30 - 20:30
Social Event

Welcome Reception

Tue 5 Sep

09:00 - 10:00: Keynotes and Reports - Tuesday Keynote at L1
Chair(s): Mark Jones

09:00 - 10:00
Talk

Assuring AIKeynote

John Launchbury

10:00 - 10:30: Catering - Tuesday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Tuesday coffee break 1

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

10:30 - 10:52
Talk

Persistence for the Masses: RRB-Vectors in a Systems Language

Juan Pedro Bolívar Puente

10:52 - 11:15
Talk

Verified Low-Level Programming Embedded in F*

Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy

11:15 - 11:37
Talk

Verifying Efficient Function Calls in CakeML

Scott Owens, Michael Norrish, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan

11:37 - 12:00
Talk

Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols

Geoffrey Mainland

10:30 - 11:30: FSCD 2017 - Session 5 at L2

10:30 - 11:30
Talk

Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses

11:30 - 12:00: FSCD 2017 - Session 6 at L2

11:30 - 12:00
Talk

Continuation Passing Style for Effect Handlers

Daniel Hillerström, Sam Lindley, Bob Atkey, KC Sivaramakrishnan

12:00 - 13:00: Catering - Tuesday lunch at Catering

12:00 - 13:00
Lunch

13:00 - 14:30: Research Papers - Foundations of Higher-Order Programming at L1
Chair(s): Gabriel Scherer

13:00 - 13:22
Talk

How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation

13:22 - 13:45
Talk

A Relational Logic for Higher-Order Programs

Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub

13:45 - 14:07
Talk

Foundations of Strong Call by Need

Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, Delia Kesner

14:07 - 14:30
Talk

No-Brainer CPS Conversion

Milo Davis, William Meehan, Olin Shivers

13:00 - 14:30: FSCD 2017 - Session 7 at L2

13:00 - 13:30
Talk

Confluence of an extension of Combinatory Logic by Boolean constants

13:30 - 14:00
Talk

Improving Rewriting Induction Approach for Proving Ground Confluence

Takahito Aoto, Yoshihito Toyama, Yuta Kimura

14:00 - 14:30
Talk

The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal type

14:30 - 15:00: Catering - Tuesday coffee break 2 at Catering

14:30 - 15:00
Coffee break

Tuesday coffee break 2

15:00 - 16:00: FSCD 2017 - Session 8 at L2

15:00 - 15:30
Talk

Is the optimal implementation inefficient? Elementarily not

Stefano Guerrini, Marco Solieri

15:30 - 16:00
Talk

Optimality and the Linear Substitution Calculus

Pablo Barenbaum, Eduardo Bonelli

15:00 - 16:10: Research Papers - Tools for Verification at L1
Chair(s): Nikhil Swamy

15:00 - 15:23
Talk

Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification

Joonwon Choi, Muralidaran Vijayaraghavan, Benjamin Sherman, Adam Chlipala, Arvind

15:23 - 15:46
Talk

SpaceSearch: A Library for Building and Verifying Solver-Aided Tools

Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, Zachary Tatlock

15:46 - 16:10
Talk

Local Refinement Typing

Benjamin Cosman, Ranjit Jhala

16:10 - 16:40: Catering - Tuesday coffee break 3 at Catering

16:10 - 16:40
Coffee break

Tuesday coffee break 3

16:40 - 17:50: Research Papers - Program Construction at L1
Chair(s): John Hughes

16:40 - 17:03
Talk

Compiling to Categories

17:03 - 17:26
Talk

Visitors Unchained

François Pottier

17:26 - 17:50
Talk

Staged Generic Programming

16:40 - 18:10: FSCD 2017 - Session 9 at L2

16:40 - 17:10
Talk

Generalized Refocusing: from Hybrid Strategies to Abstract Machines

Malgorzata Biernacka, Witold Charatonik, Klara Zielińska

17:10 - 17:40
Talk

Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or

Simon Castellan, Pierre Clairambault, Glynn Winskel

17:40 - 18:10
Talk

Refutation of Sallé's Longstanding Conjecture

Benedetto Intrigila, Giulio Manzonetto, Andrew Polonsky

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

17:50 - 18:20
Talk

Programming Contest Report

Wed 6 Sep

09:00 - 09:37: Student Research Competition - SRC Presentations at L1
Chair(s): Ilya Sergey

09:00 - 09:37
Awards

Student Research Competition: Finalist Presentations

09:00 - 10:00: FSCD 2017 - Session 10 at L2

09:00 - 10:00
Talk

Quantitative semantics for probabilistic programming

Christine Tasson

09:37 - 10:00: Research Papers - Domain-Specific Languages at L1
Chair(s): Martin Erwig

09:37 - 10:00
Talk

Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)

Vincent St-Amour, Daniel Feltey, Spencer P. Florence, Shu-Hung You, Robby Findler

10:00 - 10:30: Catering - Wednesday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Wednesday coffee break 1

10:30 - 12:00: Research Papers - Dependently Typed Programming at L1
Chair(s): Dan Licata

10:30 - 10:52
Talk

A Specification for Dependent Types in Haskell

Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, Richard A. Eisenberg

10:52 - 11:15
Talk

Parametric Quantifiers for Dependent Type Theory

Andreas Nuyts, Andrea Vezzosi, Dominique Devriese

11:15 - 11:37
Talk

Normalization by Evaluation for Sized Dependent Types

Andreas Abel, Andrea Vezzosi, Theo Winterhalter

11:37 - 12:00
Talk

A Metaprogramming Framework for Formal Verification

Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo De Moura

10:30 - 12:00: FSCD 2017 - Session 11 at L2

10:30 - 11:00
Talk

Displayed categories

Benedikt Ahrens, Peter Lefanu Lumsdaine

11:00 - 11:30
Talk

List Objects with Algebraic Structure

Marcelo Fiore, Philip Saville

11:30 - 12:00
Talk

There is only one notion of differentiation

Robin Cockett, Jean-Simon Lemay

12:00 - 13:00: Catering - Wednesday lunch at Catering

12:00 - 13:00
Lunch

Wednesday lunch

13:00 - 14:30: Research Papers - Contracts and Sessions at L1
Chair(s): Matthew Flatt

13:00 - 13:22
Talk

Chaperone Contracts for Higher-Order Sessions

Hernan Melgratti, Luca Padovani

13:22 - 13:45
Talk

Whip: Higher-Order Contracts for Modern Services

Lucas Waye, Christos Dimoulas, Stephen Chong

13:45 - 14:07
Talk

Manifest Sharing with Session Types

Stephanie Balzer, Frank Pfenning

14:07 - 14:30
Talk

Gradual Session Types

Atsushi Igarashi, Peter Thiemann, Vasco Vasconcelos, Philip Wadler

13:00 - 14:30: FSCD 2017 - Session 12 at L2

13:00 - 13:30
Talk

A Fibrational Framework for Substructural and Modal Logics

Dan Licata, Michael Shulman, Mitchell Riley

13:30 - 14:00
Talk

Dinaturality between syntax and semantics

14:00 - 14:30
Talk

Models of Type Theory Based on Moore Paths

Andrew Pitts, Ian Orton

14:30 - 15:00: Catering - Wednesday coffee break 2 at Catering

14:30 - 15:00
Coffee break

Wednesday coffee break 2

15:00 - 16:10: Research Papers - Integrating Static and Dynamic Typing at L1
Chair(s): Ronald Garcia

15:00 - 15:23
Talk

Theorems for Free for Free: Parametricity, With and Without Types

Amal Ahmed, Dustin Jamner, Jeremy G. Siek, Philip Wadler

15:23 - 15:46
Talk

On Polymorphic Gradual Typing

Yuu Igarashi, Taro Sekiyama, Atsushi Igarashi

15:46 - 16:10
Talk

Gradual Typing with Union and Intersection Types

Giuseppe Castagna, Victor Lanvin

15:00 - 16:00: FSCD 2017 - Session 13 at L2

15:00 - 15:30
Talk

Böhm Reduction in Infinitary Term Graph Rewriting Systems

15:30 - 16:00
Talk

Infinite Runs in Abstract Completion

Nao Hirokawa, aart Middeldorp, Christian Sternagel, Sarah Winkler

16:10 - 16:40: Catering - Wednesday coffee break 3 at Catering

16:10 - 16:40
Coffee break

Wednesday coffee break 3

16:40 - 17:50: Research Papers - Inference and Analysis at L1
Chair(s): Mark Jones

16:40 - 17:03
Talk

Constrained Type Families

J. Garrett Morris, Richard A. Eisenberg

17:03 - 17:26
Talk

Automating Sized-Type Inference for Complexity Analysis

Martin Avanzini, Ugo Dal Lago

17:26 - 17:50
Talk

Inferring Scope through Syntactic Sugar

Justin Pombrio, Shriram Krishnamurthi, Mitchell Wand

16:40 - 17:10: FSCD 2017 - Session 14 at L2

16:40 - 17:10
Talk

Negative Translations and Normal Modality

Tadeusz Litak, Miriam Polzer, Ulrich Rabenstein

17:10 - 17:20: FSCD 2017 - Termination and Complexity Competition 2017 at L2

17:10 - 17:20
Other

Termination and Complexity Competition 2017

Jürgen Giesl, Albert Rubio, Johannes Waldmann, Akihisa Yamada

17:20 - 18:10: FSCD 2017 - FSCD General Meeting at L2

17:20 - 18:10
Meeting

FSCD General Meeting

17:50 - 18:00: Student Research Competition - SRC Awards at L1
Chair(s): Ilya Sergey

17:50 - 18:00
Awards

Student Research Competition Awards

18:00 - 18:20: Keynotes and Reports - Wednesday Closing Events at L1

18:00 - 18:10
Talk

Program Chair's Report

18:10 - 18:20
Talk

ICFP 2018 Announcement

18:30 - 22:30: Social Events - Banquet at Weston Library

18:30 - 22:30
Social Event

Thu 7 Sep

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C1 at L6
Chair(s): Runhang Li

09:00 - 10:00
Other

Tutorial C1: Online Applications with Incremental

Yaron Minsky, Sebastian Funk

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C2 at L5
Chair(s): Runhang Li

09:00 - 10:00
Other

Tutorial C2: Extensible Effects: understanding them, implementing them, using them

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

09:00 - 10:00
Talk

Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (Invited Talk)

09:00 - 10:00: FSCD 2017 - Session 15 at L2

09:00 - 10:00
Talk

Type systems for the relational verification of higher order programs

09:00 - 09:05: ML 2017 - Welcome at L3
Chair(s): Sam Lindley

09:00 - 09:05
Day opening

09:00 - 09:10: FHPC 2017 - Welcome to FHPC'17 at L4

09:00 - 09:10
Day opening

Welcome to FHPC'17

Phil Trinder, Cosmin Oancea

09:05 - 10:00: ML 2017 - Invited talk at L3
Chair(s): Sam Lindley

09:05 - 10:00
Talk

State machines all the way down

09:10 - 10:10: FHPC 2017 - First Keynote at L4
Chair(s): Kevin Hammond

09:10 - 10:10
Talk

Haskell in the Datacentre

10:00 - 10:30: Catering - Thursday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Thursday coffee break 1

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C1 at L6

10:30 - 11:30
Talk

Tutorial C1: Online Applications with Incremental (part 2)

Yaron Minsky, Sebastian Funk

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C2 at L5

10:30 - 11:30
Talk

Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 2)

10:30 - 11:30: FHPC 2017 - Compilation at L4
Chair(s): Phil Trinder

10:30 - 11:00
Talk

From High-level Radio Protocol Specifications to Efficient Low-level Implementations via Partial Evaluation

Geoffrey Mainland, Siddhanathan Shanmugam

11:00 - 11:30
Talk

Destination-Passing Style for Efficient Memory Management

Amir Shaikhha, Andrew Fitzgibbon, Simon Peyton Jones, Dimitrios Vytiniotis

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

10:30 - 11:00
Talk

Algebraic Graphs with Class (Functional Pearl)

11:00 - 11:30
Talk

Packrats Parse in Packs

Mario Blažević, Jacques Légaré

10:30 - 11:59: FSCD 2017 - Session 16 at L2

10:30 - 11:00
Talk

Arrays and References in Resource Aware ML

Benjamin Lichtman, Jan Hoffmann

11:00 - 11:30
Talk

The Complexity of Principal Inhabitation

Andrej Dudenhefner, Jakob Rehof

11:30 - 11:59
Talk

Types as Resources for Classical Natural Deduction

Delia Kesner, Pierre Vial

10:30 - 11:45: ML 2017 - Types and modules at L3

10:30 - 10:55
Talk

Mergeable types

Gowtham Kaki, KC Sivaramakrishnan, Samodya Abeysiriwardane, Suresh Jagannathan

10:55 - 11:20
Talk

Tierless modules

Gabriel Radanne, Jérôme Vouillon

11:20 - 11:45
Talk

First-class subtypes

Jeremy Yallop, Stephen Dolan

11:20 - 12:00: Catering - Thursday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Thursday coffee break 2

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C1 at L6

12:00 - 12:30
Talk

Tutorial C1: Online Applications with Incremental (part 3)

Yaron Minsky, Sebastian Funk

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C2 at L5

12:00 - 12:30
Talk

Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 3)

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

12:00 - 12:30
Talk

Ode on a Random Urn (Functional Pearl)

Leonidas Lampropoulos, Antal Spector-Zabusky, Kenneth Foner

12:00 - 12:30: FHPC 2017 - Tools at L4
Chair(s): Cosmin Oancea

12:00 - 12:30
Talk

VisPar: Visualising dataflow graphs from the Par monad

Maximilian Algehed, Patrik Jansson

12:00 - 12:25: ML 2017 - Verification at L3

12:00 - 12:25
Talk

VOCAL -- a verified OCAml Library

Arthur Charguéraud, Jean-Christophe Filliatre, Mário Pereira, François Pottier

12:25 - 14:00: Catering - Thursday lunch at Catering

12:25 - 14:00
Lunch

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C3 at L5
Chair(s): Runhang Li

14:00 - 15:00
Other

Tutorial C3: Concurrent Programming with Effect Handlers

Daniel Hillerström, KC Sivaramakrishnan

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C4 at L6
Chair(s): Runhang Li

14:00 - 15:00
Talk

Tutorial C4: Git under the hood with OCaml

Romain Calascibetta

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

14:00 - 14:30
Demonstration

QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration)

Maximilian Algehed, Koen Claessen, Moa Johansson, Nicholas Smallbone

14:30 - 15:00
Talk

Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results

Rudy Braquehais, Colin Runciman

14:00 - 15:00: FHPC 2017 - Parallel Programming at L4
Chair(s): Geoffrey Mainland

14:00 - 14:30
Talk

In Search of a Map: using Program Slicing to Discover Potential Parallelism in Recursive Functions

Adam Barwell, Kevin Hammond

14:30 - 15:00
Talk

Strategies for Regular Segmented Reductions on GPU

Rasmus Wriedt Larsen, Troels Henriksen

14:00 - 15:15: ML 2017 - Programming language design at L3

14:00 - 14:25
Talk

Typer: an infix statically typed Lisp

Pierre Delaunay, Vincent Archambault-Bouffard, Stefan Monnier

14:25 - 14:50
Talk

Relational conversion for OCaml

Petr Lozov, Dmitri Boulytchev

14:50 - 15:15
Talk

Towards abductive functional programming

14:50 - 15:30: Catering - Thursday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Thursday coffee break 3

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C3 at L5

15:30 - 16:20
Talk

Tutorial C3: Concurrent Programming with Effect Handlers (part 2)

Daniel Hillerström, KC Sivaramakrishnan

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C4 at L6

15:30 - 16:20
Talk

Tutorial C4: Git under the hood with OCaml (part 2)

Romain Calascibetta

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

15:30 - 16:00
Talk

Using Coq to Write Fast and Correct Haskell

John Wiegley, Benjamin Delaware

16:00 - 16:30
Talk

A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq

Niki Vazou, Leonidas Lampropoulos, Jeff Polakow

15:30 - 16:30: FHPC 2017 - Demo Session at L4
Chair(s): Cosmin Oancea

15:30 - 15:59
Demonstration

Troels Henriksen

16:00 - 16:29
Demonstration

ParaFormance Demo: Democratizing Parallel Software Development

Christopher Brown, Kevin Hammond

16:30 - 16:50
Social Event

Break 16:30 - 16:50: Wine and Nibbles @ North Mezzanine

15:30 - 16:20: ML 2017 - Performance at L3

15:30 - 15:55
Talk

Making SML# a general-purpose high-performance language

Atsushi Ohori, Kenjiro Taura, Katsuhiro Ueno

15:55 - 16:20
Talk

Efficient representation of large, dynamic sequences in ML

Arthur Charguéraud, Mike Rainey

16:20 - 16:50: Catering - Thursday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Thursday coffee break 4

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C3 at L5

16:50 - 17:30
Talk

Tutorial C3: Concurrent Programming with Effect Handlers (part 3)

Daniel Hillerström, KC Sivaramakrishnan

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C4 at L6

16:50 - 17:30
Talk

Tutorial C4: Git under the hood with OCaml (part 3)

Romain Calascibetta

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

16:50 - 17:20
Talk

A Meta-EDSL for Distributed Web Applications

17:20 - 17:50
Talk

Composable Network Stacks and Remote Monads

Justin Dawson, Mark Grebe, Andy Gill

16:50 - 17:50: FHPC 2017 - Demo and Panel at L4
Chair(s): Phil Trinder

16:50 - 17:20
Demonstration

Ziria Demo: Wringing performance from high-level code

Siddhanathan Shanmugam, Geoffrey Mainland

17:20 - 17:50
Day closing

Panel Discussion: The challenges for Functional High Performance Computing

Geoffrey Mainland, Kevin Hammond, Simon Marlow

16:50 - 17:40: ML 2017 - Effects at L3

16:50 - 17:15
Talk

Effects without monads: non-determinism

17:15 - 17:40
Talk

Effectively tackling the awkward squad

Stephen Dolan, Spiros Eliopoulos, Daniel Hillerström, Anil Madhavapeddy, KC Sivaramakrishnan, Leo White

18:15 - 20:30: Social Events - Industry Reception at Ashmolean Museum

18:15 - 20:30
Social Event

Industry Reception

Fri 8 Sep

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C5 at L6
Chair(s): Runhang Li

09:00 - 10:00
Talk

Tutorial C5: Teaching Functional Programming

Michael Sperber

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C6 at L5
Chair(s): Runhang Li

09:00 - 10:00
Talk

Tutorial C6: Transducers in Practice

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

09:00 - 10:00
Talk

Algorithmic Music in Haskell (Invited Talk)

09:00 - 09:10: OCaml 2017 - Opening at L3

09:00 - 09:05
Day opening

Gabriel Scherer

09:00 - 09:10: Erlang 2017 - Opening & Welcome at L4

09:00 - 09:10
Day opening

Opening & Welcome

09:10 - 10:00: Erlang 2017 - Keynote Invited Talk at L4

09:10 - 10:00
Talk

09:10 - 10:10: OCaml 2017 - Talk session 1 at L3

09:05 - 09:40
Talk

Invited talk: new contributors

David Allsopp, Florian Angeletti, Sébastien Hinderer

09:40 - 10:05
Talk

The State of the OCaml Platform: September 2017

Anil Madhavapeddy

10:00 - 10:30: Catering - Friday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Friday coffee break 1

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C5 at L6

10:30 - 11:30
Talk

Tutorial C5: Teaching Functional Programming (part 2)

Michael Sperber

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C6 at L5

10:30 - 11:30
Talk

Tutorial C6: Transducers in Practice (part 2)

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

10:30 - 11:00
Talk

Well-Typed Music Does Not Sound Wrong (Experience Report)

Dmitrij Szamozvancev, Michael Gale

11:00 - 11:30
Talk

Back to the Future: Time Travel in FRP

10:30 - 11:20: Erlang 2017 - Session 2 at L4

10:30 - 10:55
Talk

Construction and Formal Verification of a Fault-Tolerant Distributed Mutual Exclusion Algorithm

Evgeniy Shishkin

DOI File Attached

10:55 - 11:20
Talk

Towards an Isabelle/HOL Formalisation of Core Erlang

Joseph Harrison

10:30 - 11:30: OCaml 2017 - Talk session 2 at L3

10:30 - 10:50
Talk

Owl: A General-Purpose Numerical Library in OCaml

Link to publication Pre-print

10:50 - 11:10
Talk

Extending OCaml's open

Runhang Li, Jeremy Yallop

Link to publication Pre-print

11:10 - 11:30
Talk

Genspio: Generating Shell Phrases In OCaml

Sebastien Mondet

11:20 - 12:00: Catering - Friday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Friday coffee break 2

11:35 - 12:30: OCaml 2017 - Poster session at L3

11:35 - 11:45
Talk

Flash poster presentation

11:45 - 12:30
Talk

mSAT: An OCaml SAT Solver

Link to publication

11:45 - 12:30
Talk

Jbuilder: a modern approach to OCaml development

Jeremie Dimino, Mark Shinwell

11:45 - 12:30
Talk

Tyre – Typed Regular Expressions

Gabriel Radanne

Link to publication

11:45 - 12:30
Talk

ocamli: Interpreted OCaml

John Whitington

Link to publication

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C5 at L6

12:00 - 12:30
Talk

Tutorial C5: Teaching Functional Programming (part 3)

Michael Sperber

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C6 at L5

12:00 - 12:30
Talk

Tutorial C6: Transducers in Practice (part 3)

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

12:00 - 12:30
Talk

The Linearity Monad

Jennifer Paykin, Steve Zdancewic

12:00 - 12:25: Erlang 2017 - Session 3 at L4

12:00 - 12:25
Talk

Erlang and Elixir development news

12:25 - 14:00: Catering - Friday lunch at Catering

12:25 - 14:00
Lunch

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C7 at L6
Chair(s): Runhang Li

14:00 - 15:00
Talk

Tutorial C7: Owl - Data Science in OCaml

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C8 at L5
Chair(s): Runhang Li

14:00 - 15:00
Talk

Tutorial C8: GraphQL Servers in OCaml

Andreas Garnæs

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

14:00 - 14:30
Talk

Elaboration on Functional Dependencies

Georgios Karachalias, Tom Schrijvers

14:30 - 15:00
Talk

Quantified Class Constraints

Gert-Jan Bottu, Georgios Karachalias, Tom Schrijvers, Bruno C. d. S. Oliveira, Philip Wadler

14:00 - 14:50: Erlang 2017 - Session 4 at L4

14:00 - 14:25
Talk

Distributed Memory Architecture for High-Level Synthesis of Embedded Controllers from Erlang

Kagumi Azuma, Nagisa Ishiura, Nobuaki Yoshida, Hiroyuki Kanbara

14:25 - 14:50
Talk

Structuring Erlang BEAM control flow

Dániel Lukács, Melinda Toth

14:00 - 15:00: OCaml 2017 - Talk session 3 at L3

14:00 - 14:20
Talk

ROTOR: First Steps Towards a Refactoring Tool for OCaml

Reuben N. S. Rowe, Simon Thompson

Link to publication

14:20 - 14:40
Talk

A memory model for multicore OCaml

Stephen Dolan, KC Sivaramakrishnan

Link to publication

14:40 - 15:00
Talk

Bioinformatics, The Typed Tagless Final Way

Sebastien Mondet

14:50 - 15:30: Catering - Friday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Friday coffee break 3

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C7 at L6

15:30 - 16:20
Talk

Tutorial C7: Owl - Data Science in OCaml (part 2)

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C8 at L5

15:30 - 16:20
Talk

Tutorial C8: GraphQL Servers in OCaml (part 2)

Andreas Garnæs

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

15:30 - 16:00
Talk

Hardware Software Co-Design in Haskell

Markus Aronsson, Mary Sheeran

16:00 - 16:30
Talk

Streaming Irregular Arrays

Robert Clifton-Everest, Trevor L. McDonell, Manuel Chakravarty, Gabriele Keller

15:30 - 16:20: Erlang 2017 - Session 5 at L4

15:30 - 15:55
Talk

The Shared-Memory Interferences of Erlang/OTP Built-ins

Stavros Aronis, Kostis Sagonas

15:55 - 16:20
Talk

Towards Change-driven Testing

Viktória Fördős, István Bozó, Melinda Toth

15:30 - 16:30: OCaml 2017 - Talk session 4 at L3

15:30 - 15:50
Talk

A B-tree library for OCaml

Link to publication

15:50 - 16:10
Talk

Wodan: a pure OCaml, flash-aware filesystem library

Gabriel de Perthuis

Link to publication

16:10 - 16:30
Talk

Tezos: the OCaml Crypto-Ledger

Benjamin Canou, Grégoire Henry, Pierre Chambart, Fabrice Le Fessant, Arthur BREITMAN

16:20 - 16:50: Catering - Friday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Friday coffee break 4

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C7 at L6

16:50 - 17:30
Talk

Tutorial C7: Owl - Data Science in OCaml (part 3)

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C8 at L5

16:50 - 17:30
Talk

Tutorial C8: GraphQL Servers in OCaml (part 3)

Andreas Garnæs

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

16:50 - 17:20
Talk

Improving STM Performance with Transactional Structs

Ryan Yates, Michael Scott

17:20 - 17:50
Talk

Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping

Chao-Hong Chen, Vikraman Choudhury, Ryan R. Newton

16:50 - 17:50: Erlang 2017 - Session 6 at L4

16:50 - 17:20
Talk

eAOP - An Aspect Oriented Programming Framework for Erlang

Ian Cassar, Adrian Francalanza, Luca Aceto, Anna Ingolfsdottir

17:20 - 17:50
Talk

In medias res: WIP discussion

16:50 - 17:40: OCaml 2017 - Talk session 5 at L3

17:00 - 17:20
Talk

Component-based Program Synthesis in OCaml

Zhanpeng Liang, Kanae Tsushima

Link to publication

17:20 - 17:40
Talk

Testing with Crowbar

Stephen Dolan, Mindy Preston

Sat 9 Sep

09:00 - 09:10: FARM 2017 - Introduction at L3

09:00 - 09:10
Day opening

Michael Sperber, Jean Bresson

09:00 - 10:10: HIW 2017 - State of GHC at L1
Chair(s): Richard A. Eisenberg

09:00 - 09:30
Talk

Progress on GHC

Simon Peyton Jones

09:30 - 10:00
Talk

GHC Infrastructure Update and Discussion

10:00 - 10:10
Talk

Getting Ready for Hadrian

Andrey Mokhov, Zhen Zhang, Ben Gamari, Neil Mitchell

09:10 - 10:00: CUFP 2017 - CUFP Talks 1 at L2

09:10 - 09:35
Talk

Keynote: Are We There Yet?

09:35 - 10:00
Talk

Bonsai: a DSL for serverless firm real-time decisioning

Jeremie Lasalle-Ratelle

09:10 - 10:00: FARM 2017 - Session 1: Papers/Demos at L3
Chair(s): Jean Bresson

09:10 - 09:40
Talk

A Categorial Grammar for Music and Its Use in Automatic Melody Generation

09:40 - 10:00
Demonstration

Demo — Representation of Musical Notation in Haskell

10:00 - 10:30: Catering - Saturday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Saturday coffee break 1

10:30 - 11:20: CUFP 2017 - CUFP Talks 2 at L2

10:30 - 10:55
Talk

Interfacing OCaml and Rust: picking the right tool for the job

Joris Giovannangeli

10:55 - 11:20
Talk

Distributed load testing with MZBench

10:30 - 11:30: HIW 2017 - Compiling to LLVM at L1
Chair(s): Jan Stolarek

10:30 - 10:55
Talk

Native Support for Explicit Stacks in LLVM

Kavon Farvardin, Simon Peyton Jones

10:55 - 11:20
Talk

SimplexHC: Lowering High-Level Haskell to Imperative IR

11:20 - 11:30
Talk

Lightning Talk Slot #1

10:30 - 11:30: FARM 2017 - Session 2: Papers/Demos at L3
Chair(s): Ivan Perez

10:30 - 10:50
Demonstration

Demo — African Polyphony and Polyrhythm

10:50 - 11:10
Demonstration

Demo — Vivid: Sound Synthesis with Haskell and SuperCollider

11:10 - 11:40
Talk

GALE: A Functional Graphic Adventure Library and Engine

11:20 - 12:00: Catering - Saturday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Saturday coffee break 2

12:00 - 12:25: CUFP 2017 - CUFP Talks 3 at L2

12:00 - 12:25
Talk

Gens N' Roses: Appetite for Reduction

12:00 - 12:25: HIW 2017 - Constraints at L1
Chair(s): Ben Gamari

12:00 - 12:25
Talk

On Unsatisfiability

J. Garrett Morris

12:00 - 12:30: FARM 2017 - Session 3: Paper at L3
Chair(s): Michael Sperber

12:00 - 12:30
Talk

Modelling the Way Mathematics Is Actually Done

Joe Corneli, Ursula Martin, Dave Murray-Rust, Alison Pease, Raymond Puzio, Gabriela Rino Nesin

12:25 - 14:00: Catering - Saturday lunch at Catering

12:25 - 14:00
Lunch

14:00 - 14:50: CUFP 2017 - CUFP Talks 4 at L2

14:00 - 14:25
Talk

Formally Verifying a Smart-Contract Language Implementation with Isabelle

14:25 - 14:50
Talk

Haskell games and apps for iOS and Android

14:00 - 15:00: FARM 2017 - Session 4: Tutorial at L3
Chair(s): Jean Bresson

14:00 - 15:00
Talk

FAUST Tutorial for Functional Programmers

Yann Orlarey, Stéphane Letz, Dominique Fober, Romain Michon

14:00 - 15:00: HIW 2017 - Working in Core at L1
Chair(s): Adam Gundry

14:00 - 14:25
Talk

Why GHC Core and Linear Logic Should be Best Friends

Carter Schonwald, Joel Burget

14:25 - 14:50
Talk

Demand Analysis vs. Call Arity

14:50 - 15:00
Talk

Lightning Talk Slot #2

14:50 - 15:30: Catering - Saturday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Saturday coffee break 3

15:30 - 16:20: CUFP 2017 - CUFP Talks 5 at L2

15:30 - 15:55
Talk

Using Haskell to run a datacenter

15:55 - 16:20
Talk

Functional Facades over Legacy Code

Nicholas Cowle, Robin Kay

15:30 - 16:20: FARM 2017 - Session 5: Demos at L3
Chair(s): David Janin

15:30 - 15:50
Demonstration

Demo — The Arpeggigon: A Functional Reactive Musical Automaton

15:50 - 16:10
Demonstration

Demo — Ait: A Concatenative Language for Creative Programming

Stian Veum Møllersen

15:30 - 16:30: HIW 2017 - Tool Support at L1
Chair(s): Wren Romano

15:30 - 15:55
Talk

IDE Support in GHC

15:55 - 16:20
Talk

Tracking GHC Performance

Mathieu Boespflug, Manuel Chakravarty

16:20 - 16:30
Talk

Lightning Talk Slot #3

16:20 - 16:50: Catering - Saturday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Saturday coffee break 4

16:50 - 17:50: HIW 2017 - All Broken Up at L1
Chair(s): Bartosz Nitka

16:50 - 17:15
Talk

An Experiment in Fragment-Based Code Distribution

Philipp Schuster

17:15 - 17:50
Talk

Lightning Talk Slot #4

16:50 - 17:40: CUFP 2017 - CUFP Talks 6 at L2

16:50 - 17:15
Talk

Building the largest payment sandbox on a tiny machine

17:15 - 17:40
Talk

Using Functional Programming to Accelerate Translational Research at Pfizer

16:50 - 17:40: FARM 2017 - Session 6: Papers/Demos at L3
Chair(s): Henrik Nilsson

16:50 - 17:20
Talk

Unified Media Programming: An Algebraic Approach

Simon Archipoff, David Janin

17:20 - 17:40
Demonstration

Demo — Octopus: A High-Level Fast 3D Animation Language

Simon Archipoff, David Janin

19:30 - 22:00: Social Events - FARM Performance Evening at Old Fire Station

19:30 - 22:00
Social Event

FARM Evening Of Algorithmic Arts

Sun 3 Sep 2017


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
Catering													Catering Sunday coffee break 1 10:00 - 10:30																Catering Sunday coffee break 2 11:20 - 12:00													Catering Sunday lunch 12:25 - 14:00																													Catering Sunday coffee break 3 14:50 - 15:30																		Catering Sunday coffee break 4 16:20 - 16:50
L1	PLMW 2017 Welcome 09:00 - 09:10		PLMW 2017 Keynote 09:10 - 10:00																PLMW 2017 Session 1 10:30 - 11:30																		PLMW 2017 Session 2 12:00 - 12:30																								PLMW 2017 Session 3 14:00 - 15:00																		PLMW 2017 Session 4 15:30 - 16:30																PLMW 2017 Session 5 16:50 - 17:40
L2	TyDe 2017 Welcome 09:00 - 09:05	TyDe 2017 Invited talk 09:05 - 10:00																	TyDe 2017 Full papers 1 10:30 - 11:30																		TyDe 2017 Extended abstracts 1 12:00 - 12:25																								TyDe 2017 Full papers 2 14:00 - 15:00																		TyDe 2017 Extended abstracts 2 15:30 - 16:20																TyDe 2017 Extended abstracts 3 16:50 - 17:40
L3	HOPE 2017 Welcome 09:00 - 09:10		HOPE 2017 Invited talk 09:10 - 10:00																HOPE 2017 Modular Semantics 10:30 - 11:30																		HOPE 2017 Rust 12:00 - 12:30																								HOPE 2017 Effects and Dependent Types 14:00 - 15:00																		HOPE 2017 Effects 15:30 - 16:30																HOPE 2017 Monotonicity 16:50 - 17:40
L4	Scheme 2017 Session 0 09:00 - 09:10		Scheme 2017 Session 1 09:10 - 10:10																Scheme 2017 Session 2 10:30 - 11:30																		Scheme 2017 Session 3 12:00 - 12:30																								Scheme 2017 Session 4 14:00 - 15:00																		Scheme 2017 Session 5 15:30 - 16:30																Scheme 2017 Session 6 16:50 - 17:50
L5	Tutorials Morning tutorial session 1 09:00 - 10:00																		Tutorials Morning tutorial session 2 10:30 - 11:30																		Tutorials Morning tutorial session 3 12:00 - 12:30																								Tutorials Afternoon tutorial session 1 14:00 - 15:00																		Tutorials Afternoon tutorial session 2 15:30 - 16:20																Tutorials Afternoon tutorial session 3 16:50 - 17:50

Mon 4 Sep 2017


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						19:00						30						20:00						30
Catering													Catering Monday coffee break 1 10:00 - 10:30																								Catering Monday lunch 12:00 - 13:00																														Catering Monday coffee break 2 14:30 - 15:00																				Catering Monday coffee break 3 16:10 - 16:40
Foyer																																																																	Social Events Welcome Reception 18:30 - 20:30
L1	Keynotes and Reports Monday Keynote 09:00 - 10:00																		Research Papers Art and Education 10:30 - 12:00																														Research Papers Functional Programming Techniques 13:00 - 14:30																								Research Papers Applications 15:00 - 16:10																				Research Papers Effects 16:40 - 18:10																		Keynotes and Reports Monday Closing Events 18:10 - 18:20
L2																			FSCD 2017 Welcome 10:30 - 10:45			FSCD 2017 Session 1 10:45 - 11:45																											FSCD 2017 Session 2 13:00 - 14:30																								FSCD 2017 Session 3 15:00 - 16:00																				FSCD 2017 Session 4 16:40 - 18:10

Tue 5 Sep 2017


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
Catering													Catering Tuesday coffee break 1 10:00 - 10:30																								Catering Tuesday lunch 12:00 - 13:00																														Catering Tuesday coffee break 2 14:30 - 15:00																				Catering Tuesday coffee break 3 16:10 - 16:40
L1	Keynotes and Reports Tuesday Keynote 09:00 - 10:00																		Research Papers Low-level and Systems Programming 10:30 - 12:00																														Research Papers Foundations of Higher-Order Programming 13:00 - 14:30																								Research Papers Tools for Verification 15:00 - 16:10																				Research Papers Program Construction 16:40 - 17:50														Keynotes and Reports Tuesday Closing Events 17:50 - 18:20
L2																			FSCD 2017 Session 5 10:30 - 11:30												FSCD 2017 Session 6 11:30 - 12:00																		FSCD 2017 Session 7 13:00 - 14:30																								FSCD 2017 Session 8 15:00 - 16:00																				FSCD 2017 Session 9 16:40 - 18:10

Wed 6 Sep 2017


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						19:00						30						20:00						30						21:00						30						22:00						30
Catering													Catering Wednesday coffee break 1 10:00 - 10:30																								Catering Wednesday lunch 12:00 - 13:00																														Catering Wednesday coffee break 2 14:30 - 15:00																				Catering Wednesday coffee break 3 16:10 - 16:40
L1	Student Research Competition SRC Presentations 09:00 - 09:37							Research Papers Domain-Specific Languages 09:37 - 10:00											Research Papers Dependently Typed Programming 10:30 - 12:00																														Research Papers Contracts and Sessions 13:00 - 14:30																								Research Papers Integrating Static and Dynamic Typing 15:00 - 16:10																				Research Papers Inference and Analysis 16:40 - 17:50														Student Research Competition SRC Awards 17:50 - 18:00		Keynotes and Reports Wednesday Closing Events 18:00 - 18:20				Keynotes and Reports 18:10 - 18:20
L2	FSCD 2017 Session 10 09:00 - 10:00																		FSCD 2017 Session 11 10:30 - 12:00																														FSCD 2017 Session 12 13:00 - 14:30																								FSCD 2017 Session 13 15:00 - 16:00																				FSCD 2017 Session 14 16:40 - 17:10						FSCD 2017 Termination and Complexity Competition 2017 17:10 - 17:20		FSCD 2017 FSCD General Meeting 17:20 - 18:10
Weston Library																																																																	Social Events Banquet 18:30 - 22:30

Thu 7 Sep 2017


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						19:00						30						20:00						30
Ashmolean Museum																																																																	Social Events Industry Reception 18:15 - 20:30
Catering													Catering Thursday coffee break 1 10:00 - 10:30																Catering Thursday coffee break 2 11:20 - 12:00													Catering Thursday lunch 12:25 - 14:00																													Catering Thursday coffee break 3 14:50 - 15:30																		Catering Thursday coffee break 4 16:20 - 16:50
L1	Haskell 2017 Day 1, Session 1 09:00 - 10:00																		Haskell 2017 Day 1, Session 2 10:30 - 11:30																		Haskell 2017 Day 1, Session 3 12:00 - 12:30																								Haskell 2017 Day 1, Session 4 14:00 - 15:00																		Haskell 2017 Day 1, Session 5 15:30 - 16:30																Haskell 2017 Day 1, Session 6 16:50 - 17:50
L2	FSCD 2017 Session 15 09:00 - 10:00																		FSCD 2017 Session 16 10:30 - 11:59
L3	ML 2017 Welcome 09:00 - 09:05	ML 2017 Invited talk 09:05 - 10:00																	ML 2017 Types and modules 10:30 - 11:45																		ML 2017 Verification 12:00 - 12:25																								ML 2017 Programming language design 14:00 - 15:15																		ML 2017 Performance 15:30 - 16:20																ML 2017 Effects 16:50 - 17:40
L4	FHPC 2017 Welcome to FHPC'17 09:00 - 09:10		FHPC 2017 First Keynote 09:10 - 10:10																FHPC 2017 Compilation 10:30 - 11:30																		FHPC 2017 Tools 12:00 - 12:30																								FHPC 2017 Parallel Programming 14:00 - 15:00																		FHPC 2017 Demo Session 15:30 - 16:30																FHPC 2017 Demo and Panel 16:50 - 17:50
L5	CUFP 2017 CUFP Tutorials C2 09:00 - 10:00																		CUFP 2017 CUFP Tutorials C2 10:30 - 11:30																		CUFP 2017 CUFP Tutorials C2 12:00 - 12:30																								CUFP 2017 CUFP Tutorials C3 14:00 - 15:00																		CUFP 2017 CUFP Tutorials C3 15:30 - 16:20																CUFP 2017 CUFP Tutorials C3 16:50 - 17:30
L6	CUFP 2017 CUFP Tutorials C1 09:00 - 10:00																		CUFP 2017 CUFP Tutorials C1 10:30 - 11:30																		CUFP 2017 CUFP Tutorials C1 12:00 - 12:30																								CUFP 2017 CUFP Tutorials C4 14:00 - 15:00																		CUFP 2017 CUFP Tutorials C4 15:30 - 16:20																CUFP 2017 CUFP Tutorials C4 16:50 - 17:30

Fri 8 Sep 2017


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
Catering													Catering Friday coffee break 1 10:00 - 10:30																Catering Friday coffee break 2 11:20 - 12:00													Catering Friday lunch 12:25 - 14:00																													Catering Friday coffee break 3 14:50 - 15:30																		Catering Friday coffee break 4 16:20 - 16:50
L1	Haskell 2017 Day 2, Session 1 09:00 - 10:00																		Haskell 2017 Day 2, Session 2 10:30 - 11:30																		Haskell 2017 Day 2, Session 3 12:00 - 12:30																								Haskell 2017 Day 2, Session 4 14:00 - 15:00																		Haskell 2017 Day 2, Session 5 15:30 - 16:30																Haskell 2017 Day 2, Session 6 16:50 - 17:50
L3	OCaml 2017 Opening 09:00 - 09:10		OCaml 2017 Talk session 1 09:10 - 10:10																OCaml 2017 Talk session 2 10:30 - 11:30													OCaml 2017 Poster session 11:35 - 12:30																													OCaml 2017 Talk session 3 14:00 - 15:00																		OCaml 2017 Talk session 4 15:30 - 16:30																OCaml 2017 Talk session 5 16:50 - 17:40
L4	Erlang 2017 Opening & Welcome 09:00 - 09:10		Erlang 2017 Keynote Invited Talk 09:10 - 10:00																Erlang 2017 Session 2 10:30 - 11:20																		Erlang 2017 Session 3 12:00 - 12:25																								Erlang 2017 Session 4 14:00 - 14:50																		Erlang 2017 Session 5 15:30 - 16:20																Erlang 2017 Session 6 16:50 - 17:50
L5	CUFP 2017 CUFP Tutorials C6 09:00 - 10:00																		CUFP 2017 CUFP Tutorials C6 10:30 - 11:30																		CUFP 2017 CUFP Tutorials C6 12:00 - 12:30																								CUFP 2017 CUFP Tutorials C8 14:00 - 15:00																		CUFP 2017 CUFP Tutorials C8 15:30 - 16:20																CUFP 2017 CUFP Tutorials C8 16:50 - 17:30
L6	CUFP 2017 CUFP Tutorials C5 09:00 - 10:00																		CUFP 2017 CUFP Tutorials C5 10:30 - 11:30																		CUFP 2017 CUFP Tutorials C5 12:00 - 12:30																								CUFP 2017 CUFP Tutorials C7 14:00 - 15:00																		CUFP 2017 CUFP Tutorials C7 15:30 - 16:20																CUFP 2017 CUFP Tutorials C7 16:50 - 17:30

Sat 9 Sep 2017


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						19:00						30						20:00						30						21:00						30						22:00						30
Catering													Catering Saturday coffee break 1 10:00 - 10:30																Catering Saturday coffee break 2 11:20 - 12:00													Catering Saturday lunch 12:25 - 14:00																													Catering Saturday coffee break 3 14:50 - 15:30																		Catering Saturday coffee break 4 16:20 - 16:50
L1	HIW 2017 State of GHC 09:00 - 10:10																		HIW 2017 Compiling to LLVM 10:30 - 11:30																		HIW 2017 Constraints 12:00 - 12:25																								HIW 2017 Working in Core 14:00 - 15:00																		HIW 2017 Tool Support 15:30 - 16:30																HIW 2017 All Broken Up 16:50 - 17:50
L2	CUFP 2017 09:00 - 09:10		CUFP 2017 CUFP Talks 1 09:10 - 10:00																CUFP 2017 CUFP Talks 2 10:30 - 11:20																		CUFP 2017 CUFP Talks 3 12:00 - 12:25																								CUFP 2017 CUFP Talks 4 14:00 - 14:50																		CUFP 2017 CUFP Talks 5 15:30 - 16:20																CUFP 2017 CUFP Talks 6 16:50 - 17:40
L3	FARM 2017 Introduction 09:00 - 09:10		FARM 2017 Session 1: Papers/Demos 09:10 - 10:00																FARM 2017 Session 2: Papers/Demos 10:30 - 11:30																		FARM 2017 Session 3: Paper 12:00 - 12:30																								FARM 2017 Session 4: Tutorial 14:00 - 15:00																		FARM 2017 Session 5: Demos 15:30 - 16:20