@ARTICLE{Vestergaard-Brotherston:IandC03,
  author =       {Ren{\'e} Vestergaard and James Brotherston},
  title =        {A Formalised First-Order Confluence Proof for
                  the {$\lambda$}-Calculus using One-Sorted
                  Variable Names},
  journal =      {Information and Computation},
  editor =       "Aart Middeldorp",
  year =         {2003},
  volume =       183,
  number =       2,
  pages =        {212 -- 244},
  note =         {Special edition with selected papers from RTA01},
}