Shallow versus Deep Embeddings
What are the advantages and limitations of the various approaches?



Pros of deep embeddings : You can prove and define things by induction on formulas' structure. Examples of interests are the size of a formula. 
Cons of deep embeddings: You have do deal explicitly with binding of variables. That's usually very laborious. 



  Are there any guidelines available for determining which to use ?


Shallow embeddings are very useful to import result proved in the object logic. For instance, if you have prove something in a small logic (e.g. separation logic) shallow
embeddings can be a tool of choice to import your result in Coq.

On the other side, deep embedding are almost mandatory when you want to prove 
meta-theorems about the object logic (like cut-elimination for instance).    


  Is it possible to switch between the two representations in any systematic fashion?


The idea behind the shallow embedding is really to work directly in a model of the object formulas. Usually people will maps an object formula P directly (using notations or by doing the translation by hand) to an inhabitant of Prop. Of course, there are inhabitants of Prop which cannot be obtained by embedding a formula of the object logic. Therefore you lose some kind of completeness. 

So it is possible to send every result obtained in a deep embedding setting through an interpretation function. 

Here is a little coq example: 


Inductive formula : Set :=
    Ftrue : formula
  | Ffalse : formula
  | Fand : formula -> formula -> formula 
  | For : formula -> formula -> formula.

Fixpoint interpret (F : formula) : Prop := match F with 
    Ftrue => True
  | Ffalse => False
  | Fand a b => (interpret a) /\ (interpret b)
  | For a b => (interpret a) \/ (interpret b)
 end.

Inductive derivable : formula -> Prop := 
    deep_axiom : derivable Ftrue
  | deep_and : forall a b, derivable a -> derivable b -> derivable (Fand a b)
  | deep_or1 : forall a b, derivable a -> derivable (For a b)
  | deep_or2 : forall a b, derivable b -> derivable (For a b).

Inductive sderivable : Prop -> Prop := 
    shallow_axiom : sderivable True 
  | shallow_and : forall a b, sderivable a -> sderivable b -> sderivable (a /\ b)
  | shallow_or1 : forall a b, sderivable a -> sderivable (a \/ b)
  | shallow_or2 : forall a b, sderivable b -> sderivable (a \/ b).

(* You can prove the following lemma: *)
Lemma shallow_deep : 
   forall F, derivable F -> sderivable (interpret F).

(* You can NOT prove the following lemma :*)
Lemma t : 
   forall P, sderivable P -> exists F, interpret F = P.