@InProceedings{PoplMark,
  author =	 {Brian E. Aydemir and Aaron Bohannon and Matthew
                  Fairbairn and J. Nathan Foster and Benjamin
                  C. Pierce and Peter Sewell and Dimitrios Vytiniotis
                  and Geoffrey Washburn and Stephanie Weirich and
                  Steve Zdancewic},
  title =	 {{M}echanized {M}etatheory for the {M}asses: {T}he
                  {\sc PoplMark} {C}hallenge},
  booktitle =	 {Theorem Proving in Higher Order Logics: {TPHOLs}
                  2005},
  editor =	 {Tom Melham and Joe Hurd},
  series =	 {LNCS},
  year =	 2005,
  publisher =	 {Springer-Verlag}
}

@Misc{Barras-Werner-JAR,
  author =	 {Bruno Barras and Benjamin Werner},
  title =	 {{Coq} in {Coq}},
  howpublished = {To appear in Journal of Automated Reasoning}
}

@article{Nipkow-JAR01,
  author =	 {Tobias Nipkow},
  title =	 {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
  journal =	 {Journal of Automated Reasoning},
  volume =	 26,
  pages =	 {51--66},
  year =	 2001
}
