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

Room information: L2

VenueMathematical Institute
Room nameL2
Floor0
Capacity210
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:05
WelcomeTyDe at L2
09:00
5m
Day opening
Welcome
TyDe
Sam Lindley University of Edinburgh, UK, Brent Yorgey Hendrix College
09:05 - 10:00
Invited talkTyDe at L2
09:05
55m
Talk
Driving types into PHP
TyDe
Andrew Kennedy Facebook London
10:30 - 11:30
Full papers 1TyDe at L2
10:30
30m
Talk
Generic packet descriptions: verified parsing and pretty printing of low-level data
TyDe
Marcell van Geest Utrecht University, Wouter Swierstra University of Utrecht
11:00
30m
Talk
Structured asynchrony with algebraic effects
TyDe
Daan Leijen Microsoft Research
12:00 - 12:25
Extended abstracts 1TyDe at L2
12:00
25m
Talk
Cogent⇑: giving systems engineers a stepping stone
TyDe
Zilin Chen UNSW, Australia
14:00 - 15:00
Full papers 2TyDe at L2
14:00
30m
Talk
Type safe Redis queries -- a case study of type-level programming in Haskell
TyDe
Ting-Yan Lai Institute of Information Science, Academia Sinica, Tyng-Ruey Chuang Institute of Information Science, Academia Sinica, Shin-Cheng Mu Academia Sinica, Taiwan
14:30
30m
Talk
Type-directed diffing of structured data
TyDe
Victor Cacciari Miraldo University of Utrecht, Pierre-Evariste Dagand LIP6/CNRS , Wouter Swierstra University of Utrecht
15:30 - 16:20
Extended abstracts 2TyDe at L2
15:30
25m
Talk
Affine killing
TyDe
Kiko Fernandez-Reyes Uppsala University, Dave Clarke Uppsala Univ. Sweden and KU Leuvern
15:55
25m
Talk
On ringads and foldables
TyDe
James McKinna University of Edinburgh
16:50 - 17:40
Extended abstracts 3TyDe at L2
16:50
25m
Talk
Type oriented programming for task based parallelism
TyDe
Nick Brown EPCC, Ludovic Capelli EPCC, James Mark Bull EPCC
17:15
25m
Talk
Type-directed reasoning for probabilistic, non-compositional resources
TyDe
Edwin Brady University of St. Andrews, UK, Kevin Hammond University of St. Andrews, UK, Christopher Schwaab University of St Andrews

Mon 4 Sep

Displayed time zone: Belfast change

10:30 - 10:45
WelcomeFSCD at L2
10:30
15m
Other
Welcome message
FSCD
C: Sam Staton University of Oxford, P: Dale Miller INRIA Saclay and LIX
10:45 - 11:45
Session 1FSCD at L2
10:45
60m
Talk
Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages
FSCD
I: Alexandra Silva University College London
13:00 - 14:30
Session 2FSCD at L2
13:00
30m
Talk
Polynomial running times for polynomial-time oracle machines
FSCD
A: Akitoshi Kawamura , A: Florian Steinberg
13:30
30m
Talk
A Curry-Howard Approach to Church’s Synthesis
FSCD
A: Colin Riba , A: Pierre Pradic
14:00
30m
Talk
Streett Automata Model Checking of Higher-Order Recursion Schemes
FSCD
A: Ryota Suzuki , A: Koichi Fujima , A: Naoki Kobayashi University of Tokyo, Japan, A: Takeshi Tsukada University of Tokyo, Japan
15:00 - 16:00
Session 3FSCD at L2
15:00
30m
Talk
Relating System F and λ2: A Case Study in Coq, Abella and Beluga
FSCD
A: Jonas Kaiser , A: Brigitte Pientka McGill University, A: Gert Smolka Saarland University
15:30
30m
Talk
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
FSCD
Jasmin Blanchette Vrije Universiteit Amsterdam, A: Mathias Fleury MPI-INF, A: Dmitriy Traytel ETH Zurich
16:40 - 18:10
Session 4FSCD at L2
16:40
30m
Talk
A polynomial-time algorithm for the Lambek calculus with brackets of bounded order
FSCD
A: Max Kanovich , A: Stepan Kuznetsov , A: Glyn Morrill , A: Andre Scedrov
17:10
30m
Talk
A sequent calculus for semi-associativity
FSCD
A: Noam Zeilberger University of Birmingham, UK
17:40
30m
Talk
Combinatorial Flows and their Normalisation
FSCD
A: Lutz Strassburger

Tue 5 Sep

Displayed time zone: Belfast change

10:30 - 11:30
Session 5FSCD at L2
10:30
60m
Talk
Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses
FSCD
Georg Moser University of Innsbruck
11:30 - 12:00
Session 6FSCD at L2
11:30
30m
Talk
Continuation Passing Style for Effect Handlers
FSCD
A: Daniel Hillerström The University of Edinburgh, A: Sam Lindley University of Edinburgh, UK, A: Robert Atkey University of Strathclyde, A: KC Sivaramakrishnan University of Cambridge
13:00 - 14:30
Session 7FSCD at L2
13:00
30m
Talk
Confluence of an extension of Combinatory Logic by Boolean constants
FSCD
A: Lukasz Czajka University of Innsbruck
13:30
30m
Talk
Improving Rewriting Induction Approach for Proving Ground Confluence
FSCD
A: Takahito Aoto , A: Yoshihito Toyama , A: Yuta Kimura
14:00
30m
Talk
The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal type
FSCD
A: Yohji Akama
15:00 - 16:00
Session 8FSCD at L2
15:00
30m
Talk
Is the optimal implementation inefficient? Elementarily not
FSCD
A: Stefano Guerrini , A: Marco Solieri University of Bath
15:30
30m
Talk
Optimality and the Linear Substitution Calculus
FSCD
A: Pablo Barenbaum University of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, A: Eduardo Bonelli CONICET, Argentina / Universidad Nacional de Quilmes, Argentina
16:40 - 18:10
Session 9FSCD at L2
16:40
30m
Talk
Generalized Refocusing: from Hybrid Strategies to Abstract Machines
FSCD
A: Malgorzata Biernacka University of Wroclaw, A: Witold Charatonik , A: Klara Zielińska
17:10
30m
Talk
Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or
FSCD
A: Simon Castellan , A: Pierre Clairambault , A: Glynn Winskel
17:40
30m
Talk
Refutation of Sallé's Longstanding Conjecture
FSCD
A: Benedetto Intrigila , A: Giulio Manzonetto , A: Andrew Polonsky

Wed 6 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Session 10FSCD at L2
09:00
60m
Talk
Quantitative semantics for probabilistic programming
FSCD
A: Christine Tasson
10:30 - 12:00
Session 11FSCD at L2
10:30
30m
Talk
Displayed categories
FSCD
A: Benedikt Ahrens , A: Peter Lefanu Lumsdaine
11:00
30m
Talk
List Objects with Algebraic Structure
FSCD
A: Marcelo Fiore Computer Laboratory, University of Cambridge, A: Philip Saville
11:30
30m
Talk
There is only one notion of differentiation
FSCD
A: Robin Cockett , A: Jean-Simon Lemay
13:00 - 14:30
Session 12FSCD at L2
13:00
30m
Talk
A Fibrational Framework for Substructural and Modal Logics
FSCD
A: Daniel R. Licata Wesleyan University, A: Michael Shulman , A: Mitchell Riley
13:30
30m
Talk
Dinaturality between syntax and semantics
FSCD
A: Paolo Pistone
14:00
30m
Talk
Models of Type Theory Based on Moore Paths
FSCD
A: Andrew M. Pitts University of Cambridge, A: Ian Orton
15:00 - 16:00
Session 13FSCD at L2
15:00
30m
Talk
Böhm Reduction in Infinitary Term Graph Rewriting Systems
FSCD
A: Patrick Bahr IT University of Copenhagen
15:30
30m
Talk
Infinite Runs in Abstract Completion
FSCD
A: Nao Hirokawa JAIST, A: Aart Middeldorp , A: Christian Sternagel , A: Sarah Winkler
16:40 - 17:10
Session 14FSCD at L2
16:40
30m
Talk
Negative Translations and Normal Modality
FSCD
A: Tadeusz Litak , A: Miriam Polzer , A: Ulrich Rabenstein
17:10 - 17:20
Termination and Complexity Competition 2017FSCD at L2
17:10
10m
Other
Termination and Complexity Competition 2017
FSCD
P: Jürgen Giesl , P: Albert Rubio , P: Johannes Waldmann , P: Akihisa Yamada
17:20 - 18:10
FSCD General MeetingFSCD at L2
17:20
50m
Meeting
FSCD General Meeting
FSCD

Thu 7 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Session 15FSCD at L2
09:00
60m
Talk
Type systems for the relational verification of higher order programs
FSCD
A: Marco Gaboardi University at Buffalo, SUNY, USA
10:30 - 11:59
Session 16FSCD at L2
10:30
30m
Talk
Arrays and References in Resource Aware ML
FSCD
A: Benjamin Lichtman , A: Jan Hoffmann Carnegie Mellon University
11:00
30m
Talk
The Complexity of Principal Inhabitation
FSCD
A: Andrej Dudenhefner Technical University Dortmund, A: Jakob Rehof Technical University Dortmund
11:30
29m
Talk
Types as Resources for Classical Natural Deduction
FSCD
A: Delia Kesner Université de Paris, CNRS, IRIF, France, A: Pierre Vial

Sat 9 Sep

Displayed time zone: Belfast change

09:10 - 10:00
CUFP Talks 1CUFP at L2
09:10
25m
Talk
Keynote: Are We There Yet?
CUFP
Bodil Stokke Church of Emacs
09:35
25m
Talk
Bonsai: a DSL for serverless firm real-time decisioning
CUFP
Jeremie Lasalle-Ratelle AppNexus
10:30 - 11:20
CUFP Talks 2CUFP at L2
10:30
25m
Talk
Interfacing OCaml and Rust: picking the right tool for the job
CUFP
Joris Giovannangeli Ahrefs Research
10:55
25m
Talk
Distributed load testing with MZBench
CUFP
Renat Idrisov
12:00 - 12:25
CUFP Talks 3CUFP at L2
12:00
25m
Talk
Gens N' Roses: Appetite for Reduction
CUFP
Jacob Stanley Ambiata
14:00 - 14:50
CUFP Talks 4CUFP at L2
14:00
25m
Talk
Formally Verifying a Smart-Contract Language Implementation with Isabelle
CUFP
Simon Meier Digital Asset
14:25
25m
Talk
Haskell games and apps for iOS and Android
CUFP
Ivan Perez University of Nottingham, UK
15:30 - 16:20
CUFP Talks 5CUFP at L2
15:30
25m
Talk
Using Haskell to run a datacenter
CUFP
Pavlo Kerestey
15:55
25m
Talk
Functional Facades over Legacy Code
CUFP
Nicholas Cowle G-Research, Robin Kay G-Research
16:50 - 17:40
CUFP Talks 6CUFP at L2
16:50
25m
Talk
Building the largest payment sandbox on a tiny machine
CUFP
A: Máté Marjai TestingPays
17:15
25m
Talk
Using Functional Programming to Accelerate Translational Research at Pfizer
CUFP
Austin Huang Pfizer

Sun 3 Sep

Displayed time zone: Belfast change

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

TyDe

Welcome

TyDe

Invited talk

TyDe

Full papers 1

TyDe

Extended abstracts 1

TyDe

Full papers 2

TyDe

Extended abstracts 2

TyDe

Extended abstracts 3

Mon 4 Sep

Displayed time zone: Belfast change

Room10:003011:003012:003013:003014:003015:003016:003017:003018:0030
L2

FSCD

Welcome

FSCD

Session 1

FSCD

Session 2

FSCD

Session 3

FSCD

Session 4

Tue 5 Sep

Displayed time zone: Belfast change

Room10:003011:003012:003013:003014:003015:003016:003017:003018:0030
L2

FSCD

Session 5

FSCD

Session 6

FSCD

Session 7

FSCD

Session 8

FSCD

Session 9

Wed 6 Sep

Displayed time zone: Belfast change

Room9:003010:003011:003012:003013:003014:003015:003016:003017:003018:0030
L2

FSCD

Session 10

FSCD

Session 11

FSCD

Session 12

FSCD

Session 13

FSCD

Session 14

FSCD

Termination and Complexity Competition 2017

FSCD

FSCD General Meeting

Thu 7 Sep

Displayed time zone: Belfast change

Room9:003010:003011:0030
L2

FSCD

Session 15

FSCD

Session 16

Sat 9 Sep

Displayed time zone: Belfast change

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

CUFP

CUFP

CUFP Talks 1

CUFP

CUFP Talks 2

CUFP

CUFP Talks 3

CUFP

CUFP Talks 4

CUFP

CUFP Talks 5

CUFP

CUFP Talks 6

Sun 3 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
L2
TyDe
Welcome
09:00 - 09:05
TyDe
Driving types into PHP
09:05 - 10:00
TyDe
Generic packet descriptions: verified parsing and pretty printing of lo ...
10:30 - 11:00
TyDe
Structured asynchrony with algebraic effects
11:00 - 11:30
TyDe
Cogent⇑: giving systems engineers a stepping stone
12:00 - 12:25
TyDe
Type safe Redis queries -- a case study of type-level programming in Ha ...
14:00 - 14:30
TyDe
Type-directed diffing of structured data
14:30 - 15:00
TyDe
Affine killing
15:30 - 15:55
TyDe
On ringads and foldables
15:55 - 16:20
TyDe
Type oriented programming for task based parallelism
16:50 - 17:15
TyDe
Type-directed reasoning for probabilistic, non-compositional resources
17:15 - 17:40

Mon 4 Sep

Displayed time zone: Belfast change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
L2
FSCD
Welcome message
10:30 - 10:45
FSCD
Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages
10:45 - 11:45
FSCD
Polynomial running times for polynomial-time oracle machines
13:00 - 13:30
FSCD
A Curry-Howard Approach to Church’s Synthesis
13:30 - 14:00
FSCD
Streett Automata Model Checking of Higher-Order Recursion Schemes
14:00 - 14:30
FSCD
Relating System F and λ2: A Case Study in Coq, Abella and Beluga
15:00 - 15:30
FSCD
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabe ...
15:30 - 16:00
FSCD
A polynomial-time algorithm for the Lambek calculus with brackets of bo ...
16:40 - 17:10
FSCD
A sequent calculus for semi-associativity
17:10 - 17:40
FSCD
Combinatorial Flows and their Normalisation
17:40 - 18:10

Tue 5 Sep

Displayed time zone: Belfast change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
L2
FSCD
Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses
10:30 - 11:30
FSCD
Continuation Passing Style for Effect Handlers
11:30 - 12:00
FSCD
Confluence of an extension of Combinatory Logic by Boolean constants
13:00 - 13:30
FSCD
Improving Rewriting Induction Approach for Proving Ground Confluence
13:30 - 14:00
FSCD
The confluent terminating context-free substitutive rewriting system fo ...
14:00 - 14:30
FSCD
Is the optimal implementation inefficient? Elementarily not
15:00 - 15:30
FSCD
Optimality and the Linear Substitution Calculus
15:30 - 16:00
FSCD
Generalized Refocusing: from Hybrid Strategies to Abstract Machines
16:40 - 17:10
FSCD
Observably Deterministic Concurrent Strategies and Intensional Full Abs ...
17:10 - 17:40
FSCD
Refutation of Sallé's Longstanding Conjecture
17:40 - 18:10

Wed 6 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:00153045
L2
FSCD
Quantitative semantics for probabilistic programming
09:00 - 10:00
FSCD
Displayed categories
10:30 - 11:00
FSCD
List Objects with Algebraic Structure
11:00 - 11:30
FSCD
There is only one notion of differentiation
11:30 - 12:00
FSCD
A Fibrational Framework for Substructural and Modal Logics
13:00 - 13:30
FSCD
Dinaturality between syntax and semantics
13:30 - 14:00
FSCD
Models of Type Theory Based on Moore Paths
14:00 - 14:30
FSCD
Böhm Reduction in Infinitary Term Graph Rewriting Systems
15:00 - 15:30
FSCD
Infinite Runs in Abstract Completion
15:30 - 16:00
FSCD
Negative Translations and Normal Modality
16:40 - 17:10
FSCD
Termination and Complexity Competition 2017
17:10 - 17:20
FSCD
FSCD General Meeting
17:20 - 18:10

Thu 7 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:00153045
L2
FSCD
Type systems for the relational verification of higher order programs
09:00 - 10:00
FSCD
Arrays and References in Resource Aware ML
10:30 - 11:00
FSCD
The Complexity of Principal Inhabitation
11:00 - 11:30
FSCD
Types as Resources for Classical Natural Deduction
11:30 - 11:59

Sat 9 Sep

Displayed time zone: Belfast change

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
L2
CUFP
Keynote: Are We There Yet?
09:10 - 09:35
CUFP
Bonsai: a DSL for serverless firm real-time decisioning
09:35 - 10:00
CUFP
Interfacing OCaml and Rust: picking the right tool for the job
10:30 - 10:55
CUFP
Distributed load testing with MZBench
10:55 - 11:20
CUFP
Gens N' Roses: Appetite for Reduction
12:00 - 12:25
CUFP
Formally Verifying a Smart-Contract Language Implementation with Isabelle
14:00 - 14:25
CUFP
Haskell games and apps for iOS and Android
14:25 - 14:50
CUFP
Using Haskell to run a datacenter
15:30 - 15:55
CUFP
Functional Facades over Legacy Code
15:55 - 16:20
CUFP
Building the largest payment sandbox on a tiny machine
16:50 - 17:15
CUFP
Using Functional Programming to Accelerate Translational Research at Pfizer
17:15 - 17:40