Preface Volume 58, Issue 1

AbstractMechanised Reasoning about Languages with Variable Binding 2001This volume contains the Proceedings of the Workshop on Mechanised Reasoning about Languages with Variable Binding (MERLIN 2001), which was held in conjunction with IJCAR 2001, the International Joint Conference on Automated Reasoning. The Workshop took place in Siena, Italy, on the 18th June 2001, and was organized by the editors of this volume.Currently, there is considerable interest in the use of computers to encode (operational) semantic descriptions of programming languages. Such encodings are often done within the metalanguage of a theorem prover or related system. The encodings may require the use of variable binding constructs, inductive definitions, coinductive definitions, and associated schemes of (co)recursion. The broad aims of MERLIN 2001 were to provide researchers with a forum to review state of the art results and techniques, and to present recent and new progress in the areas of •the automation of the metatheory of programming language semantics, particularly work which involves variable binding; and•theoretical and practical problems of encoding variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures.Automating variable binding and its associated properties is notoriously difficult, but such automation pervades the encoding of programming language semantics. Thus theoretical methods and practical techniques which simplify the definition and implementation of such encodings will prove very useful to the community. Ultimately we hope that advances in these areas will have significance for the general programming language community.The papers in this volume were reviewed by the following programme committee: •Simon Ambler (University of Leicester)•Roy Crole (Chair; University of Leicester)•Amy Felty (University of Ottawa)•Andrew Gordon (Microsoft Research, Cambridge)•Furio Honsell (University of Udine)•Tom Melham (University of Glasgow)•Frank Pfenning (Carnegie Mellon University)Alberto Momigliano was the local organizer, and devoted a lot of time to the preparations for MERLIN 2001.The editors would like to thank the other committee members for their input into all stages of the organization of MERLIN 2001, but especially that of reviewing the paper submissions. We thank Andrew Pitts, Cambridge University, for giving an excellent invited talk on A First Order Theory of Names and Binding. We would also like to thank Dieter Hutter, IJCAR Workshop Chair, and Fabio Massacci, IJCAR Conference Chair, who put enormous efforts into the organization of all of the IJCAR Workshops. Finally we thank the authors, participants, and others who contributed to MERLIN 2001