Citing Entries

The following gives an example of the preferred way for citing entries in the AFP:

M. Jaskelioff and S. Merz, Proving the Correctness of Disk Paxos. In: G. Klein, T. Nipkow, and L. Paulson (ed), The Archive of Formal Proofs, http://afp.sf.net/entries/DiskPaxos.shtml, June 2005, Formal proof development.

The bibtext entry for this would be:

@incollection{Jaskelioff-Merz-AFP05,
  author =       {Mauro Jaskelioff and Stephan Merz},
  title =        {Proving the Correctness of Disk Paxos},
  booktitle =    {The Archive of Formal Proofs},
  editor =       {Gerwin Klein and Tobias Nipkow and Lawrence Paulson},
  publisher =    {\url{http://afp.sf.net/entries/DiskPaxos.shtml}},
  month =        Jun,
  year =         2005,
  note =         {Formal proof development},
}