What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?
The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of reductions, but clarify the presentation in my opinion. 
Let's assume your language is given by
the following grammar.
$$
\newcommand{\PROGRAM}[1]{\mathsf{#1}}
\newcommand{\FV}[1]{\mathsf{fv}(#1)}
\newcommand{\DOM}[1]{\mathsf{dom}(#1)}
\newcommand{\VERTICAL}{\;  \mid\hspace{-3.0pt}\mid \; }
\newcommand{\CALLCC}{\PROGRAM{callcc}}
\newcommand{\CONT}[1]{\mathsf{Cont}(#1)}
\newcommand{\THROW}{\PROGRAM{throw}}
\newcommand{\infer}[2]{\frac{\displaystyle{ #1 }}{\displaystyle{ #2 }}}
\newcommand{\ZEROPREMISERULE}[1]{\infer{-}{#1}}
\newcommand{\FS}{\rightarrow}
\newcommand{\RED}{\rightarrow}
\newcommand{\ONEPREMISERULE}[2]{\infer{#1}{#2}}
\newcommand{\TYPES}[3]{#1 \vdash #2 : #3}
\newcommand{\TWOPREMISERULE}[3]{\infer{#1 \quad #2}{#3}}
   M ::= x \VERTICAL \lambda x.M \VERTICAL MM \VERTICAL ... \VERTICAL \CALLCC \VERTICAL \THROW
$$
Here $\CALLCC$ and $\THROW$ are seen as constants although we could also have defined them in different ways.
Let us denote by $\FV{M}$ the free variables of the program $M$.
Types could be something like this:
$$
        \alpha\
                ::=\
        \alpha \FS\alpha
\VERTICAL \PROGRAM{Int} \VERTICAL
        ...
                \VERTICAL
        \CONT{\alpha}
$$
Here $\CONT{\alpha}$ is the type of continuations with final answer
type $\alpha$.
The constants $\CALLCC$ and $\THROW$ are values and have the following types.
$$
        \ZEROPREMISERULE
        {
          \TYPES{\Gamma}{\CALLCC}{(\CONT{\alpha} \FS \alpha) \FS \alpha}
        }
                \qquad
        \ZEROPREMISERULE
 {
                \TYPES{\Gamma}{\THROW}{\CONT{\alpha} \FS \alpha \FS \beta}
        }
$$
Depending on your use-case, the type variables may be quantified.
Reductions are defined with the help of configurations. 
A configuration is a pair $(M, \sigma)$ such that $M$ is a
program and $\sigma$, the continuation map, ranged over by
$\sigma, ...$, maps each $k \in \FV{M}$ of type $\CONT{\alpha}$ to an appropriately typed program.
Then
reductions are of the form $(M, \sigma) \RED (N,                                                             
\sigma')$. For  call-by-value, the reductions are generated as usual, with the following additions for $\CALLCC$
and $\THROW$.
$$
        \ONEPREMISERULE
        {
                k, x\ \text{fresh}
        }
        {
                (E[\CALLCC\ V], \sigma) \RED (E[V\;k], \sigma \cdot k \mapsto \lambda x.E[x])
        }
                \quad
        \ONEPREMISERULE
        {
                \sigma(k) = M
        }
        {
                (E[\THROW\ k\ V], \sigma) \RED (MV, \sigma)
        }
$$
Here $V$ over ranges over values, and
$E[\cdot]$ over the usual call-by-value reduction contexts. The two new constants give rise to the following evaluation contexts: $\CALLCC\ E[\cdot]$, $\THROW\ E[\cdot]\ M$
and $\THROW\ V\ E[\cdot]$.

Note that (1) does not use continuation maps to define the CBV semantics of $\CALLCC$
 and $\THROW$. Instead a run-time value is introoduced. The two approaches are equivalent.

As to evaluation order, $\CALLCC$ enriches the power of contexts and can distinguish  programs by application that are
  indistinguishable in the absence of continuations: 

$$
  \newcommand{\ARGFC}{\PROGRAM{argfc}}
  \ARGFC  = \CALLCC\ \lambda k.(\THROW\ {k}\ {\lambda
  x.(\THROW\ {k}\ {\lambda y.x}}))
  $$

This is the classic example of calling a function once, but
  returning twice. e.g. in
  $$
  (\lambda x.(x\; 1);(x\; 2))\ \ARGFC = 1
  $$
  and
  $$
  (\lambda x.\lambda y.(x\; 1);(y\; 2))\ \ARGFC\ \ARGFC = 2
  $$

with $M;N$ being the sequential composition of $M$ and $N$, binding
more tightly than $\lambda$-abstraction.  The reason is that
continuations carry information about contexts that may be returned
(jumped) to later.




J. G. Riecke, H. Thielecke, Typed Exceptions and Continuations Cannot Macro-Express Each Other (Postscript file).
R. Harper, B. F. Duba, D. MacQueen, Typing First-Class Continuations in ML.
H. Thielecke, Continuations, functions and jumps.