•  Ulrich Kohlenbach (TU Darmstadt)

CL&C is focused on the exploration of the computational content of mathematical and logical principles. The scientific aim of this workshop is to bring together researchers from both fields and exchange ideas. This workshop aims to support a fruitful exchange of ideas between the various lines of research on Classical Logic and Computation, covering all work aiming to explore computational aspects of classical logic and mathematics.

•  Yves Guiraud (INRIA / Université Paris 7)
•  Philippe Malbos (Université Claude Bernard Lyon 1)
•  Samuel Mimram (École Polytechnique)

Over recent years, rewriting methods have been generalized from strings and terms to richer algebraic structures such as operads, monoidal categories, and more generally higher-dimensional categories. These extensions of rewriting fit in the general scope of higher-dimensional rewriting theory, which has emerged as a unifying algebraic framework. This approach allows one to perform homotopical and homological analysis of rewriting systems (Squier theory). It also provides new computational methods in combinatorial algebra (Artin-Tits monoids, Coxeter and Garside structures), in homotopical and homological algebra (construction of cofibrant replacements, Koszulness properties).

•  Jakob Grue Simonsen (University Copenhagen)

The aim of the International Workshop on Higher-Order Rewriting (HOR) is to provide an informal and friendly setting to discuss recent work and work in progress concerning higher-order rewriting, broadly construed. This includes rewriting systems that have functional variables or bound variables In this way both, the lambda-calculus and combinatory logic being paradigmatic examples.

•  Peter LeFanu Lumsdaine (Stockholm University)
•  Nicolas Tabareau (Inria, Rennes)

Homotopy Type Theory/Univalent Foundations is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, informed by ideas and tools from abstract homotopy theory. One practical goal of the programme is to facilitate computer formalisation of mathematics in such logical systems.  We aim to focus on that aspect: bringing together researchers on formalisation in HoTT/UF to discuss the various established and experimental proof assistants for it, the different libraries available (HoTT Coq, Unimath, HoTT-Agda…), what logical features are convenient for the formalisation of “homotopical mathematics”, and how to make formalisation in HoTT/UF accessible and practical for mathematicians.

•  Georg Moser (University of Innsbruck)

IFIP Working Group 1.6 is one of working groups of the Technical Committee 1 of the International Federation for Information Processing (IFIP). WG 1.6 aims are: to promote research efforts in rewriting and its applications; to establish close cooperation between existing groups and to facilitate the emergence of new ones; to increase awareness of rewriting techniques in the computer science community at large; to foster development of applications of theoretical advances.

•  Naoki Kobayashi (University Tokyo)

Intersection types were introduced near the end of the 1970s to overcome the limitations of Curry’s type assignment system and to provide a char- acterization of the strongly normalizing terms of the Lambda Calculus. Although intersection types were initially intended for use in analyzing and/or synthesizing lambda models as well as in analyzing normalization properties, over the last twenty years the scope of the research on intersec- tion types and related systems has broadened in many directions, including programming language design, program analysis and verification. ITRS 2016 workshop aims to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches.

•  Gilles Dowek (INRIA)
•  Dan Licata (Wesleyan University)

Logical frameworks and meta-languages form a common substrate for representing, implementing, and rea- soning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems on the other hand have been the focus of considerable research over the last two decades. This workshop will bring together designers, implementors, and prac- titioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressivity and lucidity of the reasoning process.

•  Vivek Nigam (University Paraiba)
•  Mário Florido (University Porto)
•  Daniele Nantes Sobrinho (University of Brasília)

Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for formal specification of systems and programming languages, supporting tool development and reasoning. The objective of this workshop is to bring together theoreticians and practitioners to promote new techniques and results, and to facilitate feedback on the implementation and application of such techniques and results in practice. LSFA 2016 also aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research. The proceedings are produced after the meeting, so that authors can incorporate this feedback in the published papers.

•  Iliano Cervesato (Carnegie Mellon University)
•  Maribel Fernandez (King's College London)

The aim of this workshop is to bring together researchers who are currently developing theory and applications of linear calculi, to foster their interaction and provide a forum for presenting new ideas and work in progress, and enable newcomers to learn about current activities in this area. Linearity is a key feature in both theoretical and practical approaches to computer science, e.g., in proof technology, complexity analysis, and more recently quantum computation, expressive operational semantics, programming languages, and techniques for program transformation, update analysis and efficient implementation. The goal of this workshop is to present work exploring linearity both in theory and practice.

•  Silvio Ghilardi (University of Milan)
•  Manfred Schmidt-Schauß (Goethe University)

Unification is one of the central notions in automated reasoning and lies at the heart of many reasoning systems. Unification is concerned with the problem of making two terms equal, either syntactically or modulo a theory. UNIF 2016 will be the 30th in a series of annual international workshops on unification. Previous editions have taken place mostly in Europe (Austria, Denmark, France, Germany, Ireland, Italy, Poland, UK), but also in the USA and Japan. 

Traditionally, the scope of the UNIF workshops has covered the topic of unification in a broad sense, encompassing also research in constraint solving, admissibility of inference rules, and applications such as type checking, query answering and cryptographic protocol analysis.

•  Horatiu Cirstea (LORIA)
•  Santiago Escobar (University Politecnica de Valencia)
•  Naoki Nishida (Nagoya University)

The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally-based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. The programming languages of interest include pure, deterministic, impure, nondeterministic, concurrent, parallel languages, and may employ programming paradigms such as functional, logical, typed, imperative, object- oriented, and higher-order.