Scheme 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
co-located with ICFP 2017
VenueMathematical Institute
Room nameL1
Floor0
Capacity360
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

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

Mon 4 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Monday KeynoteICFP 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 computersKeynote
ICFP Keynotes and Reports
K: Chris Martens North Carolina State University
10:30 - 12:00
Art and EducationICFP Research Papers at L1
Chair(s): Kathryn E. Gray University of Cambridge
10:30
22m
Talk
Super 8 Languages for Making Movies (Functional Pearl)
ICFP 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
ICFP 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)
ICFP 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
ICFP 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 TechniquesICFP Research Papers at L1
Chair(s): Graham Hutton University of Nottingham
13:00
22m
Talk
Faster Coroutine Pipelines
ICFP Research Papers
Mike Spivey University of Oxford, UK
DOI
13:22
22m
Talk
A Pretty But Not Greedy Printer (Functional Pearl)
ICFP Research Papers
Jean-Philippe Bernardy University of Gothenburg
DOI
13:45
22m
Talk
Generic Functional Parallel Algorithms: Scan and FFT
ICFP Research Papers
Conal Elliott Target, USA
DOI
14:07
22m
Talk
A Unified Approach to Solving Seven Programming Problems (Functional Pearl)
ICFP 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
ApplicationsICFP Research Papers at L1
Chair(s): Alexandra Silva University College London
15:00
23m
Talk
Prototyping a Query Compiler using Coq (Experience Report)
ICFP 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
ICFP 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
ICFP Research Papers
Praveen Narayanan Indiana University, USA, Chung-chieh Shan Indiana University, USA
DOI
16:40 - 18:10
EffectsICFP Research Papers at L1
Chair(s): Ben Lippmeier Digital Asset / UNSW Australia
16:40
22m
Talk
Abstracting Definitional Interpreters
ICFP 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
ICFP 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
ICFP 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
ICFP 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 EventsICFP Keynotes and Reports at L1
Chair(s): Peter Thiemann University of Freiburg, Germany
18:10
10m
Day closing
Monday Announcements
ICFP Keynotes and Reports

Tue 5 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Tuesday KeynoteICFP Keynotes and Reports at L1
Chair(s): Mark Jones Portland State University
09:00
60m
Talk
Assuring AIKeynote
ICFP Keynotes and Reports
I: John Launchbury Galois, Inc.
10:30 - 12:00
Low-level and Systems ProgrammingICFP 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
ICFP 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*
ICFP 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
ICFP 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
ICFP Research Papers
Geoffrey Mainland Drexel University, USA
DOI
13:00 - 14:30
Foundations of Higher-Order ProgrammingICFP 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
ICFP Research Papers
Makoto Hamana Gunma University, Japan
DOI
13:22
22m
Talk
A Relational Logic for Higher-Order Programs
ICFP 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
ICFP 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
ICFP Research Papers
Milo Davis Northeastern University, USA, William Meehan Northeastern University, USA, Olin Shivers Northeastern University, USA
DOI
15:00 - 16:10
Tools for VerificationICFP 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
ICFP 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
ICFP 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
ICFP 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 ConstructionICFP Research Papers at L1
Chair(s): John Hughes Chalmers University of Technology
16:40
23m
Talk
Compiling to Categories
ICFP Research Papers
Conal Elliott Target, USA
DOI
17:03
23m
Talk
Visitors Unchained
ICFP Research Papers
François Pottier Inria, France
DOI
17:26
23m
Talk
Staged Generic Programming
ICFP Research Papers
Jeremy Yallop University of Cambridge, UK
DOI Pre-print
17:50 - 18:20
Tuesday Closing EventsICFP Keynotes and Reports at L1
17:50
30m
Talk
Programming Contest Report
ICFP Keynotes and Reports
P: Sam Lindley University of Edinburgh, UK

Wed 6 Sep

Displayed time zone: Belfast change

09:00 - 09:37
SRC PresentationsICFP Student Research Competition at L1
Chair(s): Ilya Sergey University College London
09:00
37m
Awards
Student Research Competition: Finalist Presentations
ICFP Student Research Competition

09:37 - 10:00
Domain-Specific LanguagesICFP Research Papers at L1
Chair(s): Martin Erwig Oregon State University
09:37
23m
Talk
Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)
ICFP 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 ProgrammingICFP Research Papers at L1
Chair(s): Daniel R. Licata Wesleyan University
10:30
22m
Talk
A Specification for Dependent Types in Haskell
ICFP 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
ICFP 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
ICFP Research Papers
Andreas Abel University of Gothenburg, Sweden, Andrea Vezzosi Chalmers University of Technology, Sweden, Theo Winterhalter ENS Paris-Saclay, France
DOI
11:37
22m
Talk
A Metaprogramming Framework for Formal Verification
ICFP 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 SessionsICFP Research Papers at L1
Chair(s): Matthew Flatt University of Utah
13:00
22m
Talk
Chaperone Contracts for Higher-Order Sessions
ICFP 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
ICFP 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
ICFP Research Papers
Stephanie Balzer Carnegie Mellon University, USA, Frank Pfenning Carnegie Mellon University, USA
DOI
14:07
22m
Talk
Gradual Session Types
ICFP 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 TypingICFP 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
ICFP 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
ICFP 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
ICFP Research Papers
Giuseppe Castagna CNRS, France / University of Paris Diderot, France, Victor Lanvin ENS Cachan, France
DOI
16:40 - 17:50
Inference and AnalysisICFP Research Papers at L1
Chair(s): Mark Jones Portland State University
16:40
23m
Talk
Constrained Type Families
ICFP 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
ICFP 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
ICFP Research Papers
Justin Pombrio Brown University, USA, Shriram Krishnamurthi Brown University, USA, Mitchell Wand Northeastern University, USA
DOI
17:50 - 18:00
SRC AwardsICFP Student Research Competition at L1
Chair(s): Ilya Sergey University College London
17:50
10m
Awards
Student Research Competition Awards
ICFP Student Research Competition
S: Ilya Sergey University College London
18:00 - 18:20
Wednesday Closing EventsICFP Keynotes and Reports at L1
18:00
10m
Talk
Program Chair's Report
ICFP Keynotes and Reports
P: Mark Jones Portland State University
18:10
10m
Talk
ICFP 2018 Announcement
ICFP Keynotes and Reports
I: Robert Bruce Findler Northwestern University, USA

Thu 7 Sep

Displayed time zone: Belfast change

12:00 - 12:30
Day 1, Session 3Haskell at L1
12:00
30m
Talk
Ode on a Random Urn (Functional Pearl)
Haskell
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
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

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

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

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

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

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

Sun 3 Sep

Displayed time zone: Belfast change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
L1

Thu 7 Sep

Displayed time zone: Belfast change

Fri 8 Sep

Displayed time zone: Belfast change

Sat 9 Sep

Displayed time zone: Belfast change

Sun 3 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
L1
PLMW
Welcome
09:00 - 09:10
PLMW
Keynote
09:10 - 10:00
PLMW
Gradual Typing
14:00 - 14:30

Mon 4 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
L1

Wed 6 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
L1