Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
VenueNara Kasugano International Forum
Room nameNoh Theater
Floor1
Capacity500
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 19 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

09:15 - 10:15
Keynote 1Keynote Talks at Noh Theater
Chair(s): Eijiro Sumii Tohoku University
09:15
60m
Talk
TensorFlow: Learning Functions at Scale
Keynote Talks
10:45 - 12:25
Session 1Research Papers at Noh Theater
Chair(s): Akimasa Morihata University of Tokyo, Japan
10:45
25m
Talk
Farms, Pipes, Streams and Reforestation: Reasoning about Structured Parallel Processes using Types and Hylomorphisms
Research Papers
David Castro-Perez University of St. Andrews, UK, Kevin Hammond University of St. Andrews, UK, Susmit Sarkar University of St. Andrews, UK
DOI
11:10
25m
Talk
Dag-Calculus: A Calculus for Parallel Computation
Research Papers
Umut A. Acar Carnegie Mellon University, Arthur Charguéraud Inria, France, Mike Rainey Inria, France, Filip Sieczkowski Inria, France
DOI
11:35
25m
Talk
A Lambda-Calculus Foundation for Universal Probabilistic Programming
Research Papers
Johannes Borgström Uppsala University, Sweden, Ugo Dal Lago University of Bologna, France, Andrew D. Gordon Microsoft Research, UK, Marcin Szymczak University of Edinburgh, UK
DOI
12:00
25m
Talk
Deriving a Probability Density Calculator (Functional Pearl)
Research Papers
Wazim Mohammed Ismail Indiana University, USA, Chung-chieh Shan Indiana University, USA
DOI
13:40 - 14:55
Session 2Research Papers at Noh Theater
Chair(s): Kathleen Fisher Tufts University
13:40
25m
Talk
A New Verified Compiler Backend for CakeML
Research Papers
Yong Kiam Tan IHPC at A*STAR, Singapore, Magnus O. Myreen Chalmers University of Technology, Sweden, Ramana Kumar Data61 at CSIRO, Australia, Anthony Fox University of Cambridge, UK, Scott Owens University of Kent, UK, Michael Norrish Data61 at CSIRO, Australia
DOI
14:05
25m
Talk
Sequent Calculus as a Compiler Intermediate Language
Research Papers
Paul Downen University of Oregon, USA, Luke Maurer University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft Research, UK
DOI
14:30
25m
Talk
Refinement through Restraint: Bringing Down the Cost of Verification
Research Papers
Liam O'Connor UNSW, Australia, Zilin Chen UNSW, Australia, Christine Rizkallah University of Pennsylvania, USA, Sidney Amani UNSW, Australia, Japheth Lim Data61, Australia, Toby Murray University of Melbourne, Australia, Yutaka Nagashima Data61, Australia, Thomas Sewell UNSW, Australia, Gerwin Klein UNSW, Australia
DOI
15:15 - 16:30
Session 3Research Papers at Noh Theater
Chair(s): Neel Krishnaswami University of Birmingham, UK
15:15
25m
Talk
Fully Abstract Compilation via Universal Embedding
Research Papers
Max New Northeastern University, William J. Bowman Northeastern University, Amal Ahmed Northeastern University
DOI
15:40
25m
Talk
Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)
Research Papers
Christos Dimoulas Harvard University, Max New Northeastern University, Robby Findler Northwestern University, Matthias Felleisen Northeastern University
DOI
16:05
25m
Talk
A Type Theory for Incremental Computational Complexity with Control Flow Changes
Research Papers
Ezgi Çiçek MPI-SWS, Germany, Zoe Paraskevopoulou Princeton University, USA, Deepak Garg MPI-SWS, Germany
DOI
17:00 - 18:15
Session 4Research Papers at Noh Theater
Chair(s): Tom Schrijvers KU Leuven
17:00
25m
Talk
Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms
Research Papers
Kotaro Takeda University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan, Kazuya Yaguchi Tohoku University, Japan, Ayumi Shinohara Tohoku University, Japan
DOI
17:25
25m
Talk
Queueing and Glueing for Optimal Partitioning (Functional Pearl)
Research Papers
Shin-Cheng Mu Academia Sinica, Taiwan, Yu-Hsi Chiang National Taiwan University, Taiwan, Yu-Han Lyu Dartmouth College, USA
DOI
17:50
25m
Talk
All Sorts of Permutations (Functional Pearl)
Research Papers
Jan Christiansen Flensburg University of Applied Sciences, Germany, Nikita Danilenko University of Kiel, Germany, Sandra Dylus University of Kiel, Germany
DOI

Tue 20 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

09:15 - 10:15
Keynote 2Keynote Talks at Noh Theater
Chair(s): Gabriele Keller University of New South Wales
09:15
60m
Talk
Journey to Find Bugs in JavaScript Web Applications in the Wild
Keynote Talks
10:35 - 12:15
Session 5Research Papers at Noh Theater
Chair(s): Robby Findler Northwestern University
10:35
25m
Talk
A Glimpse of Hopjs
Research Papers
Manuel Serrano Inria, France, Vincent Prunet Inria, France
DOI
11:00
25m
Talk
Experience Report: Growing and Shrinking Polygons for Random Testing of Computational Geometry Algorithms
Research Papers
Ilya Sergey University College London, UK
DOI
11:25
25m
Talk
Think Like a Vertex, Behave Like a Function! A Functional DSL for Vertex-Centric Big Graph Processing
Research Papers
Kento Emoto Kyushu Institute of Technology, Japan, Kiminori Matsuzaki Kochi University of Technology, Japan, Zhenjiang Hu National Institute of Informatics, Japan, Akimasa Morihata University of Tokyo, Japan, Hideya Iwasaki University of Electro-Communications, Japan
DOI
11:50
25m
Talk
Datafun: A Functional Datalog
Research Papers
Michael Arntzenius University of Birmingham, UK, Neel Krishnaswami University of Birmingham, UK
DOI
13:30 - 14:45
Session 6Research Papers at Noh Theater
Chair(s): Johan Jeuring Utrecht University
13:30
25m
Talk
Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)
Research Papers
Eric Seidel University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, USA, Westley Weimer University of Virginia, USA
DOI
13:55
25m
Talk
Automatically Disproving Fair Termination of Higher-Order Functional Programs
Research Papers
Keiichi Watanabe University of Tokyo, Japan, Ryosuke Sato University of Tokyo, Japan, Takeshi Tsukada University of Tokyo, Japan, Naoki Kobayashi University of Tokyo, Japan
DOI
14:20
25m
Talk
Higher-Order Ghost State
Research Papers
Ralf Jung MPI-SWS, Germany, Robbert Krebbers Aarhus University, Denmark, Lars Birkedal Aarhus University, Denmark, Derek Dreyer MPI-SWS, Germany
DOI
15:05 - 16:20
Session 7Research Papers at Noh Theater
Chair(s): Andres Löh Well-Typed LLP
15:05
25m
Talk
Unifiers as Equivalences: Proof-Relevant Unification of Dependently Typed Data
Research Papers
Jesper Cockx iMinds, Belgium, Dominique Devriese iMinds, Belgium, Frank Piessens iMinds, Belgium
DOI
15:30
25m
Talk
Elaborator Reflection: Extending Idris in Idris
Research Papers
David Thrane Christiansen Indiana University, USA, Edwin Brady University of St. Andrews, UK
DOI
15:55
25m
Talk
Partial Type Equivalences for Verified Dependent Interoperability
Research Papers
Pierre-Evariste Dagand UPMC, France, Nicolas Tabareau Inria, France, Éric Tanter University of Chile, Chile
DOI
16:50 - 17:40
Session 8Research Papers at Noh Theater
Chair(s): Scott Owens University of Kent, UK
16:50
25m
Talk
Constructive Galois Connections: Taming the Galois Connection Framework for Mechanized Metatheory
Research Papers
David Darais University of Maryland, USA, David Van Horn University of Maryland, USA
DOI
17:15
25m
Talk
An Abstract Memory Functor for Verified C Static Analyzers
Research Papers
Sandrine Blazy University of Rennes 1, France, Vincent Laporte IMDEA Software Institute, Spain, David Pichardie ENS Rennes, France
DOI
17:40 - 18:10
ICFP Program Chair Report and Contest PresentationReports at Noh Theater
17:40
10m
Other
Program Chair Report (Eijiro Sumii)
Reports

17:50
20m
Awards
Programming Contest Presentation (Keisuke Nakano)
Reports

Wed 21 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

09:15 - 10:15
Keynote 3Keynote Talks at Noh Theater
Chair(s): Jacques Garrigue Nagoya University
09:15
60m
Talk
A Functional Programmer's Guide to Homotopy Type Theory
Keynote Talks
Dan Licata Wesleyan University
10:35 - 12:15
Session 9Research Papers at Noh Theater
Chair(s): Sam Lindley University of Edinburgh, UK
10:35
25m
Talk
Ghostbuster: A Tool for Simplifying and Converting GADTs
Research Papers
Trevor L. McDonell Indiana University, USA, Timothy A. K. Zakian Oxford University, UK, Matteo Cimini Indiana University, USA, Ryan R. Newton Indiana University, USA
DOI
11:00
25m
Talk
Indexed Codata Types
Research Papers
David Thibodeau McGill University, Canada, Andrew Cave McGill University, Canada, Brigitte Pientka McGill University, Canada
DOI
11:25
25m
Talk
Disjoint Intersection Types
Research Papers
Bruno C. d. S. Oliveira University of Hong Kong, China, Zhiyuan Shi University of Hong Kong, China, João Alpuim University of Hong Kong, China
DOI
11:50
25m
Talk
Set-Theoretic Types for Polymorphic Variants
Research Papers
Giuseppe Castagna Paris Diderot University & CNRS, Tommaso Petrucciani University of Genoa, France, Kim Nguyễn University of Paris-Sud, France
DOI
13:30 - 14:45
Session 10Research Papers at Noh Theater
Chair(s): John Reppy University of Chicago
13:30
25m
Talk
Hierarchical Memory Management for Parallel Programs
Research Papers
Ram Raghunathan Carnegie Mellon University, USA, Stefan K. Muller Carnegie Mellon University, USA, Umut A. Acar Carnegie Mellon University, Guy Blelloch Carnegie Mellon University, USA
DOI
13:55
25m
Talk
Allocation Characterizes Polyvariance: A Unified Methodology for Polyvariant Control-Flow Analysis
Research Papers
Thomas Gilray University of Utah, USA, Michael D. Adams University of Utah, USA, Matthew Might University of Utah, USA
DOI
14:20
25m
Talk
A Fully Concurrent Garbage Collector for Functional Programs on Multicore Processors
Research Papers
Katsuhiro Ueno Tohoku University, Japan, Atsushi Ohori Tohoku University, Japan
DOI
15:05 - 16:20
Session 11Research Papers at Noh Theater
Chair(s): Alejandro Russo Chalmers University of Technology
15:05
25m
Talk
Talking Bananas: Structural Recursion for Session Types
Research Papers
Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Edinburgh, UK
DOI
15:30
25m
Talk
The Best of Both Worlds: Linear Functional Programming without Compromise
Research Papers
J. Garrett Morris University of Edinburgh, UK
DOI
15:55
25m
Talk
Context-Free Session Types
Research Papers
Peter Thiemann University of Freiburg, Germany, Vasco Thudichum Vasconcelos
DOI
16:50 - 17:40
Session 12Research Papers at Noh Theater
Chair(s): Jeremy Gibbons University of Oxford, UK
16:50
25m
Talk
Combining Effects and Coeffects via Grading
Research Papers
Marco Gaboardi SUNY Buffalo, USA, Shin-ya Katsumata Kyoto University, Japan, Dominic Orchard University of Cambridge, UK, Flavien Breuvart Inria, France, Tarmo Uustalu Tallinn University of Technology, Estonia
DOI
17:15
25m
Talk
String Diagrams for Free Monads (Functional Pearl)
Research Papers
Maciej Piróg KU Leuven, Belgium, Nicolas Wu University of Bristol, UK
DOI
17:40 - 18:10
SRC Awards and ClosingReports at Noh Theater
17:40
15m
Awards
SRC Awards (David Van Horn)
Reports

17:55
15m
Day closing
ICFP 2016 Closing / ICFP 2017 Presentation
Reports

Thu 22 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

09:15 - 10:15
TestingHaskell at Noh Theater
Chair(s): Stephanie Weirich University of Pennsylvania
09:15
10m
Day opening
Welcome
Haskell

09:25
25m
Talk
FitSpec: Refining Property Sets for Functional Testing
Haskell
DOI
09:50
25m
Talk
QuickFuzz: An Automatic Random Fuzzer for Common File Formats
Haskell
Gustavo Grieco , Martín Ceresa , Pablo Buiras Chalmers University of Technology
DOI
10:35 - 11:25
FRPHaskell at Noh Theater
Chair(s): David Terei Stanford
10:35
25m
Talk
Causal Commutative Arrows Revisited
Haskell
Jeremy Yallop University of Cambridge, UK, Hai Liu Intel Labs
DOI
11:00
25m
Talk
Functional Reactive Programming, Refactored
Haskell
Ivan Perez University of Nottingham, Manuel Bärenz , Henrik Nilsson
DOI
11:45 - 12:35
FunctorsHaskell at Noh Theater
Chair(s): Zhenjiang Hu National Institute of Informatics, Japan
11:45
25m
Talk
Free Delivery (Functional Pearl)
Haskell
Jeremy Gibbons University of Oxford, UK
DOI
12:10
25m
Talk
How to Twist Pointers without Breaking Them
Haskell
DOI
15:20 - 16:10
Language FeaturesHaskell at Noh Theater
Chair(s): Niki Vazou UC San Diego
15:20
25m
Talk
Pattern Synonyms
Haskell
Matthew Pickering , Gergo Erdi , Simon Peyton Jones Microsoft Research, UK, Richard A. Eisenberg Bryn Mawr College
DOI
15:45
25m
Talk
Desugaring Haskell's do-Notation into Applicative Operations
Haskell
Simon Marlow Facebook, Simon Peyton Jones Microsoft Research, UK, Edward Kmett , Andrey Mokhov
DOI
16:40 - 18:00
Lightning TalksHaskell at Noh Theater
Chair(s): Geoffrey Mainland Drexel University
16:40
80m
Talk
Lightning Talks
Haskell

Fri 23 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

09:15 - 10:15
Strictness and STM Haskell at Noh Theater
Chair(s): Richard A. Eisenberg Bryn Mawr College
09:25
25m
Talk
Revisiting Software Transactional Memory in Haskell
Haskell
Matthew Le , Ryan Yates , Matthew Fluet Rochester Institute of Technology
DOI
09:50
25m
Talk
Autobahn: Using Genetic Algorithms to Infer Strictness Annotations
Haskell
Yisu Remy Wang Tufts University, Diogenes Nunez , Kathleen Fisher Tufts University
DOI
10:35 - 11:25
TypesHaskell at Noh Theater
Chair(s): David Duke University of Leeds
10:35
25m
Talk
Experience Report: Types for a Relational Algebra Library
Haskell
DOI
11:00
25m
Talk
Embedding Session Types in Haskell
Haskell
Sam Lindley University of Edinburgh, UK, J. Garrett Morris University of Edinburgh, UK
DOI
11:45 - 12:35
PC Chair Report and State of HaskellHaskell at Noh Theater
11:45
50m
Talk
PC Chair Report and State of Haskell
Haskell

14:00 - 14:50
MonadsHaskell at Noh Theater
Chair(s): Yukiyoshi Kameyama University of Tsukuba
14:00
25m
Talk
The Key Monad: Type-Safe Unconstrained Dynamic Typing
Haskell
Pablo Buiras Chalmers University of Technology, Koen Claessen Chalmers University of Technology, Atze van der Ploeg
DOI
14:25
25m
Talk
Supermonads: One Notion to Bind Them All
Haskell
DOI
15:20 - 16:10
Abstractions that ScaleHaskell at Noh Theater
Chair(s): Geoffrey Mainland Drexel University
15:20
25m
Talk
Non-recursive Make Considered Harmful: Build Systems at Scale
Haskell
Andrey Mokhov , Neil Mitchell , Simon Peyton Jones Microsoft Research, UK, Simon Marlow Facebook
DOI
15:45
25m
Talk
Lazy Graph Processing in Haskell
Haskell
DOI

Mon 19 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

Wed 21 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

Thu 22 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

Fri 23 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

Sat 24 Sep

Displayed time zone: Osaka, Sapporo, Tokyo change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Noh Theater