UNIF 2009
August 2, 2009. Montreal, Canada


UNIF is the main international meeting on unification. Unification is concerned with the problem of identifying given terms, either syntactically or modulo a given logical theory. Syntactic unification is the basic operation of most automated reasoning systems, and unification modulo theories can be used, for instance, to build in special equational theories into theorem provers.

The aim of UNIF 2009 is to bring together people interested in unification, present recent (even unfinished) work, and discuss new ideas and trends in unification and related fields. This includes scientific presentations, but also descriptions of applications and software using unification as a strong component.

UNIF 2009, the 23nd International Workshop on Unification, is colocated with the 22nd International Conference on Automated Deduction (CADE 22 ) in Montreal.

This workshop is the 23nd in the series: UNIF'87 (Val D'Ajol, France), UNIF'88 (Val D'Ajol, France), UNIF'89 (Lambrecht, Germany), UNIF'90 (Leeds, England), UNIF'91 (Barbizon, France), UNIF'92 (Dagstuhl, Germany), UNIF'93 (Boston, USA), UNIF'94 (Val D'Ajol, France), UNIF'95 (Sitges, Spain), UNIF'96 (Herrsching, Germany), UNIF'97 (Orléans, France), UNIF'98 (Rome, Italy), UNIF'99 (Frankfurt, Germany), UNIF'00 (Pittsburgh, USA), UNIF'01 (Siena, Italy), UNIF'02 (Copenhagen, Denmark). UNIF'03 (Valencia, Spain). UNIF'04 (Cork, Ireland). UNIF'05 (Nara, Japan). UNIF'06 (Seattle, USA). UNIF'07 (Paris, France). UNIF'08 (Hagenburg, Austria). 

2009 Schedule

2009 UNIF/ADDCT Proceedings



The meeting will include one invited talk (tentatively), contributed talks, and social time to discuss current topics of interest, which include (but are not limited to):
Unification Algorithms
Higher-Order Unification
String Unification
Context Unification
Combination problems
Typed Unification
Constraint Solving
Tree Descriptions
Type Checking and Type Inference
Automated Deduction
Functional and Logic Programming
Computational Linguistics

Important dates

Paper submission May 30, 2009 <-- Extended Deadline
Notification June 15, 2009
Workshop August 2, 2009

Submission and Publication

There are three categories of submissions:

Papers should be submitted using the automated submission system.

Papers in all categories will be peer-reviewed. Submitted papers (PDF or PostScript) should not exceed 10 pages and should be written in LaTeX with the following settings: 11pt, one column, a4paper and standard margins. The paper may include, in addition, an appendix containing technical details, which reviewers may read or not, at their discretion.

Informal proceedings of accepted contributions will be available on-line. A hard copy will be distributed at the workshop to registered participants.

Program Committee

Franz Baader TU Dresden, Dresden, Germany
Santiago Escobar Universidad Politecnica de Valencia, Valencia, Spain
Christopher Lynch
Clarkson University, Potsdam, New York, USA
Paliath Narendran University at Albany--SUNY, Albany, New York, USA
Christophe Ringeissen LORIA - INRIA, Nancy, France

Program co-chairs:    Christopher Lynch and Paliath Narendran