Published: 21st December 2010|
|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|
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.
London, December 2010