| Foreword |
| Session 1 | |
| 09:15 - 10:15 | Invited Talk: Jose Meseguer Extensible Symbolic System Analysis (paper, talk) |
| 10:15 - 10:45 | Coffee break |
| Session 2 | |
| 10:45 - 11:15 | Peter Hibbs, Paliath Narendran and Shweta Mehto Unification Modulo Common List Functions (paper, talk) |
| 11:15 - 11:45 | Franz Baader and Barbara Morawska Matching with respect to general concept inclusions in the Description Logic EL (paper, talk) |
| 11:45 - 12:15 | Philippe Balbiani and Tinko Tinchev Unification in the normal modal logic Alt1 (paper, talk) |
| 12:15 - 12:35 | Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Catherine Meadows, Paliath Narendran and Christophe Ringeissen On Asymmetric Unification and the Combination Problem in Disjoint Theories (paper, talk) |
| 12:35 - 12:55 | Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran and Christophe Ringeissen Hierarchical Combination of Matching Algorithms (paper, talk) |
| 13:00 - 14:30 | Lunch Break |
| Session 3 | |
| 14:30 - 15:30 | Invited Talk: Jordi Levy On the Limits of Second-Order Unification (paper, talk) |
| 15:30 - 16:00 | Leonardo Manuel Cabrer and George Mectalfe From Admissibility to a New Hierarchy of Unification Types (paper, talk) |
| 16:00 - 16:30 | Coffee Break |
| Session 4 | |
| 16:30 - 17:00 | Maria Paola Bonacina and David Plaisted Constraint Manipulation in SGGS (paper, talk) |
| 17:00 - 17:30 | Tatyana Novikova and Vladimir Zakharov Two-sided unification is NP-complete (paper, talk) |
| 17:30 - 18:00 | Alexander Baumgartner, Temur Kutsia, Jordi Levy and Mateu Villaret Nominal Anti-Unification (paper, talk) |
| Session 5 | |
| 18:00 - 18:30 | Andrea Vezzosi and Andreas Abel A Categorical Perspective on Pattern Unification (paper, talk) |
| 18:30 - 19:00 | Beta Ziliani and Matthieu Sozeau Towards a better-behaved unification algorithm for Coq (paper, talk) |