Here are some publications related to your question:

[Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998.](http://homepages.inf.ed.ac.uk/rpollack/export/believing.ps.gz)

[Pollack-inconsistency, Freek Wiedijk](http://www.cs.ru.nl/~freek/pubs/rap.pdf) Freek demonstrates the most popular proof assistants are Pollack inconsistent.

In an [internet post](https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00032.html?checked_cas=2) Pollack discusses Coq coercions:
>The problem is that Coq coercions are informally specified and behave
somewhat unpredictably.  A formal theory of coercions, such as Luo's
Coercive subtyping (with proof theory and semantics) would eliminate
this question of the meaning of statements using coercions.  However,
the proof theory of coercions is complicated.