ICFP 2017 Program

09:00 - 09:10: PLMW 2017 - Welcome at L1
Chair(s): Brigitte PientkaMcGill University

09:00 - 09:10
Talk

Brigitte PientkaMcGill University, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Dan LicataWesleyan University

09:00 - 09:05: TyDe 2017 - Welcome at L2

09:00 - 09:05
Day opening

Sam LindleyUniversity of Edinburgh, UK, Brent YorgeyHendrix College

09:00 - 09:10: HOPE 2017 - Welcome at L3

09:00 - 09:10
Day opening

Invited Talk: Semantics of Effect Systems by Graded Monads

François PottierInria, France, Aleksandar NanevskiIMDEA Software Institute

09:05 - 10:00: TyDe 2017 - Invited talk at L2

09:05 - 10:00
Talk

Driving types into PHP

Andrew KennedyFacebook London

09:10 - 10:00: HOPE 2017 - Invited talk at L3

09:10 - 10:10
Talk

Shin-ya KatsumataNational Institute of Informatics

09:10 - 10:00: PLMW 2017 - Keynote at L1
Chair(s): Neel KrishnaswamiComputer Laboratory, University of Cambridge

09:10 - 10:00
Talk

Keynote

Chris MartensNorth Carolina State University

09:10 - 10:10: Scheme 2017 - Session 1 at L4

09:10 - 10:10
Talk

Keynote

Sam Tobin-HochstadtIndiana University

10:00 - 10:30: Catering - Sunday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Sunday coffee break 1

10:30 - 11:30: TyDe 2017 - Full papers 1 at L2

10:30 - 11:00
Talk

Generic packet descriptions: verified parsing and pretty printing of low-level data

Marcell van GeestUtrecht University, Wouter SwierstraUniversity of Utrecht

11:00 - 11:30
Talk

Structured asynchrony with algebraic effects

Daan LeijenMicrosoft Research

10:30 - 11:30: HOPE 2017 - Modular Semantics at L3

10:30 - 11:00
Talk

Higher-order Programming is an Effect

A monadic solution to the Cartwright-Felleisen-Wadler conjecture

11:00 - 11:30
Talk

Ohad KammarUniversity of Oxford, UK, Dylan McDermottUniversity of Cambridge

Tutorial T1: Writing Verified Programs in CakeML (part 2)

10:30 - 11:30: Tutorials - Morning tutorial session 2 at L5

10:30 - 11:30
Talk

10:30 - 11:30: PLMW 2017 - Session 1 at L1

10:30 - 11:00
Talk

A Few Frank Remarks

Conor McBride

11:00 - 11:30
Talk

Compositional Compiler Correctness

Amal AhmedNortheastern University, USA

Paper: Scalar and Tensor Parameters for Importing Tensor Index Notation including Einstein Summation Notation

10:30 - 11:30: Scheme 2017 - Session 2 at L4

10:30 - 11:15
Talk

Satoshi EgiRakuten Institute of Technology

11:15 - 11:30
Talk

Lightning Talk: Extending the LISP model from cons cells to triples, from trees to hypergraphs

Joe Corneli, Raymond Puzio

11:20 - 12:00: Catering - Sunday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Sunday coffee break 2

12:00 - 12:25: TyDe 2017 - Extended abstracts 1 at L2

12:00 - 12:25
Talk

Cogent⇑: giving systems engineers a stepping stone

Zilin ChenUNSW, Australia

12:00 - 12:30: Tutorials - Morning tutorial session 3 at L5

12:00 - 12:30
Talk

Tutorial T1: Writing Verified Programs in CakeML (part 3)

12:00 - 12:30: HOPE 2017 - Rust at L3

12:00 - 12:30
Talk

RustBelt: Securing the Foundations of the Rust Programming Language

Ralf JungMPI-SWS, Germany, Jacques-Henri JourdanMPI-SWS, Germany, Robbert KrebbersDelft University of Technology, Netherlands, Derek DreyerMPI-SWS

12:00 - 12:30: PLMW 2017 - Session 2 at L1

12:00 - 12:30
Talk

Not How To Do Your PhD

Gabriel SchererNortheastern University

Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL

12:00 - 12:30: Scheme 2017 - Session 3 at L4

12:00 - 12:30
Talk

Panel: Future of Scheme

François-René Rideau, Marc FeeleyUniversité de Montréal, Arthur GlecklerSRFI Editor, Kathy Gray, Alaric Snell-Pym, Andy WingoIgalia, S.L.

12:25 - 14:00: Catering - Sunday lunch at Catering

12:25 - 14:00
Lunch

Sunday lunch

14:00 - 15:00: Tutorials - Afternoon tutorial session 1 at L5

14:00 - 15:00
Talk

Jasmin BlanchetteVrije Universiteit Amsterdam, Andreas Lochbihler, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH Zurich

14:00 - 15:00: HOPE 2017 - Effects and Dependent Types at L3

14:00 - 14:30
Talk

Handling fibred algebraic effects

Danel AhmanUniversity of Edinburgh

14:30 - 15:00
Talk

Only Control Effects and Dependent Types

Youyou CongOchanomizu University, William J. BowmanNortheastern University

14:00 - 15:00: TyDe 2017 - Full papers 2 at L2

14:00 - 14:30
Talk

Type safe Redis queries -- a case study of type-level programming in Haskell

Ting-Yan LaiInstitute of Information Science, Academia Sinica, Tyng-Ruey ChuangInstitute of Information Science, Academia Sinica, Shin-Cheng MuAcademia Sinica, Taiwan

14:30 - 15:00
Talk

Type-directed diffing of structured data

Victor Cacciari MiraldoUniversity of Utrecht, Pierre-Evariste DagandLIP6/CNRS , Wouter SwierstraUniversity of Utrecht

14:00 - 15:00: PLMW 2017 - Session 3 at L1

14:00 - 14:30
Talk

Gradual Typing

Ronald GarciaUniversity of British Columbia

Scala: Types in Theory & Practice

14:30 - 15:00
Talk

Nada AminUniversity of Cambridge

Paper: Toward Parallelizing Control-flow Analysis with Datalog

14:00 - 15:00: Scheme 2017 - Session 4 at L4

14:00 - 14:45
Talk

Thomas GilrayUniversity of Utah, USA, Sidharth Kumar

14:45 - 15:00
Talk

Lightning: Gerbil on Gambit, as they say Racket on Chez

Dimitris Vyzovitis

14:50 - 15:30: Catering - Sunday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Sunday coffee break 3

15:30 - 16:20: Tutorials - Afternoon tutorial session 2 at L5

15:30 - 16:20
Talk

Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 2)

Jasmin BlanchetteVrije Universiteit Amsterdam, Andreas Lochbihler, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH Zurich

15:30 - 16:30: HOPE 2017 - Effects at L3

15:30 - 16:00
Talk

Programming a Web Server with Algebraic Effects

Daan LeijenMicrosoft Research

16:00 - 16:30
Talk

Logical Relations for Algebraic Effects

Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr Polesiuk, Filip SieczkowskiUniversity of Wrocław

15:30 - 16:20: TyDe 2017 - Extended abstracts 2 at L2

15:30 - 15:55
Talk

Affine killing

Kiko Fernandez-ReyesUppsala University, Dave ClarkeUppsala Univ. Sweden and KU Leuvern

15:55 - 16:20
Talk

On ringads and foldables

James McKinnaUniversity of Edinburgh

15:30 - 16:30: PLMW 2017 - Session 4 at L1

15:30 - 16:30
Talk

How to Write Papers and Give Talks That People Can Follow

Derek DreyerMPI-SWS

Media Attached

15:30 - 16:30: Scheme 2017 - Session 5 at L4

15:30 - 16:15
Talk

Report: Status of the ongoing R7RS standardization process

Alaric Snell-Pym

16:15 - 16:30
Talk

Lightning: {lambda talk}

Alain Marty

16:20 - 16:50: Catering - Sunday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Sunday coffee break 4

16:50 - 17:50: Tutorials - Afternoon tutorial session 3 at L5

16:50 - 17:50
Talk

Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL (part 3)

Jasmin BlanchetteVrije Universiteit Amsterdam, Andreas Lochbihler, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH Zurich

16:50 - 17:40: TyDe 2017 - Extended abstracts 3 at L2

16:50 - 17:15
Talk

Type oriented programming for task based parallelism

Nick BrownEPCC, Ludovic CapelliEPCC, James Mark BullEPCC

17:15 - 17:40
Talk

Type-directed reasoning for probabilistic, non-compositional resources

Edwin BradyUniversity of St. Andrews, UK, Kevin HammondUniversity of St. Andrews, UK, Christopher SchwaabUniversity of St Andrews

16:50 - 17:40: HOPE 2017 - Monotonicity at L3

16:50 - 17:20
Talk

Recalling a Witness

Danel AhmanUniversity of Edinburgh, Cătălin HriţcuInria Paris, Kenji MaillardInria Paris, ENS Paris, and Microsoft Research, Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, n.n., Cédric FournetMicrosoft Research, n.n.

Panel Discussion: Careers in Programming Languages

16:50 - 17:40: PLMW 2017 - Session 5 at L1

16:50 - 17:40
Talk

Sam StatonUniversity of Oxford, Richard A. EisenbergBryn Mawr College, USA, Andreas RossbergGoogle, Daan Leijen, Amal AhmedNortheastern University, USA

16:50 - 17:50: Scheme 2017 - Session 6 at L4

16:50 - 17:40
Talk

Invited Talk

Matthew MightUniversity of Utah, USA

17:40 - 17:50
Day closing

Goodbye

Mon 4 Sep

09:00 - 10:00: Keynotes and Reports - Monday Keynote at L1
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford

09:00 - 10:00
Talk

Compositional creativity: some principles for talking to computersKeynote

Chris MartensNorth Carolina State University

10:00 - 10:30: Catering - Monday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Monday coffee break 1

10:30 - 12:00: Research Papers - Art and Education at L1
Chair(s): Kathryn E. GrayUniversity of Cambridge

10:30 - 10:52
Talk

Super 8 Languages for Making Movies (Functional Pearl)

Leif AndersenNortheastern University, USA, Stephen ChangNortheastern University, USA, Matthias FelleisenNortheastern University, USA

Testing and Debugging Functional Reactive Programming

10:52 - 11:15
Talk

Ivan PerezUniversity of Nottingham, UK, Henrik NilssonUniversity of Nottingham, UK

Lock-Step Simulation Is Child's Play (Experience Report)

11:15 - 11:37
Talk

Joachim BreitnerUniversity of Pennsylvania, Chris SmithGoogle, USA

Scaling up Functional Programming Education: Under the Hood of the OCaml MOOC

11:37 - 12:00
Talk

Benjamin CanouOCamlPro, n.n., Roberto Di CosmoInria, France / University of Paris Diderot, France, Grégoire HenryOCamlPro, n.n.

Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages

10:30 - 10:45: FSCD 2017 - Welcome at L2

10:30 - 10:45
Other

Welcome message

Sam StatonUniversity of Oxford, Dale MillerINRIA Saclay and LIX

10:45 - 11:45: FSCD 2017 - Session 1 at L2

10:45 - 11:45
Talk

Alexandra SilvaUniversity College London

12:00 - 13:00: Catering - Monday lunch at Catering

12:00 - 13:00
Lunch

Monday lunch

13:00 - 14:30: Research Papers - Functional Programming Techniques at L1
Chair(s): Graham HuttonUniversity of Nottingham

13:00 - 13:22
Talk

Faster Coroutine Pipelines

Mike SpiveyUniversity of Oxford, UK

A Pretty But Not Greedy Printer (Functional Pearl)

13:22 - 13:45
Talk

Jean-Philippe BernardyUniversity of Gothenburg

Generic Functional Parallel Algorithms: Scan and FFT

13:45 - 14:07
Talk

Conal ElliottTarget, USA

A Unified Approach to Solving Seven Programming Problems (Functional Pearl)

14:07 - 14:30
Talk

William E. ByrdUniversity of Utah, USA, Michael BallantyneUniversity of Utah, USA, Gregory Rosenblattn.n., n.n., Matthew MightUniversity of Utah, USA

Polynomial running times for polynomial-time oracle machines

13:00 - 14:30: FSCD 2017 - Session 2 at L2

13:00 - 13:30
Talk

Akitoshi Kawamura, Florian Steinberg

13:30 - 14:00
Talk

A Curry-Howard Approach to Church’s Synthesis

Colin Riba, Pierre Pradic

14:00 - 14:30
Talk

Streett Automata Model Checking of Higher-Order Recursion Schemes

Ryota Suzuki, Koichi Fujima, Naoki KobayashiUniversity of Tokyo, Japan, Takeshi TsukadaUniversity of Tokyo, Japan

14:30 - 15:00: Catering - Monday coffee break 2 at Catering

14:30 - 15:00
Coffee break

Monday coffee break 2

15:00 - 16:10: Research Papers - Applications at L1
Chair(s): Alexandra SilvaUniversity College London

15:00 - 15:23
Talk

Prototyping a Query Compiler using Coq (Experience Report)

Joshua AuerbachIBM Research, Martin HirzelIBM Research, Louis MandelIBM Research, Avraham ShinnarIBM Research, Jerome SimeonIBM Research

A Framework for Adaptive Differential Privacy

15:23 - 15:46
Talk

Daniel Winograd-CortUniversity of Pennsylvania, USA, Andreas HaeberlenUniversity of Pennsylvania, USA, Aaron RothUniversity of Pennsylvania, USA, Benjamin C. PierceUniversity of Pennsylvania

Symbolic Conditioning of Arrays in Probabilistic Programs

15:46 - 16:10
Talk

Praveen NarayananIndiana University, USA, Chung-chieh ShanIndiana University, USA

Relating System F and λ2: A Case Study in Coq, Abella and Beluga

15:00 - 16:00: FSCD 2017 - Session 3 at L2

15:00 - 15:30
Talk

Jonas Kaiser, Brigitte PientkaMcGill University, Gert SmolkaSaarland University

15:30 - 16:00
Talk

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL

Jasmin BlanchetteVrije Universiteit Amsterdam, Mathias FleuryMPI-INF, Dmitriy TraytelETH Zurich

16:10 - 16:40: Catering - Monday coffee break 3 at Catering

16:10 - 16:40
Coffee break

Monday coffee break 3

16:40 - 18:10: Research Papers - Effects at L1
Chair(s): Ben LippmeierDigital Asset / UNSW Australia

16:40 - 17:02
Talk

Abstracting Definitional Interpreters

David DaraisUniversity of Maryland, USA, Nicholas LabichUniversity of Maryland, USA, Phúc C. NguyễnUniversity of Maryland, USA, David Van HornUniversity of Maryland, USA

On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control

17:02 - 17:25
Talk

Yannick ForsterSaarland University, Germany / University of Cambridge, UK, Ohad KammarUniversity of Oxford, UK, Sam LindleyUniversity of Edinburgh, UK, Matija PretnarUniversity of Ljubljana, Slovenia

Imperative Functional Programs That Explain Their Work

17:25 - 17:47
Talk

Wilmer RicciottiUniversity of Edinburgh, UK, Jan StolarekUniversity of Edinburgh, UK, Roly PereraUniversity of Edinburgh, UK / University of Glasgow, UK, James CheneyUniversity of Edinburgh, UK

Effect-Driven QuickChecking of Compilers

17:47 - 18:10
Talk

Jan MidtgaardDTU, Denmark, Mathias Nygaard JustesenDTU, Denmark, Patrick KastingDTU, Denmark, Flemming NielsonDTU, Denmark, Hanne Riis NielsonDTU, Denmark

A polynomial-time algorithm for the Lambek calculus with brackets of bounded order

16:40 - 18:10: FSCD 2017 - Session 4 at L2

16:40 - 17:10
Talk

Max Kanovich, Stepan Kuznetsov, Glyn Morrill, Andre Scedrov

17:10 - 17:40
Talk

A sequent calculus for semi-associativity

Noam ZeilbergerUniversity of Birmingham, UK

17:40 - 18:10
Talk

Combinatorial Flows and their Normalisation

Lutz Strassburger

18:10 - 18:20: Keynotes and Reports - Monday Closing Events at L1
Chair(s): Peter ThiemannUniversity of Freiburg, Germany

18:10 - 18:20
Day closing

Monday Announcements

18:30 - 20:30: Social Events - Welcome Reception at Foyer

18:30 - 20:30
Social Event

Welcome Reception

Tue 5 Sep

09:00 - 10:00: Keynotes and Reports - Tuesday Keynote at L1
Chair(s): Mark JonesPortland State University

09:00 - 10:00
Talk

Assuring AIKeynote

John LaunchburyGalois, Inc.

10:00 - 10:30: Catering - Tuesday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Tuesday coffee break 1

10:30 - 12:00: Research Papers - Low-level and Systems Programming at L1
Chair(s): Sam Tobin-HochstadtIndiana University

10:30 - 10:52
Talk

Persistence for the Masses: RRB-Vectors in a Systems Language

Juan Pedro Bolívar PuenteIndependent Consultant, Sinusoidal Engineering

DOI Pre-print

10:52 - 11:15
Talk

Verified Low-Level Programming Embedded in F*

Jonathan ProtzenkoMicrosoft Research, n.n., Jean-Karim ZinzindohouéInria, France, Aseem RastogiMicrosoft Research, Tahina RamananandroMicrosoft Research, n.n., Peng WangMassachusetts Institute of Technology, USA, Santiago Zanella-BéguelinMicrosoft Research, n.n., Antoine Delignat-LavaudMicrosoft Research, n.n., Cătălin HriţcuInria Paris, Karthikeyan BhargavanInria, France, Cédric FournetMicrosoft Research, n.n., Nikhil SwamyMicrosoft Research, n.n.

Verifying Efficient Function Calls in CakeML

11:15 - 11:37
Talk

Scott OwensUniversity of Kent, UK, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia, Ramana KumarData61 at CSIRO, Australia / UNSW, Australia, Magnus O. MyreenChalmers University of Technology, Sweden, Yong Kiam TanCarnegie Mellon University, USA

Better Living through Operational Semantics: An Optimizing Compiler for Radio Protocols

11:37 - 12:00
Talk

Geoffrey MainlandDrexel University, USA

Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses

10:30 - 11:30: FSCD 2017 - Session 5 at L2

10:30 - 11:30
Talk

Georg MoserUniversity of Innsbruck

11:30 - 12:00: FSCD 2017 - Session 6 at L2

11:30 - 12:00
Talk

Continuation Passing Style for Effect Handlers

Daniel HillerströmThe University of Edinburgh, Sam LindleyUniversity of Edinburgh, UK, Robert AtkeyUniversity of Strathclyde, KC SivaramakrishnanUniversity of Cambridge

12:00 - 13:00: Catering - Tuesday lunch at Catering

12:00 - 13:00
Lunch

Tuesday lunch

13:00 - 14:30: Research Papers - Foundations of Higher-Order Programming at L1
Chair(s): Gabriel SchererNortheastern University

13:00 - 13:22
Talk

How to Prove Your Calculus Is Decidable: Practical Applications of Second-Order Algebraic Theories and Computation

Makoto HamanaGunma University, Japan

A Relational Logic for Higher-Order Programs

13:22 - 13:45
Talk

Alejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Spain, Marco GaboardiUniversity at Buffalo, SUNY, USA, Deepak GargMPI-SWS, Germany, Pierre-Yves StrubÉcole Polytechnique, n.n.

Foundations of Strong Call by Need

13:45 - 14:07
Talk

Thibaut BalabonskiLRI, France / University of Paris-Sud, France, Pablo BarenbaumUniversity of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo BonelliCONICET, Argentina / Universidad Nacional de Quilmes, Argentina, Delia KesnerIRIF, France / University of Paris Diderot, France

No-Brainer CPS Conversion

14:07 - 14:30
Talk

Milo DavisNortheastern University, USA, William MeehanNortheastern University, USA, Olin ShiversNortheastern University, USA

Confluence of an extension of Combinatory Logic by Boolean constants

13:00 - 14:30: FSCD 2017 - Session 7 at L2

13:00 - 13:30
Talk

Lukasz CzajkaUniversity of Innsbruck

13:30 - 14:00
Talk

Improving Rewriting Induction Approach for Proving Ground Confluence

Takahito Aoto, Yoshihito Toyama, Yuta Kimura

14:00 - 14:30
Talk

The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal type

Yohji Akama

14:30 - 15:00: Catering - Tuesday coffee break 2 at Catering

14:30 - 15:00
Coffee break

Tuesday coffee break 2

15:00 - 16:00: FSCD 2017 - Session 8 at L2

15:00 - 15:30
Talk

Is the optimal implementation inefficient? Elementarily not

Stefano Guerrini, Marco SolieriUniversity of Bath

15:30 - 16:00
Talk

Optimality and the Linear Substitution Calculus

Pablo BarenbaumUniversity of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, Eduardo BonelliCONICET, Argentina / Universidad Nacional de Quilmes, Argentina

15:00 - 16:10: Research Papers - Tools for Verification at L1
Chair(s): Nikhil SwamyMicrosoft Research, n.n.

15:00 - 15:23
Talk

Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification

Joonwon ChoiMassachusetts Institute of Technology, USA, Muralidaran VijayaraghavanMassachusetts Institute of Technology, USA, Benjamin ShermanMassachusetts Institute of Technology, USA, Adam ChlipalaMassachusetts Institute of Technology, USA, Arvind Massachusetts Institute of Technology, USA

SpaceSearch: A Library for Building and Verifying Solver-Aided Tools

15:23 - 15:46
Talk

Konstantin WeitzUniversity of Washington, USA, Steven LyubomirskyUniversity of Washington, USA, Stefan HeuleStanford University, USA, Emina TorlakUniversity of Washington, USA, Michael D. ErnstUniversity of Washington, USA, Zachary TatlockUniversity of Washington, USA

15:46 - 16:10
Talk

Local Refinement Typing

Benjamin CosmanUniversity of California at San Diego, USA, Ranjit JhalaUniversity of California at San Diego, USA

16:10 - 16:40: Catering - Tuesday coffee break 3 at Catering

16:10 - 16:40
Coffee break

Tuesday coffee break 3

16:40 - 17:50: Research Papers - Program Construction at L1
Chair(s): John HughesChalmers University of Technology

16:40 - 17:03
Talk

Compiling to Categories

Conal ElliottTarget, USA

17:03 - 17:26
Talk

Visitors Unchained

François PottierInria, France

Staged Generic Programming

17:26 - 17:50
Talk

Jeremy YallopUniversity of Cambridge, UK

DOI Pre-print

16:40 - 18:10: FSCD 2017 - Session 9 at L2

16:40 - 17:10
Talk

Generalized Refocusing: from Hybrid Strategies to Abstract Machines

Malgorzata BiernackaUniversity of Wroclaw, Witold Charatonik, Klara Zielińska

17:10 - 17:40
Talk

Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or

Simon Castellan, Pierre Clairambault, Glynn Winskel

17:40 - 18:10
Talk

Refutation of Sallé's Longstanding Conjecture

Benedetto Intrigila, Giulio Manzonetto, Andrew Polonsky

17:50 - 18:20: Keynotes and Reports - Tuesday Closing Events at L1

17:50 - 18:20
Talk

Programming Contest Report

Sam LindleyUniversity of Edinburgh, UK

Wed 6 Sep

09:00 - 09:37: Student Research Competition - SRC Presentations at L1
Chair(s): Ilya SergeyUniversity College London

09:00 - 09:37
Awards

Student Research Competition: Finalist Presentations

09:00 - 10:00: FSCD 2017 - Session 10 at L2

09:00 - 10:00
Talk

Quantitative semantics for probabilistic programming

Christine Tasson

09:37 - 10:00: Research Papers - Domain-Specific Languages at L1
Chair(s): Martin ErwigOregon State University

09:37 - 10:00
Talk

Herbarium Racketensis: A Stroll through the Woods (Functional Pearl)

Vincent St-AmourNorthwestern University, USA, Daniel FelteyNorthwestern University, USA, Spencer P. FlorenceNorthwestern University, USA, Shu-Hung YouNorthwestern University, USA, Robby FindlerNorthwestern University, USA

A Specification for Dependent Types in Haskell

10:00 - 10:30: Catering - Wednesday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Wednesday coffee break 1

10:30 - 12:00: Research Papers - Dependently Typed Programming at L1
Chair(s): Dan LicataWesleyan University

10:30 - 10:52
Talk

Stephanie WeirichUniversity of Pennsylvania, USA, Antoine VoizardUniversity of Pennsylvania, USA, Pedro Henrique Azevedo de AmorimEcole Polytechnique, n.n. / University of Campinas, Brazil, Richard A. EisenbergBryn Mawr College, USA

Parametric Quantifiers for Dependent Type Theory

10:52 - 11:15
Talk

Andreas NuytsKU Leuven, Belgium, Andrea VezzosiChalmers University of Technology, Sweden, Dominique DevrieseKU Leuven, Belgium

Normalization by Evaluation for Sized Dependent Types

11:15 - 11:37
Talk

Andreas AbelUniversity of Gothenburg, Sweden, Andrea VezzosiChalmers University of Technology, Sweden, Theo WinterhalterENS Paris-Saclay, France

A Metaprogramming Framework for Formal Verification

11:37 - 12:00
Talk

Gabriel EbnerVienna University of Technology, Austria, Sebastian UllrichKIT, Germany, Jared RoeschUniversity of Washington, USA, Jeremy AvigadCarnegie Mellon University, USA, Leonardo De MouraMicrosoft Research, n.n.

Benedikt Ahrens, Peter Lefanu Lumsdaine

10:30 - 12:00: FSCD 2017 - Session 11 at L2

10:30 - 11:00
Talk

Displayed categories

11:00 - 11:30
Talk

List Objects with Algebraic Structure

Marcelo FioreComputer Laboratory, University of Cambridge, Philip Saville

11:30 - 12:00
Talk

There is only one notion of differentiation

Robin Cockett, Jean-Simon Lemay

12:00 - 13:00: Catering - Wednesday lunch at Catering

12:00 - 13:00
Lunch

Wednesday lunch

13:00 - 14:30: Research Papers - Contracts and Sessions at L1
Chair(s): Matthew FlattUniversity of Utah

13:00 - 13:22
Talk

Chaperone Contracts for Higher-Order Sessions

Hernan MelgrattiUniversity of Buenos Aires, Argentina, Luca PadovaniUniversity of Turin, Italy

Whip: Higher-Order Contracts for Modern Services

13:22 - 13:45
Talk

Lucas WayeHarvard University, USA, Christos DimoulasHarvard University, USA, Stephen ChongHarvard University, USA

Manifest Sharing with Session Types

13:45 - 14:07
Talk

Stephanie BalzerCarnegie Mellon University, USA, Frank PfenningCarnegie Mellon University, USA

14:07 - 14:30
Talk

Gradual Session Types

Atsushi IgarashiKyoto University, Japan, Peter ThiemannUniversity of Freiburg, Germany, Vasco VasconcelosUniversity of Lisbon, Portugal, Philip WadlerUniversity of Edinburgh, UK

A Fibrational Framework for Substructural and Modal Logics

13:00 - 14:30: FSCD 2017 - Session 12 at L2

13:00 - 13:30
Talk

Dan LicataWesleyan University, Michael Shulman, Mitchell Riley

13:30 - 14:00
Talk

Dinaturality between syntax and semantics

Paolo Pistone

14:00 - 14:30
Talk

Models of Type Theory Based on Moore Paths

Andrew PittsUniversity of Cambridge, Ian Orton

14:30 - 15:00: Catering - Wednesday coffee break 2 at Catering

14:30 - 15:00
Coffee break

Wednesday coffee break 2

15:00 - 16:10: Research Papers - Integrating Static and Dynamic Typing at L1
Chair(s): Ronald GarciaUniversity of British Columbia

15:00 - 15:23
Talk

Theorems for Free for Free: Parametricity, With and Without Types

Amal AhmedNortheastern University, USA, Dustin JamnerNortheastern University, USA, Jeremy G. SiekIndiana University, USA, Philip WadlerUniversity of Edinburgh, UK

On Polymorphic Gradual Typing

15:23 - 15:46
Talk

Yuu IgarashiKyoto University, Japan, Taro SekiyamaIBM Research, Japan, Atsushi IgarashiKyoto University, Japan

Gradual Typing with Union and Intersection Types

15:46 - 16:10
Talk

Giuseppe CastagnaCNRS, France / University of Paris Diderot, France, Victor LanvinENS Cachan, France

Böhm Reduction in Infinitary Term Graph Rewriting Systems

15:00 - 16:00: FSCD 2017 - Session 13 at L2

15:00 - 15:30
Talk

Patrick BahrIT University of Copenhagen

15:30 - 16:00
Talk

Infinite Runs in Abstract Completion

Nao HirokawaJAIST, Aart Middeldorp, Christian Sternagel, Sarah Winkler

16:10 - 16:40: Catering - Wednesday coffee break 3 at Catering

16:10 - 16:40
Coffee break

Wednesday coffee break 3

16:40 - 17:50: Research Papers - Inference and Analysis at L1
Chair(s): Mark JonesPortland State University

16:40 - 17:03
Talk

Constrained Type Families

J. Garrett MorrisUniversity of Kansas, USA, Richard A. EisenbergBryn Mawr College, USA

Automating Sized-Type Inference for Complexity Analysis

17:03 - 17:26
Talk

Martin AvanziniUniversity of Innsbruck, Austria, Ugo Dal LagoUniversity of Bologna, Italy / Inria, France

Inferring Scope through Syntactic Sugar

17:26 - 17:50
Talk

Justin PombrioBrown University, USA, Shriram KrishnamurthiBrown University, USA, Mitchell WandNortheastern University, USA

Negative Translations and Normal Modality

16:40 - 17:10: FSCD 2017 - Session 14 at L2

16:40 - 17:10
Talk

Tadeusz Litak, Miriam Polzer, Ulrich Rabenstein

17:10 - 17:20: FSCD 2017 - Termination and Complexity Competition 2017 at L2

17:10 - 17:20
Other

Termination and Complexity Competition 2017

Jürgen Giesl, Albert Rubio, Johannes Waldmann, Akihisa Yamada

17:20 - 18:10: FSCD 2017 - FSCD General Meeting at L2

17:20 - 18:10
Meeting

FSCD General Meeting

17:50 - 18:00: Student Research Competition - SRC Awards at L1
Chair(s): Ilya SergeyUniversity College London

17:50 - 18:00
Awards

Student Research Competition Awards

Ilya SergeyUniversity College London

18:00 - 18:20: Keynotes and Reports - Wednesday Closing Events at L1

18:00 - 18:10
Talk

Program Chair's Report

Mark JonesPortland State University

18:10 - 18:20
Talk

ICFP 2018 Announcement

Robby FindlerNorthwestern University, USA

18:30 - 22:30: Social Events - Banquet at Weston Library

18:30 - 22:30
Social Event

Banquet

Thu 7 Sep

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C1 at L6
Chair(s): Runhang LiTwitter, Inc

09:00 - 10:00
Other

Tutorial C1: Online Applications with Incremental

Yaron Minsky, Sebastian FunkJane Street

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C2 at L5
Chair(s): Runhang LiTwitter, Inc

09:00 - 10:00
Other

Tutorial C2: Extensible Effects: understanding them, implementing them, using them

Ornaments: exploiting parametricity for safer, more automated code refactorization and code reuse (Invited Talk)

09:00 - 10:00: Haskell 2017 - Day 1, Session 1 at L1

09:00 - 10:00
Talk

Didier RémyINRIA

09:00 - 10:00: FSCD 2017 - Session 15 at L2

09:00 - 10:00
Talk

Type systems for the relational verification of higher order programs

Marco GaboardiUniversity at Buffalo, SUNY, USA

09:00 - 09:05: ML 2017 - Welcome at L3
Chair(s): Sam LindleyUniversity of Edinburgh, UK

09:00 - 09:05
Day opening

State machines all the way down

09:00 - 09:10: FHPC 2017 - Welcome to FHPC'17 at L4

09:00 - 09:10
Day opening

Welcome to FHPC'17

Phil TrinderUniversity of Glasgow, Cosmin OanceaDIKU, University of Copenhagen

09:05 - 10:00: ML 2017 - Invited talk at L3
Chair(s): Sam LindleyUniversity of Edinburgh, UK

09:05 - 10:00
Talk

Edwin BradyUniversity of St. Andrews, UK

09:10 - 10:10: FHPC 2017 - First Keynote at L4
Chair(s): Kevin HammondUniversity of St. Andrews, UK

09:10 - 10:10
Talk

Haskell in the Datacentre

Simon MarlowFacebook

10:00 - 10:30: Catering - Thursday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Thursday coffee break 1

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C1 at L6

10:30 - 11:30
Talk

Tutorial C1: Online Applications with Incremental (part 2)

Yaron Minsky, Sebastian FunkJane Street

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C2 at L5

10:30 - 11:30
Talk

Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 2)

From High-level Radio Protocol Specifications to Efficient Low-level Implementations via Partial Evaluation

10:30 - 11:30: FHPC 2017 - Compilation at L4
Chair(s): Phil TrinderUniversity of Glasgow

10:30 - 11:00
Talk

Geoffrey MainlandDrexel University, USA, Siddhanathan ShanmugamDrexel University, USA

11:00 - 11:30
Talk

Destination-Passing Style for Efficient Memory Management

Amir ShaikhhaEPFL, Switzerland, Andrew FitzgibbonMicrosoft Research, Cambridge, Simon Peyton JonesMicrosoft Research, Cambridge, Dimitrios VytiniotisMicrosoft Research, Cambridge

10:30 - 11:30: Haskell 2017 - Day 1, Session 2 at L1

10:30 - 11:00
Talk

Algebraic Graphs with Class (Functional Pearl)

Andrey Mokhov

11:00 - 11:30
Talk

Packrats Parse in Packs

Mario Blažević, Jacques Légaré

10:30 - 11:59: FSCD 2017 - Session 16 at L2

10:30 - 11:00
Talk

Arrays and References in Resource Aware ML

Benjamin Lichtman, Jan HoffmannCarnegie Mellon University

11:00 - 11:30
Talk

The Complexity of Principal Inhabitation

Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund

11:30 - 11:59
Talk

Types as Resources for Classical Natural Deduction

Delia KesnerIRIF, France / University of Paris Diderot, France, Pierre Vial

10:30 - 11:45: ML 2017 - Types and modules at L3

10:30 - 10:55
Talk

Mergeable types

Gowtham KakiPurdue University, KC SivaramakrishnanUniversity of Cambridge, Samodya AbeysiriwardanePurdue University, Suresh JagannathanPurdue University

10:55 - 11:20
Talk

Tierless modules

Gabriel RadanneUniversité Denis Diderot Paris 7, PPS, Jérôme VouillonUniv Paris Diderot, Sorbonne Paris Cité, BeSport

11:20 - 11:45
Talk

First-class subtypes

Jeremy YallopUniversity of Cambridge, UK, Stephen Dolan

11:20 - 12:00: Catering - Thursday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Thursday coffee break 2

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C1 at L6

12:00 - 12:30
Talk

Tutorial C1: Online Applications with Incremental (part 3)

Yaron Minsky, Sebastian FunkJane Street

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C2 at L5

12:00 - 12:30
Talk

Tutorial C2: Extensible Effects: understanding them, implementing them, using them (part 3)

Ode on a Random Urn (Functional Pearl)

12:00 - 12:30: Haskell 2017 - Day 1, Session 3 at L1

12:00 - 12:30
Talk

Leonidas LampropoulosUniversity of Pennsylvania, Antal Spector-Zabusky, Kenneth Foner

12:00 - 12:30: FHPC 2017 - Tools at L4
Chair(s): Cosmin OanceaDIKU, University of Copenhagen

12:00 - 12:30
Talk

VisPar: Visualising dataflow graphs from the Par monad

Maximilian AlgehedChalmers University of Technology, Sweden, Patrik JanssonChalmers University of Technology

12:00 - 12:25: ML 2017 - Verification at L3

12:00 - 12:25
Talk

VOCAL -- a verified OCAml Library

Arthur CharguéraudInria, Jean-Christophe FilliatreCNRS, Paris, France, Mário PereiraLRI - Université Paris-Sud, François PottierInria, France

12:25 - 14:00: Catering - Thursday lunch at Catering

12:25 - 14:00
Lunch

Thursday lunch

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C3 at L5
Chair(s): Runhang LiTwitter, Inc

14:00 - 15:00
Other

Tutorial C3: Concurrent Programming with Effect Handlers

Daniel HillerströmThe University of Edinburgh, KC SivaramakrishnanUniversity of Cambridge

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C4 at L6
Chair(s): Runhang LiTwitter, Inc

14:00 - 15:00
Talk

Tutorial C4: Git under the hood with OCaml

Romain Calascibetta

14:00 - 15:00: Haskell 2017 - Day 1, Session 4 at L1

14:00 - 14:30
Demonstration

QuickSpec: A Lightweight Theory Exploration Tool for Programmers (System Demonstration)

Maximilian AlgehedChalmers University of Technology, Sweden, Koen ClaessenChalmers University of Technology, Moa JohanssonChalmers University of Technology, Nicholas Smallbone

14:30 - 15:00
Talk

Speculate: Discovering Conditional Equations and Inequalities about Black-Box Functions by Reasoning from Test Results

Rudy Braquehais, Colin Runciman

14:00 - 15:00: FHPC 2017 - Parallel Programming at L4
Chair(s): Geoffrey MainlandDrexel University, USA

14:00 - 14:30
Talk

In Search of a Map: using Program Slicing to Discover Potential Parallelism in Recursive Functions

Adam Barwell, Kevin HammondUniversity of St. Andrews, UK

14:30 - 15:00
Talk

Strategies for Regular Segmented Reductions on GPU

Rasmus Wriedt LarsenDIKU, University of Copenhagen, Troels HenriksenDIKU, University of Copenhagen

14:00 - 15:15: ML 2017 - Programming language design at L3

14:00 - 14:25
Talk

Typer: an infix statically typed Lisp

Pierre DelaunayUniversité de Montréal, Vincent Archambault-BouffardUniversité de Montréal, Stefan MonnierUniversité de Montréal

14:25 - 14:50
Talk

Relational conversion for OCaml

Petr LozovSain Petersburg State University, SPbGU, Dmitri Boulytchev

14:50 - 15:15
Talk

Towards abductive functional programming

Koko MuroyaUniversity of Birmingham, UK

14:50 - 15:30: Catering - Thursday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Thursday coffee break 3

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C3 at L5

15:30 - 16:20
Talk

Tutorial C3: Concurrent Programming with Effect Handlers (part 2)

Daniel Hillerström, KC SivaramakrishnanUniversity of Cambridge

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C4 at L6

15:30 - 16:20
Talk

Tutorial C4: Git under the hood with OCaml (part 2)

Romain Calascibetta

15:30 - 16:30: Haskell 2017 - Day 1, Session 5 at L1

15:30 - 16:00
Talk

Using Coq to Write Fast and Correct Haskell

John Wiegley, Benjamin DelawarePurdue University

16:00 - 16:30
Talk

A Tale of Two Provers: Verifying Monoidal String Matching in Liquid Haskell and Coq

Niki VazouUniversity of Maryland, Leonidas LampropoulosUniversity of Pennsylvania, Jeff Polakow

15:30 - 16:30: FHPC 2017 - Demo Session at L4
Chair(s): Cosmin OanceaDIKU, University of Copenhagen

15:30 - 15:59
Demonstration

Futhark Demo

Troels HenriksenDIKU, University of Copenhagen

16:00 - 16:29
Demonstration

ParaFormance Demo: Democratizing Parallel Software Development

Christopher BrownUniversity of St. Andrews, UK, Kevin HammondUniversity of St. Andrews, UK

16:30 - 16:50
Social Event

Break 16:30 - 16:50: Wine and Nibbles @ North Mezzanine

15:30 - 16:20: ML 2017 - Performance at L3

15:30 - 15:55
Talk

Making SML# a general-purpose high-performance language

Atsushi OhoriTohoku University, Japan, Kenjiro TauraThe University of Tokyo, Katsuhiro UenoTohoku University

15:55 - 16:20
Talk

Efficient representation of large, dynamic sequences in ML

Arthur CharguéraudInria, Mike Rainey

16:20 - 16:50: Catering - Thursday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Thursday coffee break 4

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C3 at L5

16:50 - 17:30
Talk

Tutorial C3: Concurrent Programming with Effect Handlers (part 3)

Daniel HillerströmThe University of Edinburgh, KC SivaramakrishnanUniversity of Cambridge

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C4 at L6

16:50 - 17:30
Talk

Tutorial C4: Git under the hood with OCaml (part 3)

Romain Calascibetta

16:50 - 17:50: Haskell 2017 - Day 1, Session 6 at L1

16:50 - 17:20
Talk

A Meta-EDSL for Distributed Web Applications

Anton EkbladChalmers University of Technology

17:20 - 17:50
Talk

Composable Network Stacks and Remote Monads

Justin Dawson, Mark Grebe, Andy Gill

16:50 - 17:50: FHPC 2017 - Demo and Panel at L4
Chair(s): Phil TrinderUniversity of Glasgow

16:50 - 17:20
Demonstration

Ziria Demo: Wringing performance from high-level code

Siddhanathan ShanmugamDrexel University, USA, Geoffrey MainlandDrexel University, USA

17:20 - 17:50
Day closing

Panel Discussion: The challenges for Functional High Performance Computing

Geoffrey MainlandDrexel University, USA, Kevin HammondUniversity of St. Andrews, UK, Simon MarlowFacebook

16:50 - 17:40: ML 2017 - Effects at L3

16:50 - 17:15
Talk

Effects without monads: non-determinism

Effectively tackling the awkward squad

17:15 - 17:40
Talk

Stephen Dolan, Spiros EliopoulosJane Street Group, Daniel HillerströmThe University of Edinburgh, Anil MadhavapeddyOCaml Labs, KC SivaramakrishnanUniversity of Cambridge, Leo WhiteJane Street

18:15 - 20:30: Social Events - Industry Reception at Ashmolean Museum

18:15 - 20:30
Social Event

Industry Reception

Fri 8 Sep

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C5 at L6
Chair(s): Runhang LiTwitter, Inc

09:00 - 10:00
Talk

Tutorial C5: Teaching Functional Programming

Michael SperberActive Group GmbH

09:00 - 10:00: CUFP 2017 - CUFP Tutorials C6 at L5
Chair(s): Runhang LiTwitter, Inc

09:00 - 10:00
Talk

Tutorial C6: Transducers in Practice

Renzo BorgattiuSwitch

09:00 - 10:00: Haskell 2017 - Day 2, Session 1 at L1

09:00 - 10:00
Talk

Algorithmic Music in Haskell (Invited Talk)

Donya QuickStevens Institute of Technology

09:00 - 09:10: OCaml 2017 - Opening at L3

09:00 - 09:05
Day opening

Opening

Gabriel SchererNortheastern University

09:00 - 09:10: Erlang 2017 - Opening & Welcome at L4

09:00 - 09:10
Day opening

Opening & Welcome

09:10 - 10:00: Erlang 2017 - Keynote Invited Talk at L4

09:10 - 10:00
Talk

Keynote

Martin Sumner

09:10 - 10:10: OCaml 2017 - Talk session 1 at L3

09:05 - 09:40
Talk

Invited talk: new contributors

David AllsoppUniversity of Cambridge, Florian Angeletti, Sébastien HindererInria

09:40 - 10:05
Talk

The State of the OCaml Platform: September 2017

Anil MadhavapeddyOCaml Labs

10:00 - 10:30: Catering - Friday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Friday coffee break 1

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C5 at L6

10:30 - 11:30
Talk

Tutorial C5: Teaching Functional Programming (part 2)

Michael SperberActive Group GmbH

10:30 - 11:30: CUFP 2017 - CUFP Tutorials C6 at L5

10:30 - 11:30
Talk

Tutorial C6: Transducers in Practice (part 2)

Renzo BorgattiuSwitch

10:30 - 11:30: Haskell 2017 - Day 2, Session 2 at L1

10:30 - 11:00
Talk

Well-Typed Music Does Not Sound Wrong (Experience Report)

Dmitrij Szamozvancev, Michael GaleUniversity of Warwick, UK

11:00 - 11:30
Talk

Back to the Future: Time Travel in FRP

Ivan PerezUniversity of Nottingham, UK

10:30 - 11:20: Erlang 2017 - Session 2 at L4

10:30 - 10:55
Talk

Construction and Formal Verification of a Fault-Tolerant Distributed Mutual Exclusion Algorithm

Evgeniy ShishkinJSC "InfoTeCS"

DOI File Attached

10:55 - 11:20
Talk

Towards an Isabelle/HOL Formalisation of Core Erlang

Joseph HarrisonUniversity of Kent

10:30 - 11:30: OCaml 2017 - Talk session 2 at L3

10:30 - 10:50
Talk

Owl: A General-Purpose Numerical Library in OCaml

Liang WangUniversity of Cambridge

Link to publication Pre-print

10:50 - 11:10
Talk

Extending OCaml's open

Runhang LiTwitter, Inc, Jeremy YallopUniversity of Cambridge, UK

Link to publication Pre-print

11:10 - 11:30
Talk

Genspio: Generating Shell Phrases In OCaml

Sebastien MondetMount Sinai - Hammer Lab

Flash poster presentation

11:20 - 12:00: Catering - Friday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Friday coffee break 2

11:35 - 12:30: OCaml 2017 - Poster session at L3

11:35 - 11:45
Talk

11:45 - 12:30
Talk

mSAT: An OCaml SAT Solver

Bury GuillaumeINRIA / LSV / CNRS

Jbuilder: a modern approach to OCaml development

11:45 - 12:30
Talk

Jeremie DiminoJane Street Europe, Mark Shinwell

11:45 - 12:30
Talk

Tyre – Typed Regular Expressions

Gabriel RadanneUniversité Denis Diderot Paris 7, PPS

ocamli: Interpreted OCaml

11:45 - 12:30
Talk

John Whitington

Tutorial C5: Teaching Functional Programming (part 3)

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C5 at L6

12:00 - 12:30
Talk

Michael SperberActive Group GmbH

12:00 - 12:30: CUFP 2017 - CUFP Tutorials C6 at L5

12:00 - 12:30
Talk

Tutorial C6: Transducers in Practice (part 3)

Renzo BorgattiuSwitch

12:00 - 12:30: Haskell 2017 - Day 2, Session 3 at L1

12:00 - 12:30
Talk

The Linearity Monad

Jennifer PaykinUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania

12:00 - 12:25: Erlang 2017 - Session 3 at L4

12:00 - 12:25
Talk

Erlang and Elixir development news

12:25 - 14:00: Catering - Friday lunch at Catering

12:25 - 14:00
Lunch

Friday lunch

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C7 at L6
Chair(s): Runhang LiTwitter, Inc

14:00 - 15:00
Talk

Tutorial C7: Owl - Data Science in OCaml

Liang WangUniversity of Cambridge

14:00 - 15:00: CUFP 2017 - CUFP Tutorials C8 at L5
Chair(s): Runhang LiTwitter, Inc

14:00 - 15:00
Talk

Tutorial C8: GraphQL Servers in OCaml

Andreas GarnæsZendesk

14:00 - 15:00: Haskell 2017 - Day 2, Session 4 at L1

14:00 - 14:30
Talk

Elaboration on Functional Dependencies

Georgios KarachaliasKU Leuven, Belgium, Tom SchrijversKU Leuven

14:30 - 15:00
Talk

Quantified Class Constraints

Gert-Jan Bottu, Georgios KarachaliasKU Leuven, Belgium, Tom SchrijversKU Leuven, Bruno C. d. S. OliveiraUniversity of Hong Kong, China, Philip WadlerUniversity of Edinburgh, UK

14:00 - 14:50: Erlang 2017 - Session 4 at L4

14:00 - 14:25
Talk

Distributed Memory Architecture for High-Level Synthesis of Embedded Controllers from Erlang

Kagumi AzumaKwansei Gakuin University, Nagisa IshiuraKwansei Gakuin University, Nobuaki YoshidaASTEM RI/KYOTO, Hiroyuki KanbaraASTEM RI/KYOTO

14:25 - 14:50
Talk

Structuring Erlang BEAM control flow

Dániel LukácsEötvös Loránd University, Melinda Toth

14:00 - 15:00: OCaml 2017 - Talk session 3 at L3

14:00 - 14:20
Talk

ROTOR: First Steps Towards a Refactoring Tool for OCaml

Reuben N. S. RoweUniversity of Kent, Simon Thompson

A memory model for multicore OCaml

14:20 - 14:40
Talk

Stephen Dolan, KC SivaramakrishnanUniversity of Cambridge

Bioinformatics, The Typed Tagless Final Way

14:40 - 15:00
Talk

Sebastien MondetMount Sinai - Hammer Lab

Tutorial C7: Owl - Data Science in OCaml (part 2)

14:50 - 15:30: Catering - Friday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Friday coffee break 3

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C7 at L6

15:30 - 16:20
Talk

Liang WangUniversity of Cambridge

15:30 - 16:20: CUFP 2017 - CUFP Tutorials C8 at L5

15:30 - 16:20
Talk

Tutorial C8: GraphQL Servers in OCaml (part 2)

Andreas GarnæsZendesk

15:30 - 16:30: Haskell 2017 - Day 2, Session 5 at L1

15:30 - 16:00
Talk

Hardware Software Co-Design in Haskell

Markus Aronsson, Mary Sheeran

16:00 - 16:30
Talk

Streaming Irregular Arrays

Robert Clifton-Everest, Trevor L. McDonellUniversity of New South Wales, Australia, Manuel Chakravarty, Gabriele KellerData61,CSIRO (formerly NICTA) and UNSW

15:30 - 16:20: Erlang 2017 - Session 5 at L4

15:30 - 15:55
Talk

The Shared-Memory Interferences of Erlang/OTP Built-ins

Stavros AronisUppsala University, Konstantinos (Kostis) Sagonas

15:55 - 16:20
Talk

Towards Change-driven Testing

Viktória Fördős, István BozóEötvös Loránd University, Melinda Toth

15:30 - 16:30: OCaml 2017 - Talk session 4 at L3

15:30 - 15:50
Talk

A B-tree library for OCaml

Tom RidgeUniversity of Leicester, UK

Wodan: a pure OCaml, flash-aware filesystem library

15:50 - 16:10
Talk

Gabriel de PerthuisOCaml Labs

Tezos: the OCaml Crypto-Ledger

16:10 - 16:30
Talk

Benjamin CanouOCamlPro, n.n., Grégoire HenryOCamlPro, n.n., Pierre ChambartOCamlPRO, Fabrice Le FessantOCamlPro, Arthur BREITMANDynamic Ledger Solutions

16:20 - 16:50: Catering - Friday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Friday coffee break 4

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C7 at L6

16:50 - 17:30
Talk

Tutorial C7: Owl - Data Science in OCaml (part 3)

Liang WangUniversity of Cambridge

16:50 - 17:30: CUFP 2017 - CUFP Tutorials C8 at L5

16:50 - 17:30
Talk

Tutorial C8: GraphQL Servers in OCaml (part 3)

Andreas GarnæsZendesk

16:50 - 17:50: Haskell 2017 - Day 2, Session 6 at L1

16:50 - 17:20
Talk

Improving STM Performance with Transactional Structs

Ryan Yates, Michael ScottUniversity of Rochester

17:20 - 17:50
Talk

Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping

Chao-Hong ChenIndiana University, Vikraman Choudhury, Ryan R. NewtonIndiana University

16:50 - 17:50: Erlang 2017 - Session 6 at L4

16:50 - 17:20
Talk

eAOP - An Aspect Oriented Programming Framework for Erlang

Ian CassarUniversity of Malta, Adrian FrancalanzaUniversity of Malta, Luca AcetoReykjavik University, Anna IngolfsdottirReykjavik University

17:20 - 17:50
Talk

In medias res: WIP discussion

16:50 - 17:40: OCaml 2017 - Talk session 5 at L3

17:00 - 17:20
Talk

Component-based Program Synthesis in OCaml

Zhanpeng LiangUniversity of Southern California, Kanae Tsushima

Stephen Dolan, Mindy Preston

17:20 - 17:40
Talk

Testing with Crowbar

Sat 9 Sep

09:00 - 09:10: FARM 2017 - Introduction at L3

09:00 - 09:10
Day opening

GHC Infrastructure Update and Discussion

Michael SperberActive Group GmbH, Jean BressonUMR STMS: IRCAM-CNRS-UPMC

09:00 - 10:10: HIW 2017 - State of GHC at L1
Chair(s): Richard A. EisenbergBryn Mawr College, USA

09:00 - 09:30
Talk

Progress on GHC

Simon Peyton JonesMicrosoft Research, Cambridge

09:30 - 10:00
Talk

Ben GamariWell-Typed LLP

10:00 - 10:10
Talk

Getting Ready for Hadrian

Andrey Mokhov, Zhen ZhangUniversity of Washington, Ben GamariWell-Typed LLP, Neil Mitchell

09:10 - 10:00: CUFP 2017 - CUFP Talks 1 at L2

09:10 - 09:35
Talk

Keynote: Are We There Yet?

Bodil StokkeChurch of Emacs

09:35 - 10:00
Talk

Bonsai: a DSL for serverless firm real-time decisioning

Jeremie Lasalle-RatelleAppNexus

09:10 - 10:00: FARM 2017 - Session 1: Papers/Demos at L3
Chair(s): Jean BressonUMR STMS: IRCAM-CNRS-UPMC

09:10 - 09:40
Talk

A Categorial Grammar for Music and Its Use in Automatic Melody Generation

Halley Young

09:40 - 10:00
Demonstration

Demo — Representation of Musical Notation in Haskell

Edward Lilley

Interfacing OCaml and Rust: picking the right tool for the job

10:00 - 10:30: Catering - Saturday coffee break 1 at Catering

10:00 - 10:30
Coffee break

Saturday coffee break 1

10:30 - 11:20: CUFP 2017 - CUFP Talks 2 at L2

10:30 - 10:55
Talk

Joris GiovannangeliAhrefs Research

10:55 - 11:20
Talk

Distributed load testing with MZBench

Renat Idrisov

10:30 - 11:30: HIW 2017 - Compiling to LLVM at L1
Chair(s): Jan StolarekUniversity of Edinburgh, UK

10:30 - 10:55
Talk

Native Support for Explicit Stacks in LLVM

Kavon FarvardinUniversity of Chicago, Simon Peyton JonesMicrosoft Research, Cambridge

10:55 - 11:20
Talk

SimplexHC: Lowering High-Level Haskell to Imperative IR

Siddharth BhatIIT Hyderabad

11:20 - 11:30
Talk

Lightning Talk Slot #1

10:30 - 11:30: FARM 2017 - Session 2: Papers/Demos at L3
Chair(s): Ivan PerezUniversity of Nottingham, UK

10:30 - 10:50
Demonstration

Demo — African Polyphony and Polyrhythm

Chris FordThoughtWorks (UK) Ltd.

Demo — Vivid: Sound Synthesis with Haskell and SuperCollider

10:50 - 11:10
Demonstration

Tom Murphy

GALE: A Functional Graphic Adventure Library and Engine

11:10 - 11:40
Talk

Ivan PerezUniversity of Nottingham, UK

11:20 - 12:00: Catering - Saturday coffee break 2 at Catering

11:20 - 12:00
Coffee break

Saturday coffee break 2

12:00 - 12:25: CUFP 2017 - CUFP Talks 3 at L2

12:00 - 12:25
Talk

Gens N' Roses: Appetite for Reduction

Jacob StanleyAmbiata

12:00 - 12:25: HIW 2017 - Constraints at L1
Chair(s): Ben GamariWell-Typed LLP

12:00 - 12:25
Talk

On Unsatisfiability

J. Garrett MorrisUniversity of Kansas, USA

12:00 - 12:30: FARM 2017 - Session 3: Paper at L3
Chair(s): Michael SperberActive Group GmbH

12:00 - 12:30
Talk

Modelling the Way Mathematics Is Actually Done

Joe Corneli, Ursula Martin, Dave Murray-Rust, Alison Pease, Raymond Puzio, Gabriela Rino Nesin

12:25 - 14:00: Catering - Saturday lunch at Catering

12:25 - 14:00
Lunch

Saturday lunch

14:00 - 14:50: CUFP 2017 - CUFP Talks 4 at L2

14:00 - 14:25
Talk

Formally Verifying a Smart-Contract Language Implementation with Isabelle

Simon MeierDigital Asset

14:25 - 14:50
Talk

Haskell games and apps for iOS and Android

Ivan PerezUniversity of Nottingham, UK

14:00 - 15:00: FARM 2017 - Session 4: Tutorial at L3
Chair(s): Jean BressonUMR STMS: IRCAM-CNRS-UPMC

14:00 - 15:00
Talk

FAUST Tutorial for Functional Programmers

Yann Orlarey, Stéphane Letz, Dominique Fober, Romain Michon

14:00 - 15:00: HIW 2017 - Working in Core at L1
Chair(s): Adam GundryWell-Typed LLP

14:00 - 14:25
Talk

Why GHC Core and Linear Logic Should be Best Friends

Carter Schonwald, Joel Burget

14:25 - 14:50
Talk

Demand Analysis vs. Call Arity

Sebastian GrafKarlsruhe Institute of Technology

14:50 - 15:00
Talk

Lightning Talk Slot #2

14:50 - 15:30: Catering - Saturday coffee break 3 at Catering

14:50 - 15:30
Coffee break

Saturday coffee break 3

15:30 - 16:20: CUFP 2017 - CUFP Talks 5 at L2

15:30 - 15:55
Talk

Using Haskell to run a datacenter

Pavlo Kerestey

15:55 - 16:20
Talk

Functional Facades over Legacy Code

Nicholas CowleG-Research, Robin KayG-Research

15:30 - 16:20: FARM 2017 - Session 5: Demos at L3
Chair(s): David JaninBordeaux INP / CNRS LaBRI / Bordeaux University

15:30 - 15:50
Demonstration

Demo — The Arpeggigon: A Functional Reactive Musical Automaton

Henrik NilssonUniversity of Nottingham, UK

Demo — Ait: A Concatenative Language for Creative Programming

15:50 - 16:10
Demonstration

Stian Veum Møllersen

An Experiment in Fragment-Based Code Distribution

15:30 - 16:30: HIW 2017 - Tool Support at L1
Chair(s): Wren RomanoX

15:30 - 15:55
Talk

IDE Support in GHC

Alan Zimmerman

15:55 - 16:20
Talk

Tracking GHC Performance

Mathieu BoespflugTweag I/O, Manuel Chakravarty

16:20 - 16:30
Talk

Lightning Talk Slot #3

16:20 - 16:50: Catering - Saturday coffee break 4 at Catering

16:20 - 16:50
Coffee break

Saturday coffee break 4

16:50 - 17:50: HIW 2017 - All Broken Up at L1
Chair(s): Bartosz NitkaFacebook

16:50 - 17:15
Talk

Philipp SchusterUniversity of Tübingen

17:15 - 17:50
Talk

Lightning Talk Slot #4

16:50 - 17:40: CUFP 2017 - CUFP Talks 6 at L2

16:50 - 17:15
Talk

Building the largest payment sandbox on a tiny machine

Máté MarjaiTestingPays

17:15 - 17:40
Talk

Using Functional Programming to Accelerate Translational Research at Pfizer

Austin HuangPfizer

16:50 - 17:40: FARM 2017 - Session 6: Papers/Demos at L3
Chair(s): Henrik NilssonUniversity of Nottingham, UK

16:50 - 17:20
Talk

Unified Media Programming: An Algebraic Approach

Simon ArchipoffCNRS LaBRI, Inria Bordeaux,, David JaninBordeaux INP / CNRS LaBRI / Bordeaux University

17:20 - 17:40
Demonstration

Demo — Octopus: A High-Level Fast 3D Animation Language

Simon ArchipoffCNRS LaBRI, Inria Bordeaux,, David JaninBordeaux INP / CNRS LaBRI / Bordeaux University