| 2016 | 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, Porto, Portugal, June 22-26, 2016 Delia Kesner, Brigitte Pientka |
| 2016 | Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems. Franziska Rapp, Aart Middeldorp |
| 2016 | Category Theory in Coq 8.5. Amin Timany, Bart Jacobs |
| 2016 | Certifying Confluence of Almost Orthogonal CTRSs via Exact Tree Automata Completion. Christian Sternagel, Thomas Sternagel |
| 2016 | Classical Extraction in Continuation Models. Valentin Blot |
| 2016 | Coalgebras and Higher-Order Computation: a GoI Approach. Ichiro Hasuo |
| 2016 | Complexity Hierarchies and Higher-Order Cons-Free Rewriting. Cynthia Kop, Jakob Grue Simonsen |
| 2016 | Complexity of Acyclic Term Graph Rewriting. Martin Avanzini, Georg Moser |
| 2016 | Compositional Compiler Verification for a Multi-Language World. Amal Ahmed |
| 2016 | Computing Connected Proof(-Structure)s From Their Taylor Expansion. Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora de Falco |
| 2016 | Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk |
| 2016 | Focusing in Orthologic. Olivier Laurent |
| 2016 | Formal Languages, Formally and Coinductively. Dmitriy Traytel |
| 2016 | Front Matter, Table of Contents, Preface, Steering Committee, Program Committee, External Reviewers, Organising Commitee. |
| 2016 | Functions-as-Constructors Higher-Order Unification. Tomer Libal, Dale Miller |
| 2016 | Globular: An Online Proof Assistant for Higher-Dimensional Rewriting. Krzysztof Bar, Aleks Kissinger, Jamie Vicary |
| 2016 | Ground Confluence Prover based on Rewriting Induction. Takahito Aoto, Yoshihito Toyama |
| 2016 | Homological Computations for Term Rewriting Systems. Philippe Malbos, Samuel Mimram |
| 2016 | Interaction Automata and the ia2d Interpreter. Stéphane Gimenez, David Obwaller |
| 2016 | Minimal Paradefinite Logics for Reasoning with Incompleteness and Inconsistency. Ofer Arieli, Arnon Avron |
| 2016 | Modular Focused Proof Systems for Intuitionistic Modal Logics. Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger |
| 2016 | New Results on Morris's Observational Theory: The Benefits of Separating the Inseparable. Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, Domenico Ruoppolo |
| 2016 | Nominal Narrowing. Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho |
| 2016 | Non-Omega-Overlapping TRSs are UN. Stefan Kahrs, Connor Smith |
| 2016 | Normalisation by Evaluation for Dependent Types. Thorsten Altenkirch, Ambrus Kaposi |
| 2016 | Normalisation by Random Descent. Vincent van Oostrom, Yoshihito Toyama |
| 2016 | On Undefined and Meaningless in Lambda Definability. Fer-Jan de Vries |
| 2016 | Proving Correctness of Logically Decorated Graph Rewriting Systems. Jon Haël Brenas, Rachid Echahed, Martin Strecker |
| 2016 | Reversible Term Rewriting. Naoki Nishida, Adrián Palacios, Germán Vidal |
| 2016 | Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule.. Ryota Akiyoshi, Kazushige Terui |
| 2016 | Strongly Normalising Cyclic Data Computation by Iteration Categories of Second-Order Algebraic Theories. Makoto Hamana |
| 2016 | Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus. Ryuta Arisaka |
| 2016 | Synthesis of Functional Programs with Help of First-Order Intuitionistic Logic. Marcin Benke, Aleksy Schubert, Daria Walukiewicz-Chrzaszcz |
| 2016 | Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. Gérard P. Huet |
| 2016 | The Independence of Markov's Principle in Type Theory. Thierry Coquand, Bassel Mannaa |
| 2016 | The Intersection Type Unification Problem. Andrej Dudenhefner, Moritz Martens, Jakob Rehof |
| 2016 | Verified Analysis of Functional Data Structures. Tobias Nipkow |
| 2016 | Weighted Relational Models for Mobility. James Laird |