UNIF 2009

Overview

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

Slides

Topics

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

E-unification
Unification Algorithms
Higher-Order Unification
String Unification
Context Unification
Combination problems
Disunification
Typed Unification

Related Topics

Constraint Solving
Tree Descriptions
Matching
Narrowing

Applications

Type Checking and Type Inference
Automated Deduction
Rewriting
Functional and Logic Programming
Grammars
Computational Linguistics

Implementations

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:

Extended abstracts are preliminary reports of work in progress. They may range in length from a couple of pages to the full 10 pages and will be judged based on the expected level of interest for the UNIF community.
Original papers contain original research and sufficient detail to assess the merits and relevance of the submission. Given the informal style of the workshop, work in progress will be welcome. Simultaneous submittions are not allowed.
Presentation-only papers describe work recently published or submitted and will not be included in the proceedings. We see this as a way to provide additional access to important developments that workshop attendees may be unaware of.

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