@inproceedings{WildmoserN-TPHOLs04,
  author =  "Martin Wildmoser and Tobias Nipkow",
  title =   "Certifying Machine Code Safety: Shallow versus Deep Embedding",
  booktitle = "Proc.\ 17th Int.\ Conf.\ on Theorem Proving in Higher Order Logics (TPHOLs'04)",
  series= LNCS,
  volume = 3223,
  publisher = "Springer Verlag",
  month= "September",
  year =    2004,
  editor = "Konrad Slind and Annette Bunker",
  pages = "305--320",
  url =  "\url{http://www4.in.tum.de/~wildmosm/publications/WildmoserN-TPHOLs04.pdf}"
}