FSCD 2017
Mon 4 - Thu 7 September 2017 Oxford, United Kingdom
co-located with ICFP 2017

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
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Conference Day
Mon 4 Sep

Displayed time zone: Belfast change

10:30 - 10:45
WelcomeFSCD 2017 at L2
10:30
15m
Other
Welcome message
FSCD 2017
C: Sam StatonUniversity of Oxford, P: Dale MillerINRIA Saclay and LIX
10:45 - 11:45
Session 1FSCD 2017 at L2
10:45
60m
Talk
Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages
FSCD 2017
I: Alexandra SilvaUniversity College London
15:00 - 16:00
Session 3FSCD 2017 at L2
15:00
30m
Talk
Relating System F and λ2: A Case Study in Coq, Abella and Beluga
FSCD 2017
A: Jonas Kaiser, A: Brigitte PientkaMcGill University, A: Gert SmolkaSaarland University
15:30
30m
Talk
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
FSCD 2017
Jasmin BlanchetteVrije Universiteit Amsterdam, A: Mathias FleuryMPI-INF, A: Dmitriy TraytelETH Zurich

Conference Day
Tue 5 Sep

Displayed time zone: Belfast change

10:30 - 11:30
Session 5FSCD 2017 at L2
10:30
60m
Talk
Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses
FSCD 2017
Georg MoserUniversity of Innsbruck
11:30 - 12:00
Session 6FSCD 2017 at L2
11:30
30m
Talk
Continuation Passing Style for Effect Handlers
FSCD 2017
A: Daniel HillerströmThe University of Edinburgh, A: Sam LindleyUniversity of Edinburgh, UK, A: Robert AtkeyUniversity of Strathclyde, A: KC SivaramakrishnanUniversity of Cambridge
15:00 - 16:00
Session 8FSCD 2017 at L2
15:00
30m
Talk
Is the optimal implementation inefficient? Elementarily not
FSCD 2017
A: Stefano Guerrini, A: Marco SolieriUniversity of Bath
15:30
30m
Talk
Optimality and the Linear Substitution Calculus
FSCD 2017
A: Pablo BarenbaumUniversity of Buenos Aires, Argentina / IRIF, France / University of Paris Diderot, France, A: Eduardo BonelliCONICET, Argentina / Universidad Nacional de Quilmes, Argentina

Conference Day
Wed 6 Sep

Displayed time zone: Belfast change

10:30 - 12:00
Session 11FSCD 2017 at L2
10:30
30m
Talk
Displayed categories
FSCD 2017
11:00
30m
Talk
List Objects with Algebraic Structure
FSCD 2017
A: Marcelo FioreComputer Laboratory, University of Cambridge, A: Philip Saville
11:30
30m
Talk
There is only one notion of differentiation
FSCD 2017
13:00 - 14:30
Session 12FSCD 2017 at L2
13:00
30m
Talk
A Fibrational Framework for Substructural and Modal Logics
FSCD 2017
A: Dan LicataWesleyan University, A: Michael Shulman, A: Mitchell Riley
13:30
30m
Talk
Dinaturality between syntax and semantics
FSCD 2017
14:00
30m
Talk
Models of Type Theory Based on Moore Paths
FSCD 2017
A: Andrew PittsUniversity of Cambridge, A: Ian Orton
15:00 - 16:00
Session 13FSCD 2017 at L2
15:00
30m
Talk
Böhm Reduction in Infinitary Term Graph Rewriting Systems
FSCD 2017
A: Patrick BahrIT University of Copenhagen
15:30
30m
Talk
Infinite Runs in Abstract Completion
FSCD 2017
17:10 - 17:20
Termination and Complexity Competition 2017FSCD 2017 at L2
17:10
10m
Other
Termination and Complexity Competition 2017
FSCD 2017
17:20 - 18:10
FSCD General MeetingFSCD 2017 at L2
17:20
50m
Meeting
FSCD General Meeting
FSCD 2017

Conference Day
Thu 7 Sep

Displayed time zone: Belfast change

09:00 - 10:00
Session 15FSCD 2017 at L2
09:00
60m
Talk
Type systems for the relational verification of higher order programs
FSCD 2017
A: Marco GaboardiUniversity at Buffalo, SUNY, USA
10:30 - 11:59
Session 16FSCD 2017 at L2
10:30
30m
Talk
Arrays and References in Resource Aware ML
FSCD 2017
A: Benjamin Lichtman, A: Jan HoffmannCarnegie Mellon University
11:00
30m
Talk
The Complexity of Principal Inhabitation
FSCD 2017
A: Andrej DudenhefnerTechnical University Dortmund, A: Jakob RehofTechnical University Dortmund
11:30
29m
Talk
Types as Resources for Classical Natural Deduction
FSCD 2017
A: Delia KesnerIRIF, France / University of Paris Diderot, France, A: Pierre Vial

Accepted Papers

Title
A Curry-Howard Approach to Church’s Synthesis
FSCD 2017
A Fibrational Framework for Substructural and Modal Logics
FSCD 2017
A polynomial-time algorithm for the Lambek calculus with brackets of bounded order
FSCD 2017
A sequent calculus for semi-associativity
FSCD 2017
Arrays and References in Resource Aware ML
FSCD 2017
Böhm Reduction in Infinitary Term Graph Rewriting Systems
FSCD 2017
Combinatorial Flows and their Normalisation
FSCD 2017
Confluence of an extension of Combinatory Logic by Boolean constants
FSCD 2017
Continuation Passing Style for Effect Handlers
FSCD 2017
Dinaturality between syntax and semantics
FSCD 2017
Displayed categories
FSCD 2017
Generalized Refocusing: from Hybrid Strategies to Abstract Machines
FSCD 2017
Improving Rewriting Induction Approach for Proving Ground Confluence
FSCD 2017
Infinite Runs in Abstract Completion
FSCD 2017
Is the optimal implementation inefficient? Elementarily not
FSCD 2017
List Objects with Algebraic Structure
FSCD 2017
Models of Type Theory Based on Moore Paths
FSCD 2017
Negative Translations and Normal Modality
FSCD 2017
Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL
FSCD 2017
Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or
FSCD 2017
Optimality and the Linear Substitution Calculus
FSCD 2017
Polynomial running times for polynomial-time oracle machines
FSCD 2017
Refutation of Sallé's Longstanding Conjecture
FSCD 2017
Relating System F and λ2: A Case Study in Coq, Abella and Beluga
FSCD 2017
Streett Automata Model Checking of Higher-Order Recursion Schemes
FSCD 2017
The Complexity of Principal Inhabitation
FSCD 2017
The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal type
FSCD 2017
There is only one notion of differentiation
FSCD 2017
Types as Resources for Classical Natural Deduction
FSCD 2017