Write a Blog >>
CUFP 2017
Sun 3 - Sat 9 September 2017
Oxford, United Kingdom
co-located with
ICFP 2017
Toggle navigation
Attending
Venue: Mathematical Institute
Program
Complete 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
Track/Call
Organization
CUFP 2017 Committees
Track Committees
Organizing Committee
Program Committee
Contributors
People Index
Search
Series
Series
CUFP 2017
CUFP 2016
Sign in
Sign up
ICFP 2017
(
series
) /
CUFP 2017 (
series
) /
Mathematical Institute
/
Room information: L3
Venue
Mathematical Institute
Room name
L3
Floor
0
Capacity
110
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
HOPE
at
L3
09:00
10m
Day opening
Welcome
HOPE
C:
François Pottier
Inria, France
,
C:
Aleksandar Nanevski
IMDEA Software Institute
09:10 - 10:00
Invited talk
HOPE
at
L3
09:10
60m
Talk
Invited Talk: Semantics of Effect Systems by Graded Monads
HOPE
Shin-ya Katsumata
National Institute of Informatics
10:30 - 11:30
Modular Semantics
HOPE
at
L3
10:30
30m
Talk
Higher-order Programming is an Effect
HOPE
Oleg Kiselyov
File Attached
11:00
30m
Talk
A monadic solution to the Cartwright-Felleisen-Wadler conjecture
HOPE
Ohad Kammar
University of Oxford, UK
,
Dylan McDermott
University of Cambridge
File Attached
12:00 - 12:30
Rust
HOPE
at
L3
12:00
30m
Talk
RustBelt: Securing the Foundations of the Rust Programming Language
HOPE
Ralf Jung
MPI-SWS, Germany
,
Jacques-Henri Jourdan
MPI-SWS, Germany
,
Robbert Krebbers
Delft University of Technology, Netherlands
,
Derek Dreyer
MPI-SWS
14:00 - 15:00
Effects and Dependent Types
HOPE
at
L3
14:00
30m
Talk
Handling fibred algebraic effects
HOPE
Danel Ahman
University of Edinburgh
14:30
30m
Talk
Only Control Effects and Dependent Types
HOPE
Youyou Cong
Ochanomizu University
,
William J. Bowman
Northeastern University
15:30 - 16:30
Effects
HOPE
at
L3
15:30
30m
Talk
Programming a Web Server with Algebraic Effects
HOPE
Daan Leijen
Microsoft Research
16:00
30m
Talk
Logical Relations for Algebraic Effects
HOPE
Dariusz Biernacki
University of Wrocław
,
Maciej Piróg
University of Wrocław
,
Piotr Polesiuk
,
Filip Sieczkowski
University of Wrocław
16:50 - 17:40
Monotonicity
HOPE
at
L3
16:50
30m
Talk
Recalling a Witness
HOPE
Danel Ahman
University of Edinburgh
,
Cătălin Hriţcu
Inria Paris
,
Kenji Maillard
Inria Paris, ENS Paris, and Microsoft Research
,
Aseem Rastogi
Microsoft Research
,
Nikhil Swamy
Microsoft Research, n.n.
,
Cédric Fournet
Microsoft Research, n.n.
Pre-print
Thu 7 Sep
Displayed time zone:
Belfast
change
09:00 - 09:05
Welcome
ML
at
L3
Chair(s):
Sam Lindley
University of Edinburgh, UK
09:00
5m
Day opening
Welcome
ML
09:05 - 10:00
Invited talk
ML
at
L3
Chair(s):
Sam Lindley
University of Edinburgh, UK
09:05
55m
Talk
State machines all the way down
ML
Edwin Brady
University of St. Andrews, UK
10:30 - 11:45
Types and modules
ML
at
L3
10:30
25m
Talk
Mergeable types
ML
Gowtham Kaki
Purdue University
,
KC Sivaramakrishnan
University of Cambridge
,
Samodya Abeysiriwardane
Purdue University
,
Suresh Jagannathan
Purdue University
10:55
25m
Talk
Tierless modules
ML
Gabriel Radanne
Université Denis Diderot Paris 7, PPS
,
Jérôme Vouillon
Univ Paris Diderot, Sorbonne Paris Cité, BeSport
11:20
25m
Talk
First-class subtypes
ML
Jeremy Yallop
University of Cambridge, UK
,
Stephen Dolan
12:00 - 12:25
Verification
ML
at
L3
12:00
25m
Talk
VOCAL -- a verified OCAml Library
ML
Arthur Charguéraud
Inria
,
Jean-Christophe Filliatre
CNRS, Paris, France
,
Mário Pereira
LRI - Université Paris-Sud
,
François Pottier
Inria, France
14:00 - 15:15
Programming language design
ML
at
L3
14:00
25m
Talk
Typer: an infix statically typed Lisp
ML
Pierre Delaunay
Université de Montréal
,
Vincent Archambault-Bouffard
Université de Montréal
,
Stefan Monnier
Université de Montréal
14:25
25m
Talk
Relational conversion for OCaml
ML
Petr Lozov
Sain Petersburg State University, SPbGU
,
Dmitri Boulytchev
14:50
25m
Talk
Towards abductive functional programming
ML
Koko Muroya
University of Birmingham, UK
15:30 - 16:20
Performance
ML
at
L3
15:30
25m
Talk
Making SML# a general-purpose high-performance language
ML
Atsushi Ohori
Tohoku University, Japan
,
Kenjiro Taura
The University of Tokyo
,
Katsuhiro Ueno
Tohoku University
15:55
25m
Talk
Efficient representation of large, dynamic sequences in ML
ML
Arthur Charguéraud
Inria
,
Mike Rainey
16:50 - 17:40
Effects
ML
at
L3
16:50
25m
Talk
Effects without monads: non-determinism
ML
Oleg Kiselyov
17:15
25m
Talk
Effectively tackling the awkward squad
ML
Stephen Dolan
,
Spiros Eliopoulos
Jane Street Group
,
Daniel Hillerström
The University of Edinburgh
,
Anil Madhavapeddy
OCaml Labs
,
KC Sivaramakrishnan
University of Cambridge
,
Leo White
Jane Street
Fri 8 Sep
Displayed time zone:
Belfast
change
09:00 - 09:10
Opening
OCaml
at
L3
09:00
5m
Day opening
Opening
OCaml
Gabriel Scherer
Northeastern University
09:10 - 10:10
Talk session 1
OCaml
at
L3
09:05
35m
Talk
Invited talk: new contributors
OCaml
David Allsopp
University of Cambridge
,
Florian Angeletti
,
Sébastien Hinderer
Inria
09:40
25m
Talk
The State of the OCaml Platform: September 2017
OCaml
Anil Madhavapeddy
OCaml Labs
10:30 - 11:30
Talk session 2
OCaml
at
L3
10:30
20m
Talk
Owl: A General-Purpose Numerical Library in OCaml
OCaml
Liang Wang
University of Cambridge
Link to publication
Pre-print
10:50
20m
Talk
Extending OCaml's open
OCaml
Runhang Li
Twitter, Inc
,
Jeremy Yallop
University of Cambridge, UK
Link to publication
Pre-print
11:10
20m
Talk
Genspio: Generating Shell Phrases In OCaml
OCaml
Sebastien Mondet
Mount Sinai - Hammer Lab
Pre-print
11:35 - 12:30
Poster session
OCaml
at
L3
11:35
10m
Talk
Flash poster presentation
OCaml
11:45
45m
Talk
mSAT: An OCaml SAT Solver
OCaml
Bury Guillaume
INRIA / LSV / CNRS
Link to publication
11:45
45m
Talk
Jbuilder: a modern approach to OCaml development
OCaml
Jeremie Dimino
Jane Street Europe
,
Mark Shinwell
11:45
45m
Talk
Tyre – Typed Regular Expressions
OCaml
Gabriel Radanne
Université Denis Diderot Paris 7, PPS
Link to publication
11:45
45m
Talk
ocamli: Interpreted OCaml
OCaml
John Whitington
Link to publication
14:00 - 15:00
Talk session 3
OCaml
at
L3
14:00
20m
Talk
ROTOR: First Steps Towards a Refactoring Tool for OCaml
OCaml
Reuben N. S. Rowe
University of Kent
,
Simon Thompson
Link to publication
14:20
20m
Talk
A memory model for multicore OCaml
OCaml
Stephen Dolan
,
KC Sivaramakrishnan
University of Cambridge
Link to publication
14:40
20m
Talk
Bioinformatics, The Typed Tagless Final Way
OCaml
Sebastien Mondet
Mount Sinai - Hammer Lab
Pre-print
15:30 - 16:30
Talk session 4
OCaml
at
L3
15:30
20m
Talk
A B-tree library for OCaml
OCaml
Tom Ridge
University of Leicester, UK
Link to publication
15:50
20m
Talk
Wodan: a pure OCaml, flash-aware filesystem library
OCaml
Gabriel de Perthuis
OCaml Labs
Link to publication
16:10
20m
Talk
Tezos: the OCaml Crypto-Ledger
OCaml
Benjamin Canou
OCamlPro, n.n.
,
Grégoire Henry
OCamlPro, n.n.
,
Pierre Chambart
OCamlPRO
,
Fabrice Le Fessant
OCamlPro
,
Arthur BREITMAN
Dynamic Ledger Solutions
16:50 - 17:40
Talk session 5
OCaml
at
L3
17:00
20m
Talk
Component-based Program Synthesis in OCaml
OCaml
Zhanpeng Liang
University of Southern California
,
Kanae Tsushima
Link to publication
17:20
20m
Talk
Testing with Crowbar
OCaml
Stephen Dolan
,
Mindy Preston
Sat 9 Sep
Displayed time zone:
Belfast
change
09:00 - 09:10
Introduction
FARM
at
L3
09:00
10m
Day opening
Welcome
FARM
C:
Michael Sperber
Active Group GmbH
,
P:
Jean Bresson
UMR STMS: IRCAM-CNRS-UPMC
09:10 - 10:00
Session 1: Papers/Demos
FARM
at
L3
Chair(s):
Jean Bresson
UMR STMS: IRCAM-CNRS-UPMC
09:10
30m
Talk
A Categorial Grammar for Music and Its Use in Automatic Melody Generation
FARM
Halley Young
09:40
20m
Demonstration
Demo — Representation of Musical Notation in Haskell
FARM
Edward Lilley
Pre-print
10:30 - 11:30
Session 2: Papers/Demos
FARM
at
L3
Chair(s):
Ivan Perez
University of Nottingham, UK
10:30
20m
Demonstration
Demo — African Polyphony and Polyrhythm
FARM
Chris Ford
ThoughtWorks (UK) Ltd.
Pre-print
10:50
20m
Demonstration
Demo — Vivid: Sound Synthesis with Haskell and SuperCollider
FARM
Tom Murphy
Pre-print
11:10
30m
Talk
GALE: A Functional Graphic Adventure Library and Engine
FARM
Ivan Perez
University of Nottingham, UK
12:00 - 12:30
Session 3: Paper
FARM
at
L3
Chair(s):
Michael Sperber
Active Group GmbH
12:00
30m
Talk
Modelling the Way Mathematics Is Actually Done
FARM
Joe Corneli
,
Ursula Martin
,
Dave Murray-Rust
,
Alison Pease
,
Raymond Puzio
,
Gabriela Rino Nesin
14:00 - 15:00
Session 4: Tutorial
FARM
at
L3
Chair(s):
Jean Bresson
UMR STMS: IRCAM-CNRS-UPMC
14:00
60m
Talk
FAUST Tutorial for Functional Programmers
FARM
Yann Orlarey
,
Stéphane Letz
,
Dominique Fober
,
Romain Michon
15:30 - 16:20
Session 5: Demos
FARM
at
L3
Chair(s):
David Janin
Bordeaux INP / CNRS LaBRI / Bordeaux University
15:30
20m
Demonstration
Demo — The Arpeggigon: A Functional Reactive Musical Automaton
FARM
Henrik Nilsson
University of Nottingham, UK
Pre-print
15:50
20m
Demonstration
Demo — Ait: A Concatenative Language for Creative Programming
FARM
Stian Veum Møllersen
Pre-print
16:50 - 17:40
Session 6: Papers/Demos
FARM
at
L3
Chair(s):
Henrik Nilsson
University of Nottingham, UK
16:50
30m
Talk
Unified Media Programming: An Algebraic Approach
FARM
Simon Archipoff
CNRS LaBRI, Inria Bordeaux,
,
David Janin
Bordeaux INP / CNRS LaBRI / Bordeaux University
17:20
20m
Demonstration
Demo — Octopus: A High-Level Fast 3D Animation Language
FARM
Simon Archipoff
CNRS LaBRI, Inria Bordeaux,
,
David Janin
Bordeaux INP / CNRS LaBRI / Bordeaux University
Pre-print
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
L3
HOPE
Welcome
HOPE
Invited talk
HOPE
Modular Semantics
HOPE
Rust
HOPE
Effects and Dependent Types
HOPE
Effects
HOPE
Monotonicity
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
L3
ML
Welcome
ML
Invited talk
ML
Types and modules
ML
Verification
ML
Programming language design
ML
Performance
ML
Effects
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
L3
OCaml
Opening
OCaml
Talk session 1
OCaml
Talk session 2
OCaml
Poster session
OCaml
Talk session 3
OCaml
Talk session 4
OCaml
Talk session 5
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
L3
FARM
Introduction
FARM
Session 1: Papers/Demos
FARM
Session 2: Papers/Demos
FARM
Session 3: Paper
FARM
Session 4: Tutorial
FARM
Session 5: Demos
FARM
Session 6: Papers/Demos
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
L3
HOPE
Welcome
09:00 - 09:10
HOPE
Invited Talk: Semantics of Effect Systems by Graded Monads
09:10 - 10:10
HOPE
Higher-order Programming is an Effect
10:30 - 11:00
HOPE
A monadic solution to the Cartwright-Felleisen-Wadler conjecture
11:00 - 11:30
HOPE
RustBelt: Securing the Foundations of the Rust Programming Language
12:00 - 12:30
HOPE
Handling fibred algebraic effects
14:00 - 14:30
HOPE
Only Control Effects and Dependent Types
14:30 - 15:00
HOPE
Programming a Web Server with Algebraic Effects
15:30 - 16:00
HOPE
Logical Relations for Algebraic Effects
16:00 - 16:30
HOPE
Recalling a Witness
16:50 - 17: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
L3
ML
Welcome
09:00 - 09:05
ML
State machines all the way down
09:05 - 10:00
ML
Mergeable types
10:30 - 10:55
ML
Tierless modules
10:55 - 11:20
ML
First-class subtypes
11:20 - 11:45
ML
VOCAL -- a verified OCAml Library
12:00 - 12:25
ML
Typer: an infix statically typed Lisp
14:00 - 14:25
ML
Relational conversion for OCaml
14:25 - 14:50
ML
Towards abductive functional programming
14:50 - 15:15
ML
Making SML# a general-purpose high-performance language
15:30 - 15:55
ML
Efficient representation of large, dynamic sequences in ML
15:55 - 16:20
ML
Effects without monads: non-determinism
16:50 - 17:15
ML
Effectively tackling the awkward squad
17:15 - 17:40
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
L3
OCaml
Opening
09:00 - 09:05
OCaml
Invited talk: new contributors
09:05 - 09:40
OCaml
The State of the OCaml Platform: September 2017
09:40 - 10:05
OCaml
Owl: A General-Purpose Numerical Library in OCaml
10:30 - 10:50
OCaml
Extending OCaml's open
10:50 - 11:10
OCaml
Genspio: Generating Shell Phrases In OCaml
11:10 - 11:30
OCaml
Flash poster presentation
11:35 - 11:45
OCaml
mSAT: An OCaml SAT Solver
11:45 - 12:30
Jbuilder: a modern approach to OCaml development
11:45 - 12:30
Tyre – Typed Regular Expressions
11:45 - 12:30
ocamli: Interpreted OCaml
11:45 - 12:30
OCaml
ROTOR: First Steps Towards a Refactoring Tool for OCaml
14:00 - 14:20
OCaml
A memory model for multicore OCaml
14:20 - 14:40
OCaml
Bioinformatics, The Typed Tagless Final Way
14:40 - 15:00
OCaml
A B-tree library for OCaml
15:30 - 15:50
OCaml
Wodan: a pure OCaml, flash-aware filesystem library
15:50 - 16:10
OCaml
Tezos: the OCaml Crypto-Ledger
16:10 - 16:30
OCaml
Component-based Program Synthesis in OCaml
17:00 - 17:20
OCaml
Testing with Crowbar
17:20 - 17:40
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
L3
FARM
Welcome
09:00 - 09:10
FARM
A Categorial Grammar for Music and Its Use in Automatic Melody Generation
09:10 - 09:40
FARM
Demo — Representation of Musical Notation in Haskell
09:40 - 10:00
FARM
Demo — African Polyphony and Polyrhythm
10:30 - 10:50
FARM
Demo — Vivid: Sound Synthesis with Haskell and SuperCollider
10:50 - 11:10
FARM
GALE: A Functional Graphic Adventure Library and Engine
11:10 - 11:40
FARM
Modelling the Way Mathematics Is Actually Done
12:00 - 12:30
FARM
FAUST Tutorial for Functional Programmers
14:00 - 15:00
FARM
Demo — The Arpeggigon: A Functional Reactive Musical Automaton
15:30 - 15:50
FARM
Demo — Ait: A Concatenative Language for Creative Programming
15:50 - 16:10
FARM
Unified Media Programming: An Algebraic Approach
16:50 - 17:20
FARM
Demo — Octopus: A High-Level Fast 3D Animation Language
17:20 - 17:40
x
Sat 9 Nov 00:14