Affiliated workshops

29 June 30 June 1-4 July 5 july 6 july
Linearity & TLLA FSCD HoTT/UF
See live program

29-30 June

Acronym Name / Description / Organisers Edition
Linearity & TLLA
Joint Workshop on Linearity and Trends in Linear Logic and Applications
This workshop aims at bringing together researchers who are currently developing theory and applications of linear calculi or use linear logic as a technical tool or a methodological guidline, 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, and the goal of this workshop is to present work exploring linearity both in theory and practice. The addressed topics include proof representation, operational, static and dynamical models of programming languages, linear languages and type systems, parallelism and concurrency, quantum and probabilist computation, as well as philosophy and linguistics.
Thomas Ehrhard - France CNRS and Université de Paris, France
Valeria de Paiva - Samsung Research America, CA, United States
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning 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 three decades. This workshop will bring together designers, implementors, and practitioners 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.
Claudio Sacerdoti Coen - University of Bologna, Italy
Alwen Tiu - The Australian National University, Australia
Workshop on Practical Aspects of Automated Reasoning
PAAR (Practical Aspects of Automated Reasoning) provides a forum for developers of automated reasoning tools to discuss and compare different implementation techniques, and for users to discuss and communicate their applications and requirements. This series of workshops brings together different groups to concentrate on practical aspects of the implementation and application of automated reasoning tools. Work in progress, new implementation techniques, and applications are particularly welcome.
Sophie Tourret - Max Planck Institute for Informatics, Germany
Pascal Fontaine - Université de Liège, Belgium
Philipp Rümmer - Uppsala University, Sweden

29 June

Acronym Name / Description / Organisers Edition
International Workshop on Unification
The 34th International Workshop on Unification is the next event in a series of international meetings devoted to unification theory and its applications. Unification is concerned with the problem of making two terms equal, finding solutions for equations, or making formulas equivalent. It is a fundamental process used in a number of fields of computer science, including automated reasoning, term rewriting, logic programming, natural language processing, program analysis, types, etc. Topics of interest of the workshop include syntactic and equational unification algorithms, matching and constraint solving, unification in modal, temporal, and description logics, higher-order unification, narrowing, disunification, anti-unification, complexity issues, combination methods, implementation techniques, and applications.
Temur Kutsia - RISC, Johannes Kepler University Linz, Austria
Andrew M. Marshall - Univeristy of Mary Washington, USA
International Workshop on Rewriting Techniques for Program Transformations and Evaluation
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.
Adrian Riesco - Universidad Complutense de Madrid, Spain
Vivek Nigam - fortiss GmbH, Germany
Proof Ground - Interactive Proving Contests
This workshop brings together researchers theorem proving enthusiasts to discuss and compete in “proving contests”. While programming contests (e.g. ACM ICPC, International Olympiad in Informatics) challenge large numbers of participants to solve algorithmic problems within a short time, we envision proving contests to entice proof engineers to formally prove small but interesting problems from mathematics or computer science. An existing contest system ( has been used to organize online proving contests where participants can solve tasks using Coq, Lean, or Isabelle. The workshop will be organized around an on-site contest, supplemented with informal discussions. We welcome participation from users of proof assistants which are not supported by the system.
Maximilian Paul Louis Haslbeck - Technical University of Munich, Germany
Simon Wimmer - Technical University of Munich, Germany
Tobias Nipkow - Technical University of Munich, Germany

30 June

Acronym Name / Description / Organisers Edition
Women in Logic
The Women in Logic workshop (WiL), provides an opportunity to increase awareness of the valuable contributions made by women in the area of logic in computer science. Its main purpose is to promote the excellent research made by women, with the ultimate goal of increasing their visibility and representation in the community, while reducing the feeling of isolation often felt by women in this area. We find these aspects particularly useful to encourage young researchers working in these topics.
Sandra Alves - University of Porto, Portugal
Sandra Kiefer - RWTH Aachen University, Germany
Ana Sokolova - University of Salzburg, Austria
International Workshop on Confluence
Confluence provides a general notion of determinism and has been conceived as one of the central properties of rewriting. Recently there is a renewed interest in confluence research, resulting in new techniques, tool support, certication as well as new applications. The workshop aims at promoting further research in confluence and related properties.
Mauricio Ayala-Rincon - Universidade de Brasilia, Brazil
Samuel Miriam - LIX, France
IFIP Working Group 1.6: Rewriting
The IFIP Working Group 1.6 is one of the working groups of the Technical Committee 1 of the International Federation for Information Processing (IFIP). IFIP is the leading multinational, apolitical organisation in Information & Communications Technologies and Sciences. It is recognised by the United Nations and other world bodies, represents IT Societies from 56 countries or regions, covering all 5 continents with a total membership of over half a million.
Georg Moser - University of Innsbruck, Austria
Martin Avanzini - INRIA, France
Isabelle Workshop
This informal workshop will bring together users and developers of the interactive theorem prover Isabelle. Participants will present their research and projects, including applications of Isabelle, internal developments, add-on tools, and reports on work in progress.
Tobias Nipkow - Technical University of Munich, Germany
Lawrence Paulson - University of Cambridge, UK
Makarius Wenzel -, Germany

5-6 July

Acronym Name / Description / Organisers Edition
Workshop on Homotopy Type Theory/Univalent Foundations
Homotopy type theory is a young and rapidly developing area at the intersection of computer science and mathematics, importing the ideas from abstract homotopy theory to dependent type theory. This workshop aims to bring together researchers interested in all aspects of homotopy type theory and univalent foundations to showcase the new techniques and results in the field.
Benedikt Ahrens - School of Computer Science, University of Birmingham, UK
Chris Kapulkin - Department of Mathematics, Western University, Canada
Geometric and Categorical Structures for Computation and deduction
The purpose of the GeoCat workshop is to offer an open, inspiring and interdisciplinary venue for researchers interested in the interactions between category theory and the formal as well as geometric aspects of computation and deduction. The topics discussed during the workshop will include algebraic topology and concurrency theory, homotopy theory and higher-dimensional rewriting, homotopy and cubical type theory, monoidal categories and string diagrams, linear logic and game semantics, differential, probabilistic, topological and metric interpretations of logic and computations, combinatorial species, automata theory, categorical logic, coalgebraic methods, syntax and semantics of effect and resource calculi, categorical and homological approaches to information theory and entropy, etc. The atmosphere of the workshop will be friendly and propitious for fruitful exchanges and discussions accross the various fields of investigation.
Paul-André Melliès - CNRS - University of Paris, France
Christine Tasson - University of Paris, France
The Coq Workshop
The Coq Workshop series brings together Coq users, developers, and contributors. It focuses on strengthening the Coq community and providing a forum for discussing practical issues, including the future of the Coq software and its associated ecosystem of libraries and tools. Thus, the workshop will be organized around informal presentations, discussions, invited talks as well as thematic sessions. We invite all members of the Coq community to propose informal talks, discussion sessions, or any potential uses of the time allocated to the workshop. Last but not the least, Coq is celebrating its 35th birthday. It was initiated in Paris area by Gérard Huet and Thierry Coquand, later joined by Christine Paulin. Some time will be reserved to retrace the evolution of Coq and highlight the new promises it continues to carry.
Emilio J. Gallego Arias - France INRIA
Hugo Herbelin - France INRIA
Théo Zimmermann - CNRS - INRIA - University of Paris, France
International Workshop on Satisfiability Modulo Theories
The SMT Workshop is focused on bringing together researchers and users of tools and techniques for satisfiability modulo theories. Relevant topics include but are not limited to: * New decision procedures and new theories of interest * Combinations of decision procedures * Novel implementation techniques * Benchmarks and evaluation methodologies * Applications and case studies * Theoretical results
Tjark Weber - Uppsala University, Sweden
François Bobot - CEA, List, France

5 July

Acronym Name / Description / Organisers Edition
International Workshop on Computing with Terms and Graphs
Graphs, and graph transformation systems, are used in many areas within Computer Science: to represent data structures and algorithms, to define models of computation, as a general modelling tool to study complex systems, etc. When computing with graphs rather than terms, common subexpressions can be shared, thus improving the efficiency of computations in space and time. Sharing is ubiquitous in implementations of programming languages: many functional, logic, object-oriented and concurrent calculi are implemented using graphs. TERMGRAPH 2020 will solicit papers describing new results relating to the theory or practical applications of graph transformation systems.
Maribel Fernandez - Kings College London, UK
Patrick Bahr - IT University of Copenhagen
Workshop on Satisfiability Checking and Symbolic Computation
Symbolic Computation is concerned with the algorithmic determination of exact solutions to complex mathematical problems; recent developments in the area of Satisfiability Checking are starting to tackle similar problems but with different algorithmic and technological solutions. The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces of tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of the SC2 workshop is to provide fertile ground to discuss, share knowledge and experience across both communities.
Konstantin Korovin - The University of Manchester, UK
Ilias Kotsireas - Wilfrid Laurier University, Canada


Acronym Name / Description / Organisers Edition
International Workshop on Semantic and formal approaches to COmplexiTy
The SCOT workshop is devoted to the problem of reasoning on the complexity properties of programs in formal and compositional ways. Many approaches have been exploited for that, taking advantage from logic, category theory, denotational semantics, type systems, interpretations \dots This workshop aims at providing a forum of discussion for all issues related to these questions, from foundational aspects on semantics of complexity to automated time or space complexity analysis.
Patrick Baillot - CNRS - ENS Lyon, France
International Workshop on Termination
The Workshop on Termination (WST) traditionally brings together, in an informal setting, researchers interested in all aspects of termination, whether this interest is practical or theoretical, primary or derived. The workshop also provides a ground for cross-fertilization of ideas from the different communities interested in termination (e.g., working on computational mechanisms, programming languages, software engineering, constraint solving, etc.). The friendly atmosphere enables fruitful exchanges leading to joint research and subsequent publications.
Samir Genaim - Universidad Complutense de Madrid, Spain
International Workshop on Automated Reasoning in Quantified Non-Classical Logics
The ARQNL workshop aims at fostering the development of proof calculi, Automated Theorem Proving systems and model finders for all sorts of quantified, i.e first- or higher-order, non-classical logics. The workshop will provide a forum for researchers to present and discuss recent developments in this area. These contributions may range from theory to system descriptions and implementations. Contributions may also outline relevant applications, describe problem formalizations, example problems and benchmarks that use a quantified non-classical logic. We welcome contributions from computer scientists, linguists, philosophers, and mathematicians. The workshop will consists of invited talks, peer-reviewed paper presentations and system demonstrations.
Christoph Benzmüller - Freie Universität Berlin, Germany
Jens Otten - University of Oslo, Norway
Theorem Prover Components for Educational Software
(Computer) Theorem Proving (TP) is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss systems already prototyping some of the features mentioned.
João Marcos - Federal University of Rio Grande do Norte, Brazil
Walther Neuper - TUG University of Technology, Austria
Pedro Quaresma - University of Coimbra, Portugal
Deduction Mentoring Workshop
The DeMent 2020 workshop will provide mentoring and help on career development for young researchers working in automated reasoning, with the overall aim to attract and help them to establish themselves as researchers in automated reasoning. The workshop will address challenges of the academic life and give insight in industrial research. For doing so, the workshop will include talks from leading experts of automated reasoning in academia and industry, and will also include presentations on career-planning. The workshop aims to reach and attract master students, PhD students and young postdocs as participants.
Laura Kovacs - Vienna University of Technology, Austria
The workshop aims at discussing recent developments in implementing, applying benchmarking and comparing first-order theorem provers and their combinations with other systems. The workshop is going to shed the light on problems such as - what is essential for substantial progress in theorem proving tools; - what are the best implementation principles to be used; - what are the best heuristics and strategies, depending on application areas; - both successful and unsuccessful case studies; - missing features in modern theorem provers. The workshop will also overview the most recent advances made in Vampire.
Laura Kovacs - Vienna University of Technology, Austria
Andrei Voronkov - The University of Manchester, UK
Tutorial on Hacking Zipperposition
Zipperposition is a highly modular first- and higher-order superposition-based theorem prover written in OCaml. In this tutorial, you will learn of its main modules, how to hack them and how to create new ones. Our aim is that after this tutorial, you can easily prototype your own calculi in Zipperposition. The tutorial will consist in three parts: 1. an introduction to OCaml and Zip
Sophie Tourret - MPII, Saarbrücken, Germany
Alexander Bentkamp - Vrije Universiteit Amsterdam, Netherlands
Simon Cruanes - Imandra Inc., Austin, Texas, USA
Petar Vukmirović - Vrije Universiteit Amsterdam, Netherlands