Conference program

Wednesday, September 25

9:00 Keynote: Ulf Norell (Chair: Tarmo Uustalu)
Interactive Programming with Dependent Types
10:00 Break
10:30 Session 1: Verification with Grammars and Automata (Chair: David Van Horn)
Verified Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions [Functional Pearl]
Dmitriy Traytel and Tobias Nipkow
Christopher Broadbent, Arnaud Carayol, Matthew Hague and Olivier Serre
11:10 Break
11:30 Session 2: Data Parallelism (Chair: Ryan Newton)
Automatic SIMD Vectorization for Haskell
Leaf Petersen, Dominic Orchard and Neal Glew
Exploiting Vector Instructions with Generalized Stream Fusion
Geoffrey Mainland, Roman Leshchinskiy and Simon Peyton Jones
Optimising Purely Functional GPU Programs
Trevor L. McDonell, Manuel Chakravarty, Gabriele Keller and Ben Lippmeier
12:30 Lunch
14:00 Session 3: Dependent Types (Chair: Sungwoo Park)
Type-Theory In Color
Jean-Philippe Bernardy and Guilhem Moulin
Typed Syntactic Meta-programming
Dominique Devriese and Frank Piessens
Mtac: A Monad for Typed Tactic Programming in Coq
Beta Ziliani, Derek Dreyer, Neelakantan Krishnaswami, Aleksandar Nanevski and Viktor Vafeiadis
15:00 Break
15:30 Session 4: Fun in the Afternoon (Chair: Jeremy Gibbons)
Fun with Semirings [Functional Pearl]
Stephen Dolan
Efficient Divide-and-Conquer Parsing of Practical Context-Free Languages
Jean-Philippe Bernardy and Koen Claessen
Functional Geometry and the "Traité de Lutherie" [Functional Pearl]
Harry Mairson
16:30 Break
17:00 Session 5: Handling Effects (Chair: Shin-Ya Katsumata)
Programming and Reasoning with Algebraic Effects and Dependent Types
Edwin Brady
Handlers in Action
Ohad Kammar, Sam Lindley and Nicolas Oury
17:40 Program Chair's Report

Thursday, September 26

9:00 Keynote: Simon Peyton Jones (Chair: Greg Morrisett)
Computer Science as a School Subject
10:00 Break
10:30 Session 6: Concurrency (Chair: Manuel Chakravarty)
Correctness of an STM Haskell Implementation
Manfred Schmidt-Schauss and David Sabel
Programming with Permissions in Mezzo
Francois Pottier and Jonathan Protzenko
11:10 Break
11:30 Session 7: (Co-)Recursion (Chair: Dimitrios Vytiniotis)
Wellfounded Recursion with Copatterns
Andreas Abel and Brigitte Pientka
Productive Coprogramming with Guarded Recursion
Robert Atkey and Conor McBride
Unifying Structured Recursion Schemes
Ralf Hinze, Nicolas Wu and Jeremy Gibbons
12:30 Lunch
14:00 Session 8: Functional Reactive Programming (Chair: Gabriele Keller)
Higher-Order Functional Reactive Programming without Spacetime Leaks
Neelakantan Krishnaswami
Functional Reactive Programming with Liveness Guarantees
Alan Jeffrey
A Short Cut to Parallelization Theorems
Akimasa Morihata
15:00 Break
15:30 Session 9: Lambda-Calculus (Chair: Silvia Ghilezan)
Using Circular Programs for Higher-Order Syntax [Functional Pearl]
Emil Axelsson and Koen Claessen
Weak Optimality, and the Meaning of Sharing
Thibaut Balabonski
System FC with Explicit Kind Equality
Stephanie Weirich, Justin Hsu and Richard A. Eisenberg
16:30 Break
17:00 Programming Contest Co-Chairs' Report and Awards
17:40 ICFP 2003 Most Influential Paper Award

Friday, September 27

9:00 Session 10: Monads (Chair: Alan Jeffrey)
The Constrained-Monad Problem
Neil Sculthorpe, Jan Bracker, George Giorgidze and Andy Gill
Simple and Compositional Reification of Monadic Embedded Languages [Functional Pearl]
Josef Svenningsson and Bo Joel Svensson
Structural Recursion for Querying Ordered Graphs
Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato and Keisuke Nakano
10:00 Break
10:30 Session 11: Modular Meta-Theory (Chair: Zhenjiang Hu)
Modular Monadic Meta-Theory
Benjamin Delaware, Steven Keuchel, Tom Schrijvers and Bruno Oliveira
Modular and Automated Type-Soundness Verification for Language Extensions
Florian Lorenzen and Sebastian Erdweg
11:10 Break
11:30 Session 12: Experience Reports (Chair: John Launchbury)
A Nanopass Framework for Commercial Compiler Development [Experience Report]
Andrew Keep and R Kent Dybvig
Applying Random Testing to a Base Type Environment [Experience Report]
Vincent St-Amour and Neil Toronto
Functional Programming of mHealth Applications [Experience Report]
Christian Petersen, Matthias Gorges, Dustin Dunsmuir, Mark Ansermino and Guy Dumont
12:30 Lunch
14:00 Session 13: Program Logics (Chair: Nikhil Swamy)
Hoare-Style Reasoning with (Algebraic) Continuations
Germán Andrés Delbianco and Aleksandar Nanevski
Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency
Aaron Turon, Derek Dreyer and Lars Birkedal
The Bedrock Structured Programming System
Adam Chlipala
15:00 Break
15:30 Session 14: Language Design (Chair: Peter Thiemann)
A Practical Theory of Language-Integrated Query
James Cheney, Sam Lindley and Philip Wadler
Calculating Threesomes, with Blame
Ronald Garcia
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism
Joshua Dunfield and Neelakantan R. Krishnaswami
16:30 Break
17:00 Session 15: Analysis and Optimization (Chair: Fritz Henglein)
Optimizing Abstract Abstract Machines
J. Ian Johnson, Nicholas Labich, Matthew Might and David Van Horn
Testing Noninterference, Quickly
Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim and Leonidas Lampropoulos
17:40 ICFP 2014 Advert & Closing