Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
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:00 - 09:05
WelcomeTyDe at L2
09:00
5m
Day opening
Welcome
TyDe
Sam Lindley University of Edinburgh, UK, Brent Yorgey Hendrix College
09:00 - 09:10
WelcomeHOPE at L3
09:00
10m
Day opening
Welcome
HOPE
C: François Pottier Inria, France, C: Aleksandar Nanevski IMDEA Software Institute
09:00 - 09:10
Session 0Scheme at L4
09:00
10m
Day opening
Welcome
Scheme

09:00 - 10:00
Morning tutorial session 1Tutorials at L5
09:00
60m
Talk
Tutorial T1: Writing Verified Programs in CakeML
Tutorials
P: Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, P: Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, P: Scott Owens University of Kent, UK, P: Magnus O. Myreen Chalmers University of Technology, Sweden
09:05 - 10:00
Invited talkTyDe at L2
09:05
55m
Talk
Driving types into PHP
TyDe
Andrew Kennedy Facebook London
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
09:10 - 10:00
Invited talkHOPE at L3
09:10
60m
Talk
Invited Talk: Semantics of Effect Systems by Graded Monads
HOPE
Shin-ya Katsumata National Institute of Informatics
09:10 - 10:10
Session 1Scheme at L4
09:10
60m
Talk
Keynote
Scheme
Sam Tobin-Hochstadt Indiana University
10:00 - 10:30
Sunday coffee break 1Catering at Catering
10:00
30m
Coffee break
Sunday coffee break 1
Catering

10:30 - 11:30
Session 1PLMW at L1
10:30
30m
Talk
A Few Frank Remarks
PLMW
11:00
30m
Talk
Compositional Compiler Correctness
PLMW
Amal Ahmed Northeastern University, USA
File Attached
10:30 - 11:30
Full papers 1TyDe at L2
10:30
30m
Talk
Generic packet descriptions: verified parsing and pretty printing of low-level data
TyDe
Marcell van Geest Utrecht University, Wouter Swierstra University of Utrecht
11:00
30m
Talk
Structured asynchrony with algebraic effects
TyDe
Daan Leijen Microsoft Research
10:30 - 11:30
Modular SemanticsHOPE at L3
10:30
30m
Talk
Higher-order Programming is an Effect
HOPE
File Attached
11:00
30m
Talk
A monadic solution to the Cartwright-Felleisen-Wadler conjecture
HOPE
Ohad Kammar University of Oxford, UK, Dylan McDermott University of Cambridge
File Attached
10:30 - 11:30
Morning tutorial session 2Tutorials at L5
10:30
60m
Talk
Tutorial T1: Writing Verified Programs in CakeML (part 2)
Tutorials
P: Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, P: Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, P: Scott Owens University of Kent, UK, P: Magnus O. Myreen Chalmers University of Technology, Sweden
11:20 - 12:00
Sunday coffee break 2Catering at Catering
11:20
40m
Coffee break
Sunday coffee break 2
Catering

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
12:00 - 12:25
Extended abstracts 1TyDe at L2
12:00
25m
Talk
Cogent⇑: giving systems engineers a stepping stone
TyDe
Zilin Chen UNSW, Australia
12:00 - 12:30
RustHOPE at L3
12:00
30m
Talk
RustBelt: Securing the Foundations of the Rust Programming Language
HOPE
Ralf Jung MPI-SWS, Germany, Jacques-Henri Jourdan MPI-SWS, Germany, Robbert Krebbers Delft University of Technology, Netherlands, Derek Dreyer MPI-SWS
12:00 - 12:30
Session 3Scheme at L4
12:00
30m
Talk
Panel: Future of Scheme
Scheme
François-René Rideau , Marc Feeley Université de Montréal, Arthur Gleckler SRFI Editor, Kathy Gray , Alaric Snell-Pym , Andy Wingo Igalia, S.L.
12:00 - 12:30
Morning tutorial session 3Tutorials at L5
12:00
30m
Talk
Tutorial T1: Writing Verified Programs in CakeML (part 3)
Tutorials
P: Ramana Kumar Data61 at CSIRO, Australia / UNSW, Australia, P: Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia, P: Scott Owens University of Kent, UK, P: Magnus O. Myreen Chalmers University of Technology, Sweden
12:25 - 14:00
Sunday lunchCatering at Catering
12:25
1h35m
Lunch
Sunday lunch
Catering

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
14:00 - 15:00
Full papers 2TyDe at L2
14:00
30m
Talk
Type safe Redis queries -- a case study of type-level programming in Haskell
TyDe
Ting-Yan Lai Institute of Information Science, Academia Sinica, Tyng-Ruey Chuang Institute of Information Science, Academia Sinica, Shin-Cheng Mu Academia Sinica, Taiwan
14:30
30m
Talk
Type-directed diffing of structured data
TyDe
Victor Cacciari Miraldo University of Utrecht, Pierre-Evariste Dagand LIP6/CNRS , Wouter Swierstra University of Utrecht
14:00 - 15:00
Effects and Dependent TypesHOPE at L3
14:00
30m
Talk
Handling fibred algebraic effects
HOPE
Danel Ahman University of Edinburgh
14:30
30m
Talk
Only Control Effects and Dependent Types
HOPE
Youyou Cong Ochanomizu University, William J. Bowman Northeastern University
14:00 - 15:00
Afternoon tutorial session 1Tutorials at L5
14:00
60m
Talk
Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL
Tutorials
P: Jasmin Blanchette Vrije Universiteit Amsterdam, P: Andreas Lochbihler , P: Andrei Popescu Middlesex University, London, P: Dmitriy Traytel ETH Zurich
14:50 - 15:30
Sunday coffee break 3Catering at Catering
14:50
40m
Coffee break
Sunday coffee break 3
Catering

15:30 - 16:20
Extended abstracts 2TyDe at L2
15:30
25m
Talk
Affine killing
TyDe
Kiko Fernandez-Reyes Uppsala University, Dave Clarke Uppsala Univ. Sweden and KU Leuvern
15:55
25m
Talk
On ringads and foldables
TyDe
James McKinna University of Edinburgh
15:30 - 16:30
EffectsHOPE at L3
15:30
30m
Talk
Programming a Web Server with Algebraic Effects
HOPE
Daan Leijen Microsoft Research
16:00
30m
Talk
Logical Relations for Algebraic Effects
HOPE
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk , Filip Sieczkowski University of Wrocław
15:30 - 16:20
Afternoon tutorial session 2Tutorials at L5
15:30
50m
Talk
Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 2)
Tutorials
Jasmin Blanchette Vrije Universiteit Amsterdam, Andreas Lochbihler , Andrei Popescu Middlesex University, London, Dmitriy Traytel ETH Zurich
16:20 - 16:50
Sunday coffee break 4Catering at Catering
16:20
30m
Coffee break
Sunday coffee break 4
Catering

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
16:50 - 17:40
Extended abstracts 3TyDe at L2
16:50
25m
Talk
Type oriented programming for task based parallelism
TyDe
17:15
25m
Talk
Type-directed reasoning for probabilistic, non-compositional resources
TyDe
Edwin Brady University of St. Andrews, UK, Kevin Hammond University of St. Andrews, UK, Christopher Schwaab University of St Andrews
16:50 - 17:40
MonotonicityHOPE at L3
16:50
30m
Talk
Recalling a Witness
HOPE
Danel Ahman University of Edinburgh, Cătălin Hriţcu Inria Paris, Kenji Maillard Inria Paris, ENS Paris, and Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, n.n., Cédric Fournet Microsoft Research, n.n.
Pre-print
16:50 - 17:50
Session 6Scheme at L4
16:50
50m
Talk
Invited Talk
Scheme
Matthew Might University of Utah, USA
17:40
10m
Day closing
Goodbye
Scheme

16:50 - 17:50
Afternoon tutorial session 3Tutorials at L5
16:50
60m
Talk
Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 3)
Tutorials
P: Jasmin Blanchette Vrije Universiteit Amsterdam, P: Andreas Lochbihler , P: Andrei Popescu Middlesex University, London, P: Dmitriy Traytel ETH Zurich

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:00 - 10:30
Monday coffee break 1Catering at Catering
10:00
30m
Coffee break
Monday coffee break 1
Catering

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
10:30 - 10:45
WelcomeFSCD at L2
10:30
15m
Other
Welcome message
FSCD
C: Sam Staton University of Oxford, P: Dale Miller INRIA Saclay and LIX
10:45 - 11:45
Session 1FSCD at L2
10:45
60m
Talk
Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages
FSCD
I: Alexandra Silva University College London
12:00 - 13:00
Monday lunchCatering at Catering
12:00
60m
Lunch
Monday lunch
Catering

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
14:30 - 15:00
Monday coffee break 2Catering at Catering
14:30
30m
Coffee break
Monday coffee break 2
Catering

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
15:00 - 16:00
Session 3FSCD at L2
15:00
30m
Talk
Relating System F and λ2: A Case Study in Coq, Abella and Beluga
FSCD
A: Jonas Kaiser , A: Brigitte Pientka McGill University, A: Gert Smolka Saarland University
15:30
30m
Talk
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
FSCD
Jasmin Blanchette Vrije Universiteit Amsterdam, A: Mathias Fleury MPI-INF, A: Dmitriy Traytel ETH Zurich
16:10 - 16:40
Monday coffee break 3Catering at Catering
16:10
30m
Coffee break
Monday coffee break 3
Catering

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

18:30 - 20:30
Welcome ReceptionSocial Events at Foyer
18:30
2h
Social Event
Welcome Reception
Social Events

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:00 - 10:30
Tuesday coffee break 1Catering at Catering
10:00
30m
Coffee break
Tuesday coffee break 1
Catering

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
10:30 - 11:30
Session 5FSCD at L2
10:30
60m
Talk
Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses
FSCD
Georg Moser University of Innsbruck
11:30 - 12:00
Session 6FSCD at L2
11:30
30m
Talk
Continuation Passing Style for Effect Handlers
FSCD
A: Daniel Hillerström The University of Edinburgh, A: Sam Lindley University of Edinburgh, UK, A: Robert Atkey University of Strathclyde, A: KC Sivaramakrishnan University of Cambridge
12:00 - 13:00
Tuesday lunchCatering at Catering
12:00
60m
Lunch
Tuesday lunch
Catering

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
14:30 - 15:00
Tuesday coffee break 2Catering at Catering
14:30
30m
Coffee break
Tuesday coffee break 2
Catering

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
15:00 - 16:00
Session 8FSCD at L2
15:00
30m
Talk
Is the optimal implementation inefficient? Elementarily not
FSCD
A: Stefano Guerrini , A: Marco Solieri University of Bath
15:30
30m
Talk
Optimality and the Linear Substitution Calculus
FSCD
A: Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, A: Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina
16:10 - 16:40
Tuesday coffee break 3Catering at Catering
16:10
30m
Coffee break
Tuesday coffee break 3
Catering

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:00 - 10:30
Wednesday coffee break 1Catering at Catering
10:00
30m
Coffee break
Wednesday coffee break 1
Catering

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
10:30 - 12:00
Session 11FSCD at L2
10:30
30m
Talk
Displayed categories
FSCD
11:00
30m
Talk
List Objects with Algebraic Structure
FSCD
A: Marcelo Fiore Computer Laboratory, University of Cambridge, A: Philip Saville
11:30
30m
Talk
There is only one notion of differentiation
FSCD
12:00 - 13:00
Wednesday lunchCatering at Catering
12:00
60m
Lunch
Wednesday lunch
Catering

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
14:30 - 15:00
Wednesday coffee break 2Catering at Catering
14:30
30m
Coffee break
Wednesday coffee break 2
Catering

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
15:00 - 16:00
Session 13FSCD at L2
15:00
30m
Talk
Böhm Reduction in Infinitary Term Graph Rewriting Systems
FSCD
A: Patrick Bahr IT University of Copenhagen
15:30
30m
Talk
Infinite Runs in Abstract Completion
FSCD
16:10 - 16:40
Wednesday coffee break 3Catering at Catering
16:10
30m
Coffee break
Wednesday coffee break 3
Catering

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:10 - 17:20
Termination and Complexity Competition 2017FSCD at L2
17:10
10m
Other
Termination and Complexity Competition 2017
FSCD
17:20 - 18:10
FSCD General MeetingFSCD at L2
17:20
50m
Meeting
FSCD General Meeting
FSCD

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
18:30 - 22:30
18:30
4h
Social Event
Banquet
Social Events

Thu 7 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Session 15FSCD at L2
09:00
60m
Talk
Type systems for the relational verification of higher order programs
FSCD
A: Marco Gaboardi University at Buffalo, SUNY, USA
09:00 - 09:05
WelcomeML at L3
Chair(s): Sam Lindley University of Edinburgh, UK
09:00
5m
Day opening
Welcome
ML

09:00 - 09:10
Welcome to FHPC'17FHPC at L4
09:00
10m
Day opening
Welcome to FHPC'17
FHPC
Phil Trinder University of Glasgow, Cosmin Oancea DIKU, University of Copenhagen
09:00 - 10:00
CUFP Tutorials C2CUFP at L5
Chair(s): Runhang Li Twitter, Inc
09:00
60m
Other
Tutorial C2: Extensible Effects: understanding them, implementing them, using them
CUFP
09:00 - 10:00
CUFP Tutorials C1CUFP at L6
Chair(s): Runhang Li Twitter, Inc
09:00
60m
Other
Tutorial C1: Online Applications with Incremental
CUFP
T: Yaron Minsky , T: Sebastian Funk Jane Street
09:05 - 10:00
Invited talkML at L3
Chair(s): Sam Lindley University of Edinburgh, UK
09:05
55m
Talk
State machines all the way down
ML
Edwin Brady University of St. Andrews, UK
09:10 - 10:10
First KeynoteFHPC at L4
Chair(s): Kevin Hammond University of St. Andrews, UK
09:10
60m
Talk
Haskell in the Datacentre
FHPC
Simon Marlow Facebook
10:00 - 10:30
Thursday coffee break 1Catering at Catering
10:00
30m
Coffee break
Thursday coffee break 1
Catering

10:30 - 11:59
Session 16FSCD at L2
10:30
30m
Talk
Arrays and References in Resource Aware ML
FSCD
A: Benjamin Lichtman , A: Jan Hoffmann Carnegie Mellon University
11:00
30m
Talk
The Complexity of Principal Inhabitation
FSCD
A: Andrej Dudenhefner Technical University Dortmund, A: Jakob Rehof Technical University Dortmund
11:30
29m
Talk
Types as Resources for Classical Natural Deduction
FSCD
A: Delia Kesner Université de Paris, CNRS, IRIF, France, A: Pierre Vial
10:30 - 11:45
Types and modulesML at L3
10:30
25m
Talk
Mergeable types
ML
Gowtham Kaki Purdue University, KC Sivaramakrishnan University of Cambridge, Samodya Abeysiriwardane Purdue University, Suresh Jagannathan Purdue University
10:55
25m
Talk
Tierless modules
ML
Gabriel Radanne Université Denis Diderot Paris 7, PPS, Jérôme Vouillon Univ Paris Diderot, Sorbonne Paris Cité, BeSport
11:20
25m
Talk
First-class subtypes
ML
Jeremy Yallop University of Cambridge, UK, Stephen Dolan
10:30 - 11:30
CompilationFHPC at L4
Chair(s): Phil Trinder University of Glasgow
10:30
30m
Talk
From High-level Radio Protocol Specifications to Efficient Low-level Implementations via Partial Evaluation
FHPC
A: Geoffrey Mainland Drexel University, USA, A: Siddhanathan Shanmugam Drexel University, USA
11:00
30m
Talk
Destination-Passing Style for Efficient Memory Management
FHPC
A: Amir Shaikhha EPFL, Switzerland, A: Andrew Fitzgibbon Microsoft Research, Cambridge, A: Simon Peyton Jones Microsoft Research, Cambridge, A: Dimitrios Vytiniotis Microsoft Research, Cambridge
10:30 - 11:30
CUFP Tutorials C1CUFP at L6
10:30
60m
Talk
Tutorial C1: Online Applications with Incremental (part 2)
CUFP
T: Yaron Minsky , T: Sebastian Funk Jane Street
11:20 - 12:00
Thursday coffee break 2Catering at Catering
11:20
40m
Coffee break
Thursday coffee break 2
Catering

12:00 - 12:30
Day 1, Session 3Haskell at L1
12:00
30m
Talk
Ode on a Random Urn (Functional Pearl)
Haskell
12:00 - 12:25
VerificationML at L3
12:00
25m
Talk
VOCAL -- a verified OCAml Library
ML
Arthur Charguéraud Inria, Jean-Christophe Filliatre CNRS, Paris, France, Mário Pereira LRI - Université Paris-Sud, François Pottier Inria, France
12:00 - 12:30
ToolsFHPC at L4
Chair(s): Cosmin Oancea DIKU, University of Copenhagen
12:00
30m
Talk
VisPar: Visualising dataflow graphs from the Par monad
FHPC
A: Maximilian Algehed Chalmers University of Technology, Sweden, A: Patrik Jansson Chalmers University of Technology
12:00 - 12:30
CUFP Tutorials C1CUFP at L6
12:00
30m
Talk
Tutorial C1: Online Applications with Incremental (part 3)
CUFP
T: Yaron Minsky , T: Sebastian Funk Jane Street
12:25 - 14:00
Thursday lunchCatering at Catering
12:25
1h35m
Lunch
Thursday lunch
Catering

14:00 - 15:15
Programming language designML at L3
14:00
25m
Talk
Typer: an infix statically typed Lisp
ML
Pierre Delaunay Université de Montréal, Vincent Archambault-Bouffard Université de Montréal, Stefan Monnier Université de Montréal
14:25
25m
Talk
Relational conversion for OCaml
ML
Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev
14:50
25m
Talk
Towards abductive functional programming
ML
Koko Muroya University of Birmingham, UK
14:00 - 15:00
Parallel ProgrammingFHPC at L4
Chair(s): Geoffrey Mainland Drexel University, USA
14:00
30m
Talk
In Search of a Map: using Program Slicing to Discover Potential Parallelism in Recursive Functions
FHPC
A: Adam Barwell , A: Kevin Hammond University of St. Andrews, UK
14:30
30m
Talk
Strategies for Regular Segmented Reductions on GPU
FHPC
A: Rasmus Wriedt Larsen DIKU, University of Copenhagen, A: Troels Henriksen DIKU, University of Copenhagen
14:00 - 15:00
CUFP Tutorials C3CUFP at L5
Chair(s): Runhang Li Twitter, Inc
14:00
60m
Other
Tutorial C3: Concurrent Programming with Effect Handlers
CUFP
T: Daniel Hillerström The University of Edinburgh, T: KC Sivaramakrishnan University of Cambridge
14:00 - 15:00
CUFP Tutorials C4CUFP at L6
Chair(s): Runhang Li Twitter, Inc
14:00
60m
Talk
Tutorial C4: Git under the hood with OCaml
CUFP
14:50 - 15:30
Thursday coffee break 3Catering at Catering
14:50
40m
Coffee break
Thursday coffee break 3
Catering

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
15:30 - 16:20
PerformanceML at L3
15:30
25m
Talk
Making SML# a general-purpose high-performance language
ML
Atsushi Ohori Tohoku University, Japan, Kenjiro Taura The University of Tokyo, Katsuhiro Ueno Tohoku University
15:55
25m
Talk
Efficient representation of large, dynamic sequences in ML
ML
15:30 - 16:30
Demo SessionFHPC at L4
Chair(s): Cosmin Oancea DIKU, University of Copenhagen
15:30
29m
Demonstration
Futhark Demo
FHPC
Troels Henriksen DIKU, University of Copenhagen
16:00
29m
Demonstration
ParaFormance Demo: Democratizing Parallel Software Development
FHPC
Christopher Brown University of St. Andrews, UK, Kevin Hammond University of St. Andrews, UK
16:30
20m
Social Event
Break 16:30 - 16:50: Wine and Nibbles @ North Mezzanine
FHPC

15:30 - 16:20
CUFP Tutorials C3CUFP at L5
15:30
50m
Talk
Tutorial C3: Concurrent Programming with Effect Handlers (part 2)
CUFP
T: Daniel Hillerström , T: KC Sivaramakrishnan University of Cambridge
15:30 - 16:20
CUFP Tutorials C4CUFP at L6
15:30
50m
Talk
Tutorial C4: Git under the hood with OCaml (part 2)
CUFP
16:20 - 16:50
Thursday coffee break 4Catering at Catering
16:20
30m
Coffee break
Thursday coffee break 4
Catering

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
16:50 - 17:40
EffectsML at L3
16:50
25m
Talk
Effects without monads: non-determinism
ML
17:15
25m
Talk
Effectively tackling the awkward squad
ML
Stephen Dolan , Spiros Eliopoulos Jane Street Group, Daniel Hillerström The University of Edinburgh, Anil Madhavapeddy OCaml Labs, KC Sivaramakrishnan University of Cambridge, Leo White Jane Street
16:50 - 17:50
Demo and PanelFHPC at L4
Chair(s): Phil Trinder University of Glasgow
16:50
30m
Demonstration
Ziria Demo: Wringing performance from high-level code
FHPC
Siddhanathan Shanmugam Drexel University, USA, Geoffrey Mainland Drexel University, USA
17:20
30m
Day closing
Panel Discussion: The challenges for Functional High Performance Computing
FHPC
Geoffrey Mainland Drexel University, USA, Kevin Hammond University of St. Andrews, UK, Simon Marlow Facebook
16:50 - 17:30
CUFP Tutorials C3CUFP at L5
16:50
40m
Talk
Tutorial C3: Concurrent Programming with Effect Handlers (part 3)
CUFP
T: Daniel Hillerström The University of Edinburgh, T: KC Sivaramakrishnan University of Cambridge
16:50 - 17:30
CUFP Tutorials C4CUFP at L6
16:50
40m
Talk
Tutorial C4: Git under the hood with OCaml (part 3)
CUFP
18:15 - 20:30
Industry ReceptionSocial Events at Ashmolean Museum
18:15
2h15m
Social Event
Industry Reception
Social Events

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
09:00 - 09:10
OpeningOCaml at L3
09:00
5m
Day opening
Opening
OCaml
Gabriel Scherer Northeastern University
09:00 - 09:10
Opening & WelcomeErlang at L4
09:00
10m
Day opening
Opening & Welcome
Erlang

09:00 - 10:00
CUFP Tutorials C6CUFP at L5
Chair(s): Runhang Li Twitter, Inc
09:00
60m
Talk
Tutorial C6: Transducers in Practice
CUFP
09:00 - 10:00
CUFP Tutorials C5CUFP at L6
Chair(s): Runhang Li Twitter, Inc
09:00
60m
Talk
Tutorial C5: Teaching Functional Programming
CUFP
Michael Sperber Active Group GmbH
09:10 - 10:10
Talk session 1OCaml at L3
09:05
35m
Talk
Invited talk: new contributors
OCaml
David Allsopp University of Cambridge, Florian Angeletti , Sébastien Hinderer Inria
09:40
25m
Talk
The State of the OCaml Platform: September 2017
OCaml
09:10 - 10:00
Keynote Invited TalkErlang at L4
09:10
50m
Talk
Keynote
Erlang
10:00 - 10:30
Friday coffee break 1Catering at Catering
10:00
30m
Coffee break
Friday coffee break 1
Catering

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
10:30 - 11:30
Talk session 2OCaml at L3
10:30
20m
Talk
Owl: A General-Purpose Numerical Library in OCaml
OCaml
Liang Wang University of Cambridge
Link to publication Pre-print
10:50
20m
Talk
Extending OCaml's open
OCaml
Runhang Li Twitter, Inc, Jeremy Yallop University of Cambridge, UK
Link to publication Pre-print
11:10
20m
Talk
Genspio: Generating Shell Phrases In OCaml
OCaml
Sebastien Mondet Mount Sinai - Hammer Lab
Pre-print
10:30 - 11:30
CUFP Tutorials C6CUFP at L5
10:30
60m
Talk
Tutorial C6: Transducers in Practice (part 2)
CUFP
T: Renzo Borgatti uSwitch
10:30 - 11:30
CUFP Tutorials C5CUFP at L6
10:30
60m
Talk
Tutorial C5: Teaching Functional Programming (part 2)
CUFP
T: Michael Sperber Active Group GmbH
11:20 - 12:00
Friday coffee break 2Catering at Catering
11:20
40m
Coffee break
Friday coffee break 2
Catering

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
12:00 - 12:25
Session 3Erlang at L4
12:00
25m
Talk
Erlang and Elixir development news
Erlang

12:00 - 12:30
CUFP Tutorials C6CUFP at L5
12:00
30m
Talk
Tutorial C6: Transducers in Practice (part 3)
CUFP
T: Renzo Borgatti uSwitch
12:00 - 12:30
CUFP Tutorials C5CUFP at L6
12:00
30m
Talk
Tutorial C5: Teaching Functional Programming (part 3)
CUFP
T: Michael Sperber Active Group GmbH
12:25 - 14:00
Friday lunchCatering at Catering
12:25
1h35m
Lunch
Friday lunch
Catering

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
14:00 - 14:50
Session 4Erlang at L4
14:00
25m
Talk
Distributed Memory Architecture for High-Level Synthesis of Embedded Controllers from Erlang
Erlang
Kagumi Azuma Kwansei Gakuin University, Nagisa Ishiura Kwansei Gakuin University, Nobuaki Yoshida ASTEM RI/KYOTO, Hiroyuki Kanbara ASTEM RI/KYOTO
14:25
25m
Talk
Structuring Erlang BEAM control flow
Erlang
Dániel Lukács Eötvös Loránd University, Melinda Tóth
14:00 - 15:00
CUFP Tutorials C8CUFP at L5
Chair(s): Runhang Li Twitter, Inc
14:00
60m
Talk
Tutorial C8: GraphQL Servers in OCaml
CUFP
T: Andreas Garnæs Zendesk
14:00 - 15:00
CUFP Tutorials C7CUFP at L6
Chair(s): Runhang Li Twitter, Inc
14:00
60m
Talk
Tutorial C7: Owl - Data Science in OCaml
CUFP
T: Liang Wang University of Cambridge
14:50 - 15:30
Friday coffee break 3Catering at Catering
14:50
40m
Coffee break
Friday coffee break 3
Catering

15:30 - 16:30
Day 2, Session 5Haskell at L1
15:30
30m
Talk
Hardware Software Co-Design in Haskell
Haskell
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
15:30 - 16:30
Talk session 4OCaml at L3
15:30
20m
Talk
A B-tree library for OCaml
OCaml
Tom Ridge University of Leicester, UK
Link to publication
15:50
20m
Talk
Wodan: a pure OCaml, flash-aware filesystem library
OCaml
Link to publication
16:10
20m
Talk
Tezos: the OCaml Crypto-Ledger
OCaml
Benjamin Canou OCamlPro, n.n., Grégoire Henry OCamlPro, n.n., Pierre Chambart OCamlPRO, Fabrice Le Fessant OCamlPro, Arthur BREITMAN Dynamic Ledger Solutions
15:30 - 16:20
CUFP Tutorials C8CUFP at L5
15:30
50m
Talk
Tutorial C8: GraphQL Servers in OCaml (part 2)
CUFP
T: Andreas Garnæs Zendesk
15:30 - 16:20
CUFP Tutorials C7CUFP at L6
15:30
50m
Talk
Tutorial C7: Owl - Data Science in OCaml (part 2)
CUFP
T: Liang Wang University of Cambridge
16:20 - 16:50
Friday coffee break 4Catering at Catering
16:20
30m
Coffee break
Friday coffee break 4
Catering

16:50 - 17:40
Talk session 5OCaml at L3
17:00
20m
Talk
Component-based Program Synthesis in OCaml
OCaml
Zhanpeng Liang University of Southern California, Kanae Tsushima
Link to publication
17:20
20m
Talk
Testing with Crowbar
OCaml
16:50 - 17:50
Session 6Erlang at L4
16:50
30m
Talk
eAOP - An Aspect Oriented Programming Framework for Erlang
Erlang
Ian Cassar University of Malta, Adrian Francalanza University of Malta, Luca Aceto Reykjavik University, Anna Ingolfsdottir Reykjavik University
17:20
30m
Talk
In medias res: WIP discussion
Erlang

16:50 - 17:30
CUFP Tutorials C8CUFP at L5
16:50
40m
Talk
Tutorial C8: GraphQL Servers in OCaml (part 3)
CUFP
T: Andreas Garnæs Zendesk
16:50 - 17:30
CUFP Tutorials C7CUFP at L6
16:50
40m
Talk
Tutorial C7: Owl - Data Science in OCaml (part 3)
CUFP
T: Liang Wang University of Cambridge

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
09:00 - 09:10
IntroductionFARM at L3
09:00
10m
Day opening
Welcome
FARM
C: Michael Sperber Active Group GmbH, P: Jean Bresson UMR STMS: IRCAM-CNRS-UPMC
09:10 - 10:00
CUFP Talks 1CUFP at L2
09:10
25m
Talk
Keynote: Are We There Yet?
CUFP
Bodil Stokke Church of Emacs
09:35
25m
Talk
Bonsai: a DSL for serverless firm real-time decisioning
CUFP
10:00 - 10:30
Saturday coffee break 1Catering at Catering
10:00
30m
Coffee break
Saturday coffee break 1
Catering

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

10:30 - 11:30
Session 2: Papers/DemosFARM at L3
Chair(s): Ivan Perez University of Nottingham, UK
10:30
20m
Demonstration
Demo — African Polyphony and Polyrhythm
FARM
Chris Ford ThoughtWorks (UK) Ltd.
Pre-print
10:50
20m
Demonstration
Demo — Vivid: Sound Synthesis with Haskell and SuperCollider
FARM
Pre-print
11:10
30m
Talk
GALE: A Functional Graphic Adventure Library and Engine
FARM
Ivan Perez University of Nottingham, UK
11:20 - 12:00
Saturday coffee break 2Catering at Catering
11:20
40m
Coffee break
Saturday coffee break 2
Catering

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
12:00 - 12:25
CUFP Talks 3CUFP at L2
12:00
25m
Talk
Gens N' Roses: Appetite for Reduction
CUFP
12:25 - 14:00
Saturday lunchCatering at Catering
12:25
1h35m
Lunch
Saturday lunch
Catering

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

14:00 - 14:50
CUFP Talks 4CUFP at L2
14:00
25m
Talk
Formally Verifying a Smart-Contract Language Implementation with Isabelle
CUFP
Simon Meier Digital Asset
14:25
25m
Talk
Haskell games and apps for iOS and Android
CUFP
Ivan Perez University of Nottingham, UK
14:00 - 15:00
Session 4: TutorialFARM at L3
Chair(s): Jean Bresson UMR STMS: IRCAM-CNRS-UPMC
14:00
60m
Talk
FAUST Tutorial for Functional Programmers
FARM
14:50 - 15:30
Saturday coffee break 3Catering at Catering
14:50
40m
Coffee break
Saturday coffee break 3
Catering

15:30 - 16:30
Tool SupportHIW at L1
Chair(s): Wren Romano X
15:30
25m
Talk
IDE Support in GHC
HIW
15:55
25m
Talk
Tracking GHC Performance
HIW
16:20
10m
Talk
Lightning Talk Slot #3
HIW

15:30 - 16:20
CUFP Talks 5CUFP at L2
15:30
25m
Talk
Using Haskell to run a datacenter
CUFP
15:55
25m
Talk
Functional Facades over Legacy Code
CUFP
Nicholas Cowle G-Research, Robin Kay G-Research
15:30 - 16:20
Session 5: DemosFARM at L3
Chair(s): David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University
15:30
20m
Demonstration
Demo — The Arpeggigon: A Functional Reactive Musical Automaton
FARM
Henrik Nilsson University of Nottingham, UK
Pre-print
15:50
20m
Demonstration
Demo — Ait: A Concatenative Language for Creative Programming
FARM
Pre-print
16:20 - 16:50
Saturday coffee break 4Catering at Catering
16:20
30m
Coffee break
Saturday coffee break 4
Catering

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

16:50 - 17:40
Session 6: Papers/DemosFARM at L3
Chair(s): Henrik Nilsson University of Nottingham, UK
16:50
30m
Talk
Unified Media Programming: An Algebraic Approach
FARM
Simon Archipoff CNRS LaBRI, Inria Bordeaux,, David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University
17:20
20m
Demonstration
Demo — Octopus: A High-Level Fast 3D Animation Language
FARM
Simon Archipoff CNRS LaBRI, Inria Bordeaux,, David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University
Pre-print
19:30 - 22:00
FARM Performance EveningSocial Events at Old Fire Station
19:30
2h30m
Social Event
FARM Evening Of Algorithmic Arts
Social Events