| 2017 | 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, Oxford, UK, September 3-9, 2017 Dale Miller |
| 2017 | A Curry-Howard Approach to Church's Synthesis. Cécilia Pradic, Colin Riba |
| 2017 | A Fibrational Framework for Substructural and Modal Logics. Daniel R. Licata, Michael Shulman, Mitchell Riley |
| 2017 | A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order. Max I. Kanovich, Stepan L. Kuznetsov, Glyn Morrill, Andre Scedrov |
| 2017 | A Sequent Calculus for a Semi-Associative Law. Noam Zeilberger |
| 2017 | Arrays and References in Resource Aware ML. Benjamin Lichtman, Jan Hoffmann |
| 2017 | Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (Invited Talk). Alexandra Silva |
| 2017 | Böhm Reduction in Infinitary Term Graph Rewriting Systems. Patrick Bahr |
| 2017 | Combinatorial Flows and Their Normalisation. Lutz Straßburger |
| 2017 | Confluence of an Extension of Combinatory Logic by Boolean Constants. Lukasz Czajka |
| 2017 | Continuation Passing Style for Effect Handlers. Daniel Hillerström, Sam Lindley, Robert Atkey, K. C. Sivaramakrishnan |
| 2017 | Displayed Categories. Benedikt Ahrens, Peter LeFanu Lumsdaine |
| 2017 | Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers. |
| 2017 | Generalized Refocusing: From Hybrid Strategies to Abstract Machines. Malgorzata Biernacka, Witold Charatonik, Klara Zielinska |
| 2017 | Improving Rewriting Induction Approach for Proving Ground Confluence. Takahito Aoto, Yoshihito Toyama, Yuta Kimura |
| 2017 | Infinite Runs in Abstract Completion. Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler |
| 2017 | Is the Optimal Implementation Inefficient? Elementarily Not. Stefano Guerrini, Marco Solieri |
| 2017 | List Objects with Algebraic Structure. Marcelo Fiore, Philip Saville |
| 2017 | Models of Type Theory Based on Moore Paths. Ian Orton, Andrew M. Pitts |
| 2017 | Negative Translations and Normal Modality. Tadeusz Litak, Miriam Polzer, Ulrich Rabenstein |
| 2017 | Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel |
| 2017 | Observably Deterministic Concurrent Strategies and Intensional Full Abstraction for Parallel-or. Simon Castellan, Pierre Clairambault, Glynn Winskel |
| 2017 | On Dinaturality, Typability and beta-eta-Stable Models. Paolo Pistone |
| 2017 | Optimality and the Linear Substitution Calculus. Pablo Barenbaum, Eduardo Bonelli |
| 2017 | Polynomial Running Times for Polynomial-Time Oracle Machines. Akitoshi Kawamura, Florian Steinberg |
| 2017 | Quantitative Semantics for Probabilistic Programming (Invited Talk). Christine Tasson |
| 2017 | Refutation of Sallé's Longstanding Conjecture. Benedetto Intrigila, Giulio Manzonetto, Andrew Polonsky |
| 2017 | Relating System F and Lambda2: A Case Study in Coq, Abella and Beluga. Jonas Kaiser, Brigitte Pientka, Gert Smolka |
| 2017 | Streett Automata Model Checking of Higher-Order Recursion Schemes. Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada |
| 2017 | The Complexity of Principal Inhabitation. Andrej Dudenhefner, Jakob Rehof |
| 2017 | The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type. Yohji Akama |
| 2017 | There Is Only One Notion of Differentiation. J. Robin B. Cockett, Jean-Simon Lemay |
| 2017 | Type Systems for the Relational Verification of Higher Order Programs (Invited Talk). Marco Gaboardi |
| 2017 | Types as Resources for Classical Natural Deduction. Delia Kesner, Pierre Vial |
| 2017 | Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk). Georg Moser |