Although the formalization of probabilistic programs already has several applications in the fields of security proofs and artificial intelligence, formal verification experiments are still underway to support the many features of probabilistic programming. We report on the formalization in the Coq proof assistant of a syntax and of an evaluation relation for a probabilistic programming language. We use dependent types in a crucial way since our syntax is intrinsically-typed and since the semantic values are dependent records. Thanks to the features of Coq, we can use notations to hide details about types when writing concrete examples. We can also use the the resulting formalization to perform formal verification proofs akin to equational reasoning for probabilistic programs.