FSCD 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/.

Time Zone

The program is currently displayed in (GMT+01:00) Greenwich Mean Time : Belfast.

Use conference time zone: (GMT+01:00) Greenwich Mean Time : BelfastSelect other time zone

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 programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone -

Mon 4 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast

	10:30 - 10:45: WelcomeFSCD 2017 at L2

	10:30 - 10:45 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 - 11:45 Talk		Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages FSCD 2017 I: Alexandra SilvaUniversity College London

	13:00 - 14:30: Session 2FSCD 2017 at L2

	13:00 - 13:30 Talk		Polynomial running times for polynomial-time oracle machines FSCD 2017 A: Akitoshi Kawamura, A: Florian Steinberg
	13:30 - 14:00 Talk		A Curry-Howard Approach to Church’s Synthesis FSCD 2017 A: Colin Riba, A: Pierre Pradic
	14:00 - 14:30 Talk		Streett Automata Model Checking of Higher-Order Recursion Schemes FSCD 2017 A: Ryota Suzuki, A: Koichi Fujima, A: Naoki KobayashiUniversity of Tokyo, Japan, A: Takeshi TsukadaUniversity of Tokyo, Japan

	15:00 - 16:00: Session 3FSCD 2017 at L2

	15:00 - 15:30 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 - 16:00 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

	16:40 - 18:10: Session 4FSCD 2017 at L2

	16:40 - 17:10 Talk		A polynomial-time algorithm for the Lambek calculus with brackets of bounded order FSCD 2017 A: Max Kanovich, A: Stepan Kuznetsov, A: Glyn Morrill, A: Andre Scedrov
	17:10 - 17:40 Talk		A sequent calculus for semi-associativity FSCD 2017 A: Noam ZeilbergerUniversity of Birmingham, UK
	17:40 - 18:10 Talk		Combinatorial Flows and their Normalisation FSCD 2017 A: Lutz Strassburger

Tue 5 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast

	10:30 - 11:30: Session 5FSCD 2017 at L2

	10:30 - 11:30 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 - 12:00 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

	13:00 - 14:30: Session 7FSCD 2017 at L2

	13:00 - 13:30 Talk		Confluence of an extension of Combinatory Logic by Boolean constants FSCD 2017 A: Lukasz CzajkaUniversity of Innsbruck
	13:30 - 14:00 Talk		Improving Rewriting Induction Approach for Proving Ground Confluence FSCD 2017 A: Takahito Aoto, A: Yoshihito Toyama, A: Yuta Kimura
	14:00 - 14:30 Talk		The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal type FSCD 2017 A: Yohji Akama

	15:00 - 16:00: Session 8FSCD 2017 at L2

	15:00 - 15:30 Talk		Is the optimal implementation inefficient? Elementarily not FSCD 2017 A: Stefano Guerrini, A: Marco SolieriUniversity of Bath
	15:30 - 16:00 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

	16:40 - 18:10: Session 9FSCD 2017 at L2

	16:40 - 17:10 Talk		Generalized Refocusing: from Hybrid Strategies to Abstract Machines FSCD 2017 A: Malgorzata BiernackaUniversity of Wroclaw, A: Witold Charatonik, A: Klara Zielińska
	17:10 - 17:40 Talk		Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or FSCD 2017 A: Simon Castellan, A: Pierre Clairambault, A: Glynn Winskel
	17:40 - 18:10 Talk		Refutation of Sallé's Longstanding Conjecture FSCD 2017 A: Benedetto Intrigila, A: Giulio Manzonetto, A: Andrew Polonsky

Wed 6 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast

	09:00 - 10:00: Session 10FSCD 2017 at L2

	09:00 - 10:00 Talk		Quantitative semantics for probabilistic programming FSCD 2017 A: Christine Tasson

	10:30 - 12:00: Session 11FSCD 2017 at L2

	10:30 - 11:00 Talk		Displayed categories FSCD 2017 A: Benedikt Ahrens, A: Peter Lefanu Lumsdaine
	11:00 - 11:30 Talk		List Objects with Algebraic Structure FSCD 2017 A: Marcelo FioreComputer Laboratory, University of Cambridge, A: Philip Saville
	11:30 - 12:00 Talk		There is only one notion of differentiation FSCD 2017 A: Robin Cockett, A: Jean-Simon Lemay

	13:00 - 14:30: Session 12FSCD 2017 at L2

	13:00 - 13:30 Talk		A Fibrational Framework for Substructural and Modal Logics FSCD 2017 A: Dan LicataWesleyan University, A: Michael Shulman, A: Mitchell Riley
	13:30 - 14:00 Talk		Dinaturality between syntax and semantics FSCD 2017 A: Paolo Pistone
	14:00 - 14:30 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 - 15:30 Talk		Böhm Reduction in Infinitary Term Graph Rewriting Systems FSCD 2017 A: Patrick BahrIT University of Copenhagen
	15:30 - 16:00 Talk		Infinite Runs in Abstract Completion FSCD 2017 A: Nao HirokawaJAIST, A: Aart Middeldorp, A: Christian Sternagel, A: Sarah Winkler

	16:40 - 17:10: Session 14FSCD 2017 at L2

	16:40 - 17:10 Talk		Negative Translations and Normal Modality FSCD 2017 A: Tadeusz Litak, A: Miriam Polzer, A: Ulrich Rabenstein

	17:10 - 17:20: Termination and Complexity Competition 2017FSCD 2017 at L2

	17:10 - 17:20 Other		Termination and Complexity Competition 2017 FSCD 2017 P: Jürgen Giesl, P: Albert Rubio, P: Johannes Waldmann, P: Akihisa Yamada

	17:20 - 18:10: FSCD General MeetingFSCD 2017 at L2

	17:20 - 18:10 Meeting		FSCD General Meeting FSCD 2017

Thu 7 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast

	09:00 - 10:00: Session 15FSCD 2017 at L2

	09:00 - 10:00 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 - 11:00 Talk		Arrays and References in Resource Aware ML FSCD 2017 A: Benjamin Lichtman, A: Jan HoffmannCarnegie Mellon University
	11:00 - 11:30 Talk		The Complexity of Principal Inhabitation FSCD 2017 A: Andrej DudenhefnerTechnical University Dortmund, A: Jakob RehofTechnical University Dortmund
	11:30 - 11:59 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: Colin Riba, A: Pierre Pradic
	A Fibrational Framework for Substructural and Modal Logics FSCD 2017 A: Dan Licata, A: Michael Shulman, A: Mitchell Riley
	A polynomial-time algorithm for the Lambek calculus with brackets of bounded order FSCD 2017 A: Max Kanovich, A: Stepan Kuznetsov, A: Glyn Morrill, A: Andre Scedrov
	A sequent calculus for semi-associativity FSCD 2017 A: Noam Zeilberger
	Arrays and References in Resource Aware ML FSCD 2017 A: Benjamin Lichtman, A: Jan Hoffmann
	Böhm Reduction in Infinitary Term Graph Rewriting Systems FSCD 2017 A: Patrick Bahr
	Combinatorial Flows and their Normalisation FSCD 2017 A: Lutz Strassburger
	Confluence of an extension of Combinatory Logic by Boolean constants FSCD 2017 A: Lukasz Czajka
	Continuation Passing Style for Effect Handlers FSCD 2017 A: Daniel Hillerström, A: Sam Lindley, A: Robert Atkey, A: KC Sivaramakrishnan
	Dinaturality between syntax and semantics FSCD 2017 A: Paolo Pistone
	Displayed categories FSCD 2017 A: Benedikt Ahrens, A: Peter Lefanu Lumsdaine
	Generalized Refocusing: from Hybrid Strategies to Abstract Machines FSCD 2017 A: Malgorzata Biernacka, A: Witold Charatonik, A: Klara Zielińska
	Improving Rewriting Induction Approach for Proving Ground Confluence FSCD 2017 A: Takahito Aoto, A: Yoshihito Toyama, A: Yuta Kimura
	Infinite Runs in Abstract Completion FSCD 2017 A: Nao Hirokawa, A: Aart Middeldorp, A: Christian Sternagel, A: Sarah Winkler
	Is the optimal implementation inefficient? Elementarily not FSCD 2017 A: Stefano Guerrini, A: Marco Solieri
	List Objects with Algebraic Structure FSCD 2017 A: Marcelo Fiore, A: Philip Saville
	Models of Type Theory Based on Moore Paths FSCD 2017 A: Andrew Pitts, A: Ian Orton
	Negative Translations and Normal Modality FSCD 2017 A: Tadeusz Litak, A: Miriam Polzer, A: Ulrich Rabenstein
	Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL FSCD 2017 Jasmin Blanchette, A: Mathias Fleury, A: Dmitriy Traytel
	Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or FSCD 2017 A: Simon Castellan, A: Pierre Clairambault, A: Glynn Winskel
	Optimality and the Linear Substitution Calculus FSCD 2017 A: Pablo Barenbaum, A: Eduardo Bonelli
	Polynomial running times for polynomial-time oracle machines FSCD 2017 A: Akitoshi Kawamura, A: Florian Steinberg
	Refutation of Sallé's Longstanding Conjecture FSCD 2017 A: Benedetto Intrigila, A: Giulio Manzonetto, A: Andrew Polonsky
	Relating System F and λ2: A Case Study in Coq, Abella and Beluga FSCD 2017 A: Jonas Kaiser, A: Brigitte Pientka, A: Gert Smolka
	Streett Automata Model Checking of Higher-Order Recursion Schemes FSCD 2017 A: Ryota Suzuki, A: Koichi Fujima, A: Naoki Kobayashi, A: Takeshi Tsukada
	The Complexity of Principal Inhabitation FSCD 2017 A: Andrej Dudenhefner, A: Jakob Rehof
	The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal type FSCD 2017 A: Yohji Akama
	There is only one notion of differentiation FSCD 2017 A: Robin Cockett, A: Jean-Simon Lemay
	Types as Resources for Classical Natural Deduction FSCD 2017 A: Delia Kesner, A: Pierre Vial

FSCD 2017

Program Display Configuration

Mon 4 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast

Tue 5 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast

Wed 6 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast

Thu 7 Sep Times are displayed in time zone: Greenwich Mean Time : Belfast

Accepted Papers

Welcome message FSCD 2017

Sam StatonConference Chair

University of Oxford

Dale MillerProgram Chair

INRIA Saclay and LIX

France

Brzozowski Goes Concurrent -- A Kleene Theorem for Pomset Languages FSCD 2017

Alexandra SilvaInvited Speaker

University College London

United Kingdom

Polynomial running times for polynomial-time oracle machines FSCD 2017

Akitoshi KawamuraAuthor

Florian SteinbergAuthor

A Curry-Howard Approach to Church’s Synthesis FSCD 2017

Colin RibaAuthor

Pierre PradicAuthor

Streett Automata Model Checking of Higher-Order Recursion Schemes FSCD 2017

Ryota SuzukiAuthor

Koichi FujimaAuthor

Naoki KobayashiAuthor

University of Tokyo, Japan

Takeshi TsukadaAuthor

University of Tokyo, Japan

Relating System F and λ2: A Case Study in Coq, Abella and Beluga FSCD 2017

Jonas KaiserAuthor

Brigitte PientkaAuthor

McGill University

Gert SmolkaAuthor

Saarland University

Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL FSCD 2017

Jasmin Blanchette

Vrije Universiteit Amsterdam

Netherlands

Mathias FleuryAuthor

MPI-INF

Germany

Dmitriy TraytelAuthor

ETH Zurich

Switzerland

A polynomial-time algorithm for the Lambek calculus with brackets of bounded order FSCD 2017

Max KanovichAuthor

Stepan KuznetsovAuthor

Glyn MorrillAuthor

Andre ScedrovAuthor

A sequent calculus for semi-associativity FSCD 2017

Noam ZeilbergerAuthor

University of Birmingham, UK

Combinatorial Flows and their Normalisation FSCD 2017

Lutz StrassburgerAuthor

Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses FSCD 2017

Georg Moser

University of Innsbruck

Continuation Passing Style for Effect Handlers FSCD 2017

Daniel HillerströmAuthor

The University of Edinburgh

United Kingdom

Sam LindleyAuthor

University of Edinburgh, UK

United Kingdom

Robert AtkeyAuthor

University of Strathclyde

KC SivaramakrishnanAuthor

University of Cambridge

United Kingdom

Confluence of an extension of Combinatory Logic by Boolean constants FSCD 2017

Lukasz CzajkaAuthor

University of Innsbruck

Improving Rewriting Induction Approach for Proving Ground Confluence FSCD 2017

Takahito AotoAuthor

Yoshihito ToyamaAuthor

Yuta KimuraAuthor

The confluent terminating context-free substitutive rewriting system for the λ-calculus with surjective pairing and terminal type FSCD 2017

Yohji AkamaAuthor

Mon 4 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast

Tue 5 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast

Wed 6 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast

Thu 7 Sep
Times are displayed in time zone: Greenwich Mean Time : Belfast