@InProceedings{Vestergaard-Brotherston:RTA01,
  author    = "Ren{\'e} Vestergaard and James Brotherston",
  title     = "A Formalised First-Order Confluence Proof for the {$\lambda$}-Calculus using One-Sorted Variable Names
               (\emph{{B}arendregt was right after all {\ldots} almost})",
  booktitle = "Proceedings of RTA-12",
  editor    = "Aart Middeldorp",
  series    = "LNCS",
  volume    = 2051,
  pages     = "306--321",
  publisher = "Springer-Verlag",
  year      = 2001
}