Proper morphisms of schemes are defined to be separated, universally closed, and of finite type, for instance see The The Stacks Project - Tag 0CL4.
In section 10.3 of The Rising Sea: Foundations of Algebraic Geometry, starting with the notion of proper maps of topological spaces, Vakil motivates the requirement for being separated and emphasises the role of being universally closed.
What about finite type? Is there some important theorem about proper morphisms that does not work without the (locally of) finite type assumption, is it to prevent some counter-intuitive examples, or is it just because it is defined this way in EGA II?
1) Under the hypothesis that the scheme morphism $f:X\to S$ is separated and finite type we have the nice equivalence $$ f \operatorname {satisfies the valuation criterion} \iff f \operatorname {is proper }$$ To prove that the valuation criterion implies the universal closedness of $f$, the hypothesis that $f$ be of finite type is needed : Mumford-Oda, Chapter II, Proposition 6.8, page 78-80.
2) Given a proper map of schemes $f:X\to Y$ with $Y$ locally noetherian and a coherent sheaf $\mathcal F$ on $X$, the higher direct images $R^qf_*(\mathcal F) \;(q\geq0)$ are coherent sheaves on $Y$.
The proof requires $f$ to be of finite type: EGA III$_1$, Théorème 3.2.1, page 116.