What is the benefit of Krivine's notation?
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.