Pure type systems and let-expressions
There is a definite dearth of literature on how to add let bindings to PTSes or dependently typed systems, though I do seem to recall this reference:

Paolo Severi, Pure Type Systems with Definitions.

From a theoretical perspective, you want to have the intuitive rule:

$$\frac{\Gamma\vdash t[M/x] : A[M/x]\qquad \Gamma\vdash M:B}{\Gamma\vdash\mbox{let}\ x :B :=M\ \mbox{in}\ t\ :\ A} $$

But this doesn't help explain much about how to perform type checking and conversion, which is a quite subtle subject.