Blogs (28) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
ICFP 2017 (series) / Mathematical Institute /

Room information: L3

VenueMathematical Institute
Room nameL3
Floor0
Capacity110
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
WelcomeHOPE 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 talkHOPE 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 SemanticsHOPE 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
RustHOPE 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 TypesHOPE 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
EffectsHOPE 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
MonotonicityHOPE 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
WelcomeML at L3
Chair(s): Sam Lindley University of Edinburgh, UK
09:00
5m
Day opening
Welcome
ML

09:05 - 10:00
Invited talkML 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 modulesML 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
VerificationML 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 designML 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
PerformanceML 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
EffectsML 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
OpeningOCaml at L3
09:00
5m
Day opening
Opening
OCaml
Gabriel Scherer Northeastern University
09:10 - 10:10
Talk session 1OCaml 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 2OCaml 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 sessionOCaml 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 3OCaml 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 4OCaml 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 5OCaml 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
IntroductionFARM 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/DemosFARM 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/DemosFARM 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: PaperFARM 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: TutorialFARM 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: DemosFARM 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/DemosFARM 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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
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