Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017
Oxford, United Kingdom
Toggle navigation
Attending
Venue: Mathematical Institute
Accommodation
Registration
Travel to Oxford
Practical Information
Student Volunteers
Student Travel Support
Code of Conduct
Call for Sponsorship
Visa Support Letter
Program
ICFP Program
Your Program
Filter by Day
Sun 3 Sep
Mon 4 Sep
Tue 5 Sep
Wed 6 Sep
Thu 7 Sep
Fri 8 Sep
Sat 9 Sep
Tracks
ICFP 2017
Keynotes and Reports
Tutorials
Workshops
Research Papers
Research Artifacts
Student Research Competition
Social Events
Co-hosted Conferences
CUFP
FSCD
Workshops
Erlang
FARM
FHPC
HIW
HOPE
ML
OCaml
PLMW
Scheme
TyDe
Co-hosted Symposia
Haskell
Organization
ICFP 2017 Committees
Organizing Committee
Steering Committee
Track Committees
Research Papers
Research Artifacts
Student Research Competition
Contributors
People Index
Co-hosted Conferences
CUFP
Organizing Committee
Program Committee
FSCD
N/A - check homepage
Workshops
Erlang
Organizing Committee
Program Committee
FARM
Organizing Committee
Program Committee
FHPC
Organizing Committee
Program Committee
HIW
Program Committee
HOPE
Organizing Committee
Program Committee
ML
Organizing Committee
Program Committee
OCaml
Organizing Committee
Program Committee
PLMW
Organizing Committee
Scheme
Program Committee
Steering Committee
TyDe
Organizing Committee
Program Committee
Co-hosted Symposia
Haskell
Program Committee
Search
Series
Series
ICFP 2025
ICFP 2024
ICFP 2023
ICFP 2022
ICFP 2021
ICFP 2020
ICFP 2019
ICFP 2018
ICFP 2017
ICFP 2016
Sign in
Sign up
ICFP 2017
(
series
) /
Mathematical Institute
/
Room information: L1
Venue
Mathematical Institute
Room name
L1
Floor
0
Capacity
360
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+01:00) Belfast
.
Use conference time zone: (GMT+01:00) Belfast
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+04:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
You're viewing the program in a time zone which is different from your device's time zone
change time zone
Sun 3 Sep
Displayed time zone:
Belfast
change
09:00 - 09:10
Welcome
PLMW
at
L1
Chair(s):
Brigitte Pientka
McGill University
09:00
10m
Talk
Welcome
PLMW
Brigitte Pientka
McGill University
,
Neel Krishnaswami
Computer Laboratory, University of Cambridge
,
Daniel R. Licata
Wesleyan University
09:10 - 10:00
Keynote
PLMW
at
L1
Chair(s):
Neel Krishnaswami
Computer Laboratory, University of Cambridge
09:10
50m
Talk
Keynote
PLMW
Chris Martens
North Carolina State University
10:30 - 11:30
Session 1
PLMW
at
L1
10:30
30m
Talk
A Few Frank Remarks
PLMW
Conor McBride
11:00
30m
Talk
Compositional Compiler Correctness
PLMW
Amal Ahmed
Northeastern University, USA
File Attached
12:00 - 12:30
Session 2
PLMW
at
L1
12:00
30m
Talk
Not How To Do Your PhD
PLMW
Gabriel Scherer
Northeastern University
File Attached
14:00 - 15:00
Session 3
PLMW
at
L1
14:00
30m
Talk
Gradual Typing
PLMW
Ronald Garcia
University of British Columbia
File Attached
14:30
30m
Talk
Scala: Types in Theory & Practice
PLMW
Nada Amin
University of Cambridge
File Attached
15:30 - 16:30
Session 4
PLMW
at
L1
15:30
60m
Talk
How to Write Papers and Give Talks That People Can Follow
PLMW
Derek Dreyer
MPI-SWS
Media Attached
16:50 - 17:40
Session 5
PLMW
at
L1
16:50
50m
Talk
Panel Discussion: Careers in Programming Languages
PLMW
Sam Staton
University of Oxford
,
Richard A. Eisenberg
Bryn Mawr College, USA
,
Andreas Rossberg
Google
,
Daan Leijen
,
Amal Ahmed
Northeastern University, USA
Mon 4 Sep
Displayed time zone:
Belfast
change
09:00 - 10:00
Monday Keynote
Keynotes 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 computers
Keynote
Keynotes and Reports
K:
Chris Martens
North Carolina State University
10:30 - 12:00
Art and Education
Research Papers
at
L1
Chair(s):
Kathryn E. Gray
University of Cambridge
10:30
22m
Talk
Super 8 Languages for Making Movies (Functional Pearl)
Research Papers
Leif Andersen
Northeastern University, USA
,
Stephen Chang
Northeastern University, USA
,
Matthias Felleisen
Northeastern University, USA
DOI
10:52
22m
Talk
Testing and Debugging Functional Reactive Programming
Research Papers
Ivan Perez
University of Nottingham, UK
,
Henrik Nilsson
University of Nottingham, UK
DOI
11:15
22m
Talk
Lock-Step Simulation Is Child's Play (Experience Report)
Research Papers
Joachim Breitner
University of Pennsylvania
,
Chris Smith
Google, USA
DOI
11:37
22m
Talk
Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC
Research Papers
Benjamin Canou
OCamlPro, n.n.
,
Roberto Di Cosmo
Inria, France / University of Paris Diderot, France
,
Grégoire Henry
OCamlPro, n.n.
DOI
13:00 - 14:30
Functional Programming Techniques
Research Papers
at
L1
Chair(s):
Graham Hutton
University of Nottingham
13:00
22m
Talk
Faster Coroutine Pipelines
Research Papers
Mike Spivey
University of Oxford, UK
DOI
13:22
22m
Talk
A Pretty But Not Greedy Printer (Functional Pearl)
Research Papers
Jean-Philippe Bernardy
University of Gothenburg
DOI
13:45
22m
Talk
Generic Functional Parallel Algorithms: Scan and FFT
Research Papers
Conal Elliott
Target, USA
DOI
14:07
22m
Talk
A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
Research Papers
William E. Byrd
University of Utah, USA
,
Michael Ballantyne
University of Utah, USA
,
Gregory Rosenblatt
n.n., n.n.
,
Matthew Might
University of Utah, USA
DOI
15:00 - 16:10
Applications
Research Papers
at
L1
Chair(s):
Alexandra Silva
University College London
15:00
23m
Talk
Prototyping a Query Compiler using Coq (Experience Report)
Research Papers
Joshua Auerbach
IBM Research
,
Martin Hirzel
IBM Research
,
Louis Mandel
IBM Research
,
Avraham Shinnar
IBM Research
,
Jerome Simeon
IBM Research
DOI
15:23
23m
Talk
A Framework for Adaptive Differential Privacy
Research Papers
Daniel Winograd-Cort
University of Pennsylvania, USA
,
Andreas Haeberlen
University of Pennsylvania, USA
,
Aaron Roth
University of Pennsylvania, USA
,
Benjamin C. Pierce
University of Pennsylvania
DOI
15:46
23m
Talk
Symbolic Conditioning of Arrays in Probabilistic Programs
Research Papers
Praveen Narayanan
Indiana University, USA
,
Chung-chieh Shan
Indiana University, USA
DOI
16:40 - 18:10
Effects
Research 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 Events
Keynotes and Reports
at
L1
Chair(s):
Peter Thiemann
University of Freiburg, Germany
18:10
10m
Day closing
Monday Announcements
Keynotes and Reports
Tue 5 Sep
Displayed time zone:
Belfast
change
09:00 - 10:00
Tuesday Keynote
Keynotes and Reports
at
L1
Chair(s):
Mark Jones
Portland State University
09:00
60m
Talk
Assuring AI
Keynote
Keynotes and Reports
I:
John Launchbury
Galois, Inc.
10:30 - 12:00
Low-level and Systems Programming
Research Papers
at
L1
Chair(s):
Sam Tobin-Hochstadt
Indiana University
10:30
22m
Talk
Persistence for the Masses: RRB-Vectors in a Systems Language
Research Papers
Juan Pedro BolÃvar Puente
Independent Consultant, Sinusoidal Engineering
DOI
Pre-print
10:52
22m
Talk
Verified Low-Level Programming Embedded in F*
Research Papers
Jonathan Protzenko
Microsoft Research, n.n.
,
Jean-Karim Zinzindohoué
Inria, France
,
Aseem Rastogi
Microsoft Research
,
Tahina Ramananandro
Microsoft Research, n.n.
,
Peng Wang
Massachusetts Institute of Technology, USA
,
Santiago Zanella-Béguelin
Microsoft Research, n.n.
,
Antoine Delignat-Lavaud
Microsoft Research, n.n.
,
Cătălin Hriţcu
Inria Paris
,
Karthikeyan Bhargavan
Inria, France
,
Cédric Fournet
Microsoft Research, n.n.
,
Nikhil Swamy
Microsoft Research, n.n.
DOI
11:15
22m
Talk
Verifying Efficient Function Calls in CakeML
Research Papers
Scott Owens
University of Kent, UK
,
Michael Norrish
Data61 at CSIRO, Australia / Australian National University, Australia
,
Ramana Kumar
Data61 at CSIRO, Australia / UNSW, Australia
,
Magnus O. Myreen
Chalmers University of Technology, Sweden
,
Yong Kiam Tan
Carnegie Mellon University, USA
DOI
11:37
22m
Talk
Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols
Research Papers
Geoffrey Mainland
Drexel University, USA
DOI
13:00 - 14:30
Foundations of Higher-Order Programming
Research Papers
at
L1
Chair(s):
Gabriel Scherer
Northeastern University
13:00
22m
Talk
How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation
Research Papers
Makoto Hamana
Gunma University, Japan
DOI
13:22
22m
Talk
A Relational Logic for Higher-Order Programs
Research Papers
Alejandro Aguirre
IMDEA Software Institute, Spain
,
Gilles Barthe
IMDEA Software Institute, Spain
,
Marco Gaboardi
University at Buffalo, SUNY, USA
,
Deepak Garg
MPI-SWS, Germany
,
Pierre-Yves Strub
École Polytechnique, n.n.
DOI
13:45
22m
Talk
Foundations of Strong Call by Need
Research Papers
Thibaut Balabonski
LRI, France / University of Paris-Sud, France
,
Pablo Barenbaum
University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France
,
Eduardo Bonelli
CONICET, Argentina / Universidad Nacional de Quilmes, Argentina
,
Delia Kesner
Université de Paris, CNRS, IRIF, France
DOI
14:07
22m
Talk
No-Brainer CPS Conversion
Research Papers
Milo Davis
Northeastern University, USA
,
William Meehan
Northeastern University, USA
,
Olin Shivers
Northeastern University, USA
DOI
15:00 - 16:10
Tools for Verification
Research Papers
at
L1
Chair(s):
Nikhil Swamy
Microsoft Research, n.n.
15:00
23m
Talk
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Research Papers
Joonwon Choi
Massachusetts Institute of Technology, USA
,
Muralidaran Vijayaraghavan
Massachusetts Institute of Technology, USA
,
Benjamin Sherman
Massachusetts Institute of Technology, USA
,
Adam Chlipala
Massachusetts Institute of Technology, USA
,
A:
Arvind
Massachusetts Institute of Technology, USA
DOI
15:23
23m
Talk
SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Research Papers
Konstantin Weitz
University of Washington, USA
,
Steven Lyubomirsky
University of Washington, USA
,
Stefan Heule
Stanford University, USA
,
Emina Torlak
University of Washington, USA
,
Michael D. Ernst
University of Washington, USA
,
Zachary Tatlock
University of Washington, Seattle
DOI
15:46
23m
Talk
Local Refinement Typing
Research Papers
Benjamin Cosman
University of California at San Diego, USA
,
Ranjit Jhala
University of California at San Diego, USA
DOI
16:40 - 17:50
Program Construction
Research 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 Events
Keynotes 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 Presentations
Student 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 Languages
Research Papers
at
L1
Chair(s):
Martin Erwig
Oregon State University
09:37
23m
Talk
Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)
Research Papers
Vincent St-Amour
Northwestern University, USA
,
Daniel Feltey
Northwestern University, USA
,
Spencer P. Florence
Northwestern University, USA
,
Shu-Hung You
Northwestern University, USA
,
Robert Bruce Findler
Northwestern University, USA
DOI
10:30 - 12:00
Dependently Typed Programming
Research Papers
at
L1
Chair(s):
Daniel R. Licata
Wesleyan University
10:30
22m
Talk
A Specification for Dependent Types in Haskell
Research Papers
Stephanie Weirich
University of Pennsylvania, USA
,
Antoine Voizard
University of Pennsylvania, USA
,
Pedro Henrique Azevedo de Amorim
Ecole Polytechnique, n.n. / University of Campinas, Brazil
,
Richard A. Eisenberg
Bryn Mawr College, USA
DOI
10:52
22m
Talk
Parametric Quantifiers for Dependent Type Theory
Research Papers
Andreas Nuyts
KU Leuven, Belgium
,
Andrea Vezzosi
Chalmers University of Technology, Sweden
,
Dominique Devriese
KU Leuven, Belgium
DOI
11:15
22m
Talk
Normalization by Evaluation for Sized Dependent Types
Research Papers
Andreas Abel
University of Gothenburg, Sweden
,
Andrea Vezzosi
Chalmers University of Technology, Sweden
,
Théo Winterhalter
ENS Paris-Saclay, France
DOI
11:37
22m
Talk
A Metaprogramming Framework for Formal Verification
Research Papers
Gabriel Ebner
Vienna University of Technology, Austria
,
Sebastian Ullrich
KIT, Germany
,
Jared Roesch
University of Washington, USA
,
Jeremy Avigad
Carnegie Mellon University, USA
,
Leonardo de Moura
Microsoft Research, n.n.
DOI
13:00 - 14:30
Contracts and Sessions
Research Papers
at
L1
Chair(s):
Matthew Flatt
University of Utah
13:00
22m
Talk
Chaperone Contracts for Higher-Order Sessions
Research Papers
Hernan Melgratti
University of Buenos Aires, Argentina
,
Luca Padovani
University of Turin, Italy
DOI
13:22
22m
Talk
Whip: Higher-Order Contracts for Modern Services
Research Papers
Lucas Waye
Harvard University, USA
,
Christos Dimoulas
Harvard University, USA
,
Stephen Chong
Harvard University, USA
DOI
13:45
22m
Talk
Manifest Sharing with Session Types
Research Papers
Stephanie Balzer
Carnegie Mellon University, USA
,
Frank Pfenning
Carnegie Mellon University, USA
DOI
14:07
22m
Talk
Gradual Session Types
Research Papers
Atsushi Igarashi
Kyoto University, Japan
,
Peter Thiemann
University of Freiburg, Germany
,
Vasco T. Vasconcelos
University of Lisbon, Portugal
,
Philip Wadler
University of Edinburgh, UK
DOI
15:00 - 16:10
Integrating Static and Dynamic Typing
Research Papers
at
L1
Chair(s):
Ronald Garcia
University of British Columbia
15:00
23m
Talk
Theorems for Free for Free: Parametricity, With and Without Types
Research Papers
Amal Ahmed
Northeastern University, USA
,
Dustin Jamner
Northeastern University, USA
,
Jeremy G. Siek
Indiana University, USA
,
Philip Wadler
University of Edinburgh, UK
DOI
15:23
23m
Talk
On Polymorphic Gradual Typing
Research Papers
Yuu Igarashi
Kyoto University, Japan
,
Taro Sekiyama
IBM Research, Japan
,
Atsushi Igarashi
Kyoto University, Japan
DOI
15:46
23m
Talk
Gradual Typing with Union and Intersection Types
Research Papers
Giuseppe Castagna
CNRS, France / University of Paris Diderot, France
,
Victor Lanvin
ENS Cachan, France
DOI
16:40 - 17:50
Inference and Analysis
Research Papers
at
L1
Chair(s):
Mark Jones
Portland State University
16:40
23m
Talk
Constrained Type Families
Research Papers
J. Garrett Morris
University of Kansas, USA
,
Richard A. Eisenberg
Bryn Mawr College, USA
DOI
17:03
23m
Talk
Automating Sized-Type Inference for Complexity Analysis
Research Papers
Martin Avanzini
University of Innsbruck, Austria
,
Ugo Dal Lago
University of Bologna, Italy / Inria, France
DOI
17:26
23m
Talk
Inferring Scope through Syntactic Sugar
Research Papers
Justin Pombrio
Brown University, USA
,
Shriram Krishnamurthi
Brown University, USA
,
Mitchell Wand
Northeastern University, USA
DOI
17:50 - 18:00
SRC Awards
Student 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 Events
Keynotes and Reports
at
L1
18:00
10m
Talk
Program Chair's Report
Keynotes and Reports
P:
Mark Jones
Portland State University
18:10
10m
Talk
ICFP 2018 Announcement
Keynotes and Reports
I:
Robert Bruce Findler
Northwestern University, USA
Thu 7 Sep
Displayed time zone:
Belfast
change
09:00 - 10:00
Day 1, Session 1
Haskell
at
L1
09:00
60m
Talk
Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (Invited Talk)
Haskell
Didier Rémy
INRIA
10:30 - 11:30
Day 1, Session 2
Haskell
at
L1
10:30
30m
Talk
Algebraic Graphs with Class (Functional Pearl)
Haskell
Andrey Mokhov
11:00
30m
Talk
Packrats Parse in Packs
Haskell
Mario Blažević
,
Jacques Légaré
12:00 - 12:30
Day 1, Session 3
Haskell
at
L1
12:00
30m
Talk
Ode on a Random Urn (Functional Pearl)
Haskell
Leonidas Lampropoulos
University of Pennsylvania
,
Antal Spector-Zabusky
,
Kenneth Foner
14:00 - 15:00
Day 1, Session 4
Haskell
at
L1
14:00
30m
Demonstration
QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration)
Haskell
Maximilian Algehed
Chalmers University of Technology, Sweden
,
Koen Claessen
Chalmers University of Technology
,
Moa Johansson
Chalmers University of Technology
,
Nicholas Smallbone
14:30
30m
Talk
Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results
Haskell
Rudy Braquehais
,
Colin Runciman
15:30 - 16:30
Day 1, Session 5
Haskell
at
L1
15:30
30m
Talk
Using Coq to Write Fast and Correct Haskell
Haskell
John Wiegley
,
Benjamin Delaware
Purdue University
16:00
30m
Talk
A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq
Haskell
Niki Vazou
University of Maryland
,
Leonidas Lampropoulos
University of Pennsylvania
,
Jeff Polakow
16:50 - 17:50
Day 1, Session 6
Haskell
at
L1
16:50
30m
Talk
A Meta-EDSL for Distributed Web Applications
Haskell
Anton Ekblad
Chalmers University of Technology
17:20
30m
Talk
Composable Network Stacks and Remote Monads
Haskell
Justin Dawson
,
Mark Grebe
,
Andy Gill
Fri 8 Sep
Displayed time zone:
Belfast
change
09:00 - 10:00
Day 2, Session 1
Haskell
at
L1
09:00
60m
Talk
Algorithmic Music in Haskell (Invited Talk)
Haskell
Donya Quick
Stevens Institute of Technology
10:30 - 11:30
Day 2, Session 2
Haskell
at
L1
10:30
30m
Talk
Well-Typed Music Does Not Sound Wrong (Experience Report)
Haskell
Dmitrij Szamozvancev
,
Michael Gale
University of Warwick, UK
11:00
30m
Talk
Back to the Future: Time Travel in FRP
Haskell
Ivan Perez
University of Nottingham, UK
12:00 - 12:30
Day 2, Session 3
Haskell
at
L1
12:00
30m
Talk
The Linearity Monad
Haskell
Jennifer Paykin
University of Pennsylvania
,
Steve Zdancewic
University of Pennsylvania
14:00 - 15:00
Day 2, Session 4
Haskell
at
L1
14:00
30m
Talk
Elaboration on Functional Dependencies
Haskell
Georgios Karachalias
KU Leuven, Belgium
,
Tom Schrijvers
KU Leuven
14:30
30m
Talk
Quantified Class Constraints
Haskell
Gert-Jan Bottu
,
Georgios Karachalias
KU Leuven, Belgium
,
Tom Schrijvers
KU Leuven
,
Bruno C. d. S. Oliveira
University of Hong Kong, China
,
Philip Wadler
University of Edinburgh, UK
15:30 - 16:30
Day 2, Session 5
Haskell
at
L1
15:30
30m
Talk
Hardware Software Co-Design in Haskell
Haskell
Markus Aronsson
,
Mary Sheeran
16:00
30m
Talk
Streaming Irregular Arrays
Haskell
Robert Clifton-Everest
,
Trevor L. McDonell
University of New South Wales, Australia
,
Manuel Chakravarty
,
Gabriele Keller
Data61,CSIRO (formerly NICTA) and UNSW
16:50 - 17:50
Day 2, Session 6
Haskell
at
L1
16:50
30m
Talk
Improving STM Performance with Transactional Structs
Haskell
Ryan Yates
,
Michael Scott
University of Rochester
17:20
30m
Talk
Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping
Haskell
Chao-Hong Chen
Indiana University
,
Vikraman Choudhury
,
Ryan R. Newton
Indiana University
Sat 9 Sep
Displayed time zone:
Belfast
change
09:00 - 10:10
State of GHC
HIW
at
L1
Chair(s):
Richard A. Eisenberg
Bryn Mawr College, USA
09:00
30m
Talk
Progress on GHC
HIW
Simon Peyton Jones
Microsoft Research, Cambridge
09:30
30m
Talk
GHC Infrastructure Update and Discussion
HIW
Ben Gamari
Well-Typed LLP
10:00
10m
Talk
Getting Ready for Hadrian
HIW
Andrey Mokhov
,
Zhen Zhang
University of Washington
,
Ben Gamari
Well-Typed LLP
,
Neil Mitchell
10:30 - 11:30
Compiling to LLVM
HIW
at
L1
Chair(s):
Jan Stolarek
University of Edinburgh, UK
10:30
25m
Talk
Native Support for Explicit Stacks in LLVM
HIW
Kavon Farvardin
University of Chicago
,
Simon Peyton Jones
Microsoft Research, Cambridge
10:55
25m
Talk
SimplexHC: Lowering High-Level Haskell to Imperative IR
HIW
Siddharth Bhat
IIT Hyderabad
11:20
10m
Talk
Lightning Talk Slot #1
HIW
12:00 - 12:25
Constraints
HIW
at
L1
Chair(s):
Ben Gamari
Well-Typed LLP
12:00
25m
Talk
On Unsatisfiability
HIW
J. Garrett Morris
University of Kansas, USA
14:00 - 15:00
Working in Core
HIW
at
L1
Chair(s):
Adam Gundry
Well-Typed LLP
14:00
25m
Talk
Why GHC Core and Linear Logic Should be Best Friends
HIW
Carter Schonwald
,
Joel Burget
14:25
25m
Talk
Demand Analysis vs. Call Arity
HIW
Sebastian Graf
Karlsruhe Institute of Technology
14:50
10m
Talk
Lightning Talk Slot #2
HIW
15:30 - 16:30
Tool Support
HIW
at
L1
Chair(s):
Wren Romano
X
15:30
25m
Talk
IDE Support in GHC
HIW
Alan Zimmerman
15:55
25m
Talk
Tracking GHC Performance
HIW
Mathieu Boespflug
Tweag I/O
,
Manuel Chakravarty
16:20
10m
Talk
Lightning Talk Slot #3
HIW
16:50 - 17:50
All Broken Up
HIW
at
L1
Chair(s):
Bartosz Nitka
Facebook
16:50
25m
Talk
An Experiment in Fragment-Based Code Distribution
HIW
Philipp Schuster
University of Tübingen
17:15
35m
Talk
Lightning Talk Slot #4
HIW
Sun 3 Sep
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
L1
PLMW
Welcome
PLMW
Keynote
PLMW
Session 1
PLMW
Session 2
PLMW
Session 3
PLMW
Session 4
PLMW
Session 5
Mon 4 Sep
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
L1
Keynotes and Reports
Monday Keynote
Research Papers
Art and Education
Research Papers
Functional Programming Techniques
Research Papers
Applications
Research Papers
Effects
Keynotes and Reports
Monday Closing Events
Tue 5 Sep
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
L1
Keynotes and Reports
Tuesday Keynote
Research Papers
Low-level and Systems Programming
Research Papers
Foundations of Higher-Order Programming
Research Papers
Tools for Verification
Research Papers
Program Construction
Keynotes and Reports
Tuesday Closing Events
Wed 6 Sep
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
L1
Student Research Competition
SRC Presentations
Research Papers
Domain-Specific Languages
Research Papers
Dependently Typed Programming
Research Papers
Contracts and Sessions
Research Papers
Integrating Static and Dynamic Typing
Research Papers
Inference and Analysis
Student Research Competition
SRC Awards
Keynotes and Reports
Wednesday Closing Events
Keynotes and Reports
18:10 - 18:20
Thu 7 Sep
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
L1
Haskell
Day 1, Session 1
Haskell
Day 1, Session 2
Haskell
Day 1, Session 3
Haskell
Day 1, Session 4
Haskell
Day 1, Session 5
Haskell
Day 1, Session 6
Fri 8 Sep
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
L1
Haskell
Day 2, Session 1
Haskell
Day 2, Session 2
Haskell
Day 2, Session 3
Haskell
Day 2, Session 4
Haskell
Day 2, Session 5
Haskell
Day 2, Session 6
Sat 9 Sep
Displayed time zone:
Belfast
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
L1
HIW
State of GHC
HIW
Compiling to LLVM
HIW
Constraints
HIW
Working in Core
HIW
Tool Support
HIW
All Broken Up
Sun 3 Sep
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
L1
PLMW
Welcome
09:00 - 09:10
PLMW
Keynote
09:10 - 10:00
PLMW
A Few Frank Remarks
10:30 - 11:00
PLMW
Compositional Compiler Correctness
11:00 - 11:30
PLMW
Not How To Do Your PhD
12:00 - 12:30
PLMW
Gradual Typing
14:00 - 14:30
PLMW
Scala: Types in Theory & Practice
14:30 - 15:00
PLMW
How to Write Papers and Give Talks That People Can Follow
15:30 - 16:30
PLMW
Panel Discussion: Careers in Programming Languages
16:50 - 17:40
Mon 4 Sep
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
L1
ICFP Keynotes and Reports
Keynote
Compositional creativity: some principles for talking to computers
09:00 - 10:00
ICFP Research Papers
Super 8 Languages for Making Movies (Functional Pearl)
10:30 - 10:52
ICFP Research Papers
Testing and Debugging Functional Reactive Programming
10:52 - 11:15
ICFP Research Papers
Lock-Step Simulation Is Child's Play (Experience Report)
11:15 - 11:37
ICFP Research Papers
Scaling up Functional Programming Education: Under the Hood of the OCam ...
11:37 - 12:00
ICFP Research Papers
Faster Coroutine Pipelines
13:00 - 13:22
ICFP Research Papers
A Pretty But Not Greedy Printer (Functional Pearl)
13:22 - 13:45
ICFP Research Papers
Generic Functional Parallel Algorithms: Scan and FFT
13:45 - 14:07
ICFP Research Papers
A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
14:07 - 14:30
ICFP Research Papers
Prototyping a Query Compiler using Coq (Experience Report)
15:00 - 15:23
ICFP Research Papers
A Framework for Adaptive Differential Privacy
15:23 - 15:46
ICFP Research Papers
Symbolic Conditioning of Arrays in Probabilistic Programs
15:46 - 16:10
ICFP Research Papers
Abstracting Definitional Interpreters
16:40 - 17:02
ICFP Research Papers
On the Expressive Power of User-Defined Effects: Effect Handlers, Monad ...
17:02 - 17:25
ICFP Research Papers
Imperative Functional Programs That Explain Their Work
17:25 - 17:47
ICFP Research Papers
Effect-Driven QuickChecking of Compilers
17:47 - 18:10
ICFP Keynotes and Reports
Monday Announcements
18:10 - 18:20
Tue 5 Sep
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
L1
ICFP Keynotes and Reports
Keynote
Assuring AI
09:00 - 10:00
ICFP Research Papers
Persistence for the Masses: RRB-Vectors in a Systems Language
10:30 - 10:52
ICFP Research Papers
Verified Low-Level Programming Embedded in F*
10:52 - 11:15
ICFP Research Papers
Verifying Efficient Function Calls in CakeML
11:15 - 11:37
ICFP Research Papers
Better Living through Operational Semantics: An Optimizing Compiler for ...
11:37 - 12:00
ICFP Research Papers
How to Prove Your Calculus Is Decidable: Practical Applications of Seco ...
13:00 - 13:22
ICFP Research Papers
A Relational Logic for Higher-Order Programs
13:22 - 13:45
ICFP Research Papers
Foundations of Strong Call by Need
13:45 - 14:07
ICFP Research Papers
No-Brainer CPS Conversion
14:07 - 14:30
ICFP Research Papers
Kami: A Platform for High-Level Parametric Hardware Specification and I ...
15:00 - 15:23
ICFP Research Papers
SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
15:23 - 15:46
ICFP Research Papers
Local Refinement Typing
15:46 - 16:10
ICFP Research Papers
Compiling to Categories
16:40 - 17:03
ICFP Research Papers
Visitors Unchained
17:03 - 17:26
ICFP Research Papers
Staged Generic Programming
17:26 - 17:50
ICFP Keynotes and Reports
Programming Contest Report
17:50 - 18:20
Wed 6 Sep
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
L1
ICFP Student Research Competition
Student Research Competition: Finalist Presentations
09:00 - 09:37
ICFP Research Papers
Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)
09:37 - 10:00
ICFP Research Papers
A Specification for Dependent Types in Haskell
10:30 - 10:52
ICFP Research Papers
Parametric Quantifiers for Dependent Type Theory
10:52 - 11:15
ICFP Research Papers
Normalization by Evaluation for Sized Dependent Types
11:15 - 11:37
ICFP Research Papers
A Metaprogramming Framework for Formal Verification
11:37 - 12:00
ICFP Research Papers
Chaperone Contracts for Higher-Order Sessions
13:00 - 13:22
ICFP Research Papers
Whip: Higher-Order Contracts for Modern Services
13:22 - 13:45
ICFP Research Papers
Manifest Sharing with Session Types
13:45 - 14:07
ICFP Research Papers
Gradual Session Types
14:07 - 14:30
ICFP Research Papers
Theorems for Free for Free: Parametricity, With and Without Types
15:00 - 15:23
ICFP Research Papers
On Polymorphic Gradual Typing
15:23 - 15:46
ICFP Research Papers
Gradual Typing with Union and Intersection Types
15:46 - 16:10
ICFP Research Papers
Constrained Type Families
16:40 - 17:03
ICFP Research Papers
Automating Sized-Type Inference for Complexity Analysis
17:03 - 17:26
ICFP Research Papers
Inferring Scope through Syntactic Sugar
17:26 - 17:50
ICFP Student Research Competition
Student Research Competition Awards
17:50 - 18:00
ICFP Keynotes and Reports
Program Chair's Report
18:00 - 18:10
ICFP Keynotes and Reports
ICFP 2018 Announcement
18:10 - 18:20
Thu 7 Sep
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
L1
Haskell
Ornaments: exploiting parametricity for safer, more automated code refa ...
09:00 - 10:00
Haskell
Algebraic Graphs with Class (Functional Pearl)
10:30 - 11:00
Haskell
Packrats Parse in Packs
11:00 - 11:30
Haskell
Ode on a Random Urn (Functional Pearl)
12:00 - 12:30
Haskell
QuickSpec: A Lightweight Theory Exploration Tool for Programmers (Syste ...
14:00 - 14:30
Haskell
Speculate: Discovering Conditional Equations and Inequalities about Bla ...
14:30 - 15:00
Haskell
Using Coq to Write Fast and Correct Haskell
15:30 - 16:00
Haskell
A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Has ...
16:00 - 16:30
Haskell
A Meta-EDSL for Distributed Web Applications
16:50 - 17:20
Haskell
Composable Network Stacks and Remote Monads
17:20 - 17:50
Fri 8 Sep
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
L1
Haskell
Algorithmic Music in Haskell (Invited Talk)
09:00 - 10:00
Haskell
Well-Typed Music Does Not Sound Wrong (Experience Report)
10:30 - 11:00
Haskell
Back to the Future: Time Travel in FRP
11:00 - 11:30
Haskell
The Linearity Monad
12:00 - 12:30
Haskell
Elaboration on Functional Dependencies
14:00 - 14:30
Haskell
Quantified Class Constraints
14:30 - 15:00
Haskell
Hardware Software Co-Design in Haskell
15:30 - 16:00
Haskell
Streaming Irregular Arrays
16:00 - 16:30
Haskell
Improving STM Performance with Transactional Structs
16:50 - 17:20
Haskell
Adaptive Lock-Free Data Structures in Haskell: A General Method for Con ...
17:20 - 17:50
Sat 9 Sep
Displayed time zone:
Belfast
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
L1
HIW
Progress on GHC
09:00 - 09:30
HIW
GHC Infrastructure Update and Discussion
09:30 - 10:00
HIW
Getting Ready for Hadrian
10:00 - 10:10
HIW
Native Support for Explicit Stacks in LLVM
10:30 - 10:55
HIW
SimplexHC: Lowering High-Level Haskell to Imperative IR
10:55 - 11:20
HIW
Lightning Talk Slot #1
11:20 - 11:30
HIW
On Unsatisfiability
12:00 - 12:25
HIW
Why GHC Core and Linear Logic Should be Best Friends
14:00 - 14:25
HIW
Demand Analysis vs. Call Arity
14:25 - 14:50
HIW
Lightning Talk Slot #2
14:50 - 15:00
HIW
IDE Support in GHC
15:30 - 15:55
HIW
Tracking GHC Performance
15:55 - 16:20
HIW
Lightning Talk Slot #3
16:20 - 16:30
HIW
An Experiment in Fragment-Based Code Distribution
16:50 - 17:15
HIW
Lightning Talk Slot #4
17:15 - 17:50
x
Sat 14 Dec 18:23