The **Second International Conference on Formal Structures for Computation and Deduction** is co-located with ICFP 2017.

You can find all information at http://www.cs.ox.ac.uk/conferences/fscd2017/.

**Dates**

#### Mon 4 SepDisplayed time zone: **Belfast** change

Mon 4 Sep

Displayed time zone:

**Belfast**change10:30 - 10:45 | |||

10:30 15mOther | Welcome messageFSCD 2017 |

10:45 - 11:45 | |||

10:45 60mTalk | Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset LanguagesFSCD 2017 |

13:00 - 14:30 | |||

13:00 30mTalk | Polynomial running times for polynomial-time oracle machinesFSCD 2017 | ||

13:30 30mTalk | A Curry-Howard Approach to Church’s SynthesisFSCD 2017 | ||

14:00 30mTalk | Streett Automata Model Checking of Higher-Order Recursion SchemesFSCD 2017 A: Ryota Suzuki , A: Koichi Fujima , A: Naoki Kobayashi University of Tokyo, Japan, A: Takeshi Tsukada University of Tokyo, Japan |

15:00 - 16:00 | |||

15:00 30mTalk | Relating System F and λ2: A Case Study in Coq, Abella and BelugaFSCD 2017 | ||

15:30 30mTalk | Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOLFSCD 2017 Jasmin Blanchette Vrije Universiteit Amsterdam, A: Mathias Fleury MPI-INF, A: Dmitriy Traytel ETH Zurich |

16:40 - 18:10 | |||

16:40 30mTalk | A polynomial-time algorithm for the Lambek calculus with brackets of bounded orderFSCD 2017 | ||

17:10 30mTalk | A sequent calculus for semi-associativityFSCD 2017 | ||

17:40 30mTalk | Combinatorial Flows and their NormalisationFSCD 2017 |

#### Tue 5 SepDisplayed time zone: **Belfast** change

Tue 5 Sep

Displayed time zone:

**Belfast**change10:30 - 11:30 | |||

10:30 60mTalk | Uniform Resource Analysis by Rewriting: Strenghts and WeaknessesFSCD 2017 Georg Moser University of Innsbruck |

11:30 - 12:00 | |||

11:30 30mTalk | Continuation Passing Style for Effect HandlersFSCD 2017 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 | |||

13:00 30mTalk | Confluence of an extension of Combinatory Logic by Boolean constantsFSCD 2017 | ||

13:30 30mTalk | Improving Rewriting Induction Approach for Proving Ground ConfluenceFSCD 2017 | ||

14:00 30mTalk | The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal typeFSCD 2017 |

15:00 - 16:00 | |||

15:00 30mTalk | Is the optimal implementation inefficient? Elementarily notFSCD 2017 | ||

15:30 30mTalk | Optimality and the Linear Substitution CalculusFSCD 2017 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 | |||

16:40 30mTalk | Generalized Refocusing: from Hybrid Strategies to Abstract MachinesFSCD 2017 | ||

17:10 30mTalk | Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-orFSCD 2017 | ||

17:40 30mTalk | Refutation of Sallé's Longstanding ConjectureFSCD 2017 |

#### Wed 6 SepDisplayed time zone: **Belfast** change

Wed 6 Sep

Displayed time zone:

**Belfast**change09:00 - 10:00 | |||

09:00 60mTalk | Quantitative semantics for probabilistic programmingFSCD 2017 |

10:30 - 12:00 | |||

10:30 30mTalk | Displayed categoriesFSCD 2017 | ||

11:00 30mTalk | List Objects with Algebraic StructureFSCD 2017 | ||

11:30 30mTalk | There is only one notion of differentiationFSCD 2017 |

13:00 - 14:30 | |||

13:00 30mTalk | A Fibrational Framework for Substructural and Modal LogicsFSCD 2017 | ||

13:30 30mTalk | Dinaturality between syntax and semanticsFSCD 2017 | ||

14:00 30mTalk | Models of Type Theory Based on Moore PathsFSCD 2017 |

15:00 - 16:00 | |||

15:00 30mTalk | Böhm Reduction in Infinitary Term Graph Rewriting SystemsFSCD 2017 | ||

15:30 30mTalk | Infinite Runs in Abstract CompletionFSCD 2017 |

16:40 - 17:10 | |||

16:40 30mTalk | Negative Translations and Normal ModalityFSCD 2017 |

17:10 - 17:20 | |||

17:10 10mOther | Termination and Complexity Competition 2017FSCD 2017 |

17:20 - 18:10 | |||

17:20 50mMeeting | FSCD General MeetingFSCD 2017 |

#### Thu 7 SepDisplayed time zone: **Belfast** change

Thu 7 Sep

Displayed time zone:

**Belfast**change09:00 - 10:00 | |||

09:00 60mTalk | Type systems for the relational verification of higher order programsFSCD 2017 |

10:30 - 11:59 | |||

10:30 30mTalk | Arrays and References in Resource Aware MLFSCD 2017 | ||

11:00 30mTalk | The Complexity of Principal InhabitationFSCD 2017 | ||

11:30 29mTalk | Types as Resources for Classical Natural DeductionFSCD 2017 |