Published: 21st December 2010
DOI: 10.4204/EPTCS.42
ISSN: 2075-2180

EPTCS 42

Proceedings 24th International Workshop on
Unification
Edinburgh, United Kingdom, 14th July 2010

Edited by: Maribel Fernandez

Preface
Nominal Unification Revisited
Christian Urban
1
Unification modulo a partial theory of exponentiation
Deepak Kapur, Andrew Marshall and Paliath Narendran
12
A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints
Sunil Kothari and James Caldwell
24
Towards Correctness of Program Transformations Through Unification and Critical Pair Computation
Conrad Rau and Manfred Schmidt-Schauß
39
On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity
Paliath Narendran, Andrew Marshall and Bibhu Mahapatra
54

Preface

EPTCS: 24th International Workshop on Unification - UNIF2010

The UNIF series of workshops promotes research and collaboration in the area of unification theory and related fields, including constraint solving and applications of unification to theorem proving and programming languages. It encourages the presentation of new directions, developments and results, as well as tutorials on existing knowledge in this area.

The first International Workshop on Unification took place in 1987, and since then the workshop has run every year, serving as a forum for researchers to present recent work and work in progress, and to discuss new ideas and trends on topics such as: E-unification, narrowing, matching algorithms, specific unification algorithms, higher-order and nominal unification, constraints, disunification, combination problems, complexity analysis, implementation techniques, and applications to type checking and reconstruction, automated theorem proving, programming language design, etc.

The 24th International Workshop on Unification (UNIF 2010) was held in Edinburgh on the 14 July 2010, associated to RTA and IJCAR (part of FLoC, the Federated Logic Conference). Eight papers were presented at UNIF 2010. In addition, the programme included two invited talks, by Claude Kirchner and by Christian Urban.

This volume contains a selection of the papers presented at UNIF 2010, including an invited contribution by Christian Urban, which gives a gentle introduction to nominal unification with simplified proofs that are the basis for its formalisation in a theorem prover.

The Programme Committee of UNIF 2010 consisted of:

I would like to thank all those who contributed to UNIF 2010, in particular the authors of submitted papers, the invited speakers who kindly accepted to present their work at UNIF, and the local organisers of the FLoC conference. Easychair was used to manage submissions and to generate the pre-proceedings. Special thanks to the Programme Committee members for their support and efficient work, and to EPTCS for the publication of the final proceedings.




Maribel Fernández



London, December 2010