Shallow versus Deep Embeddings

When encoding a logic into a proof assistant such as Coq or Isabelle, a choice needs to be made between using a shallow and a deep embedding. In a shallow embedding logical formulas are written directly in the logic of the theorem prover, whereas in a deep embedding logical formulas are represented as a datatype. What are the advantages and limitations of the various approaches? Are there any guidelines available for determining which to use? Is it possible to switch between the two representations in any systematic fashion? As motivation, I would like to encode various security related logics into Coq and am wondering what the pros and cons of the different approaches are.