What is the benefit of Krivine's notation? I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus.  For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ (with the normal convention that function application associates to the left, so it actually means $\lambda f . \lambda x . \lambda y . ((f\ x)\ y)$) is written $\lambda f . \lambda x . \lambda y . (f)\ x\ y$ (with a similar convention that it actually means $\lambda f . \lambda x . \lambda y . ((f)\ x)\ y$).  I do not see the point of having another pair of parentheses around the innermost $f$.  Why do people use Krivine's notation instead of the usual one?
I'm assuming you mean Krivine's notation from Lambda Calculus: Types and Models.

This notation, used as a data representation, makes many algorithms on lambda-terms simpler to implement and prove correct. That is, given a  lambda term $f\; e_1\; e_2\; \ldots\; e_n$, you want to view it as a head $f$, together with a list of arguments $[e_1,  e_2, \ldots, e_n]$. 

For example, suppose you want to compare two terms $f\;e_1\;\ldots\; e_n$ with $g\;t_1\;\ldots\;t_n$. It is often most natural to compare the heads $f$ and $g$ first, and not even look at the $(e_i, t_i)$ pairs unless that comparison succeeds. (This often comes up in implementations of higher-order unification.) 

See Cervesato and Pfenning's paper A Linear Spine Calculus for a formalization of this idea.