@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 ... almost})",
  booktitle =    "Proceedings of RTA-12",
  editor =       "Aart Middeldorp",
  series =      "LNCS",
  year        = 2001,
  volume      = 2051,
  publisher   = "Springer-Verlag",
}