Edit: my guess in the first paragraph below is wrong! Ugo Dal Lago pointed out to me a later paper by Martin Hofmann (appeared in POPL 2002), of which I was unaware, showing (as a corollary of more general results) that the system from the ATTPL book is in fact complete for $\mathsf P$ (in spite of not being able to compute every function in $\mathsf{FP}$). So, to my surprise, the answer to the main question is yes.
Concerning the system you are referring to (from the ATTPL book), I am pretty sure it cannot decide every language in $\mathsf P$. It certainly cannot compute every function in $\mathsf{FP}$: as mentioned in the notes of that chapter, that system is taken from Martin Hofmann's LICS 1999 paper ("Linear types and non-size-increasing polynomial time computation"), in which it is shown that the representable functions are polytime and non-size-increasing, which excludes lots of polytime functions. It also seems to give a serious limitation on the size of the tape of the Turing machines you can simulate in that language. In the paper, Hofmann shows that you can encode linear space computation; my guess is that you will not be able to do much more, i.e., the class corresponding to that system is roughly the problems solvable simultaneously in polytime and linear space.
Concerning your second question, there are several $\lambda$-calculi that can solve exactly the problems in $\mathsf P$. Some of them are mentioned in the notes of the ATTPL chapter you are referring to (Sect. 1.6): Leivant's tiered $\lambda$-calculus (see his POPL 1993 paper, or the paper with Jean-Yves Marion "Lambda Calculus Characterizations of Poly-Time", Fundamenta Informaticae 19(1/2):167-184, 1993), which is related to Bellantoni and Cook's characterization of $\mathsf{FP}$; and the $\lambda$-calculi derived from Girard's light linear logic (Information and Computation, 143:175–204, 1998) or from Lafont's soft linear logic (Theoretical Computer Science 318(1-2):163-180, 2004). Type systems arising from these latter two logical systems and ensuring polytime termination (while still enjoying completeness) may be found in:
Patrick Baillot, Kazushige Terui. Light types for polynomial time computation in lambda calculus. Information and Computation 207(1):41-62, 2009.
Marco Gaboardi, Simona Ronchi Della Rocca. From light logics to type assignments: a case study. Logic Journal of the IGPL 17(5):499-530, 2009.
You'll find lots of other references in those two papers.
To conclude, let me expand on Neel Krishnaswami's remark. The situation is a bit subtle. All of the above $\lambda$-calculi may be seen as restrictions of more general calculi, in which you can compute much more than just the polytime functions, say for example system F. In other words, you define a property $\Phi$ of system F programs $P:\texttt{string}\rightarrow\texttt{bool}$ such that:
soundness: $\Phi(P)$ implies that the language decided by $P$ is in $\mathsf P$;
completeness: for every $L\in\mathsf P$, there is a system F program $P$ deciding $L$ such that $\Phi(P)$.
The interest is that the property expressed by $\Phi$ is purely syntactic and, in particular, decidable. Therefore, completeness can only hold in an extensional sense: if $L$ is your favorite language in $\mathsf P$ and if $P$ is your favorite algorithm for deciding $L$ expressed in system F, it may be that $\Phi(P)$ does not hold. All you know is that there is some other system F program $P'$ deciding $L$ and such that $\Phi(P')$ holds. Unfortunately, it may happen that $P'$ is much more contrived than your $P$. Indeed, completeness is proved by encoding polynomially-clocked Turing machines as system F terms satisfying $\Phi$. Therefore, the only guaranteed way of solving $L$ using your favorite algorithm is implementing that algorithm on a Turing machine and then translating it in system F using the encoding given in the completeness proof (your own encoding may not work!). Not exactly the most elegant solution in terms of programming... Of course, in many cases the "natural" program $P$ does satisfy $\Phi$. However, in many other cases it does not: in the LICS 1999 paper mentioned above, Hofmann gives insertion sort as an example.
Intentionally complete type systems, which are able to type exactly the polytime programs of the wider language (system F in my example above) do exist. Of course, they are undecidable in general. See
Ugo Dal Lago, Marco Gaboardi. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8(4), 2011.
