FSCD 2017 accepted papers

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