English Reference for the Bénabou-Roubaud theorem The Bénabou-Roubaud theorem links fibrational descent theory with monadicity. Particularly, it says that given a bifibration satisfying the Beck-Chevalley condition w.r.t some arrow $p$ in the base category (with pullbacks), the category of descent data is canonically equivalent to the category of algebras of the monad induced by $p_!\dashv p^\ast$.
Where can I find a proof of this result in English?
For instance, there's a paper by Obradovic J titled The Bénabou-Roubaud monadic descent theorem via string diagrams, but I can't find an actual copy.
Also, since some sources cite unpublished work of Beck's for this result as well, is the unpublished work of Beck available anywhere?
 A:  This is incoporated into an existing answer for several reasons, e.g. to avoid moving it to the front page. I only noticed this reference now, when I continued to work on this. While the 'translation' answer does not lend itself to harboring the following, the 'pointing out a published announcement of a translation' answer does, so I add it herein. The old version, and what I add to the thread here, are roughly of the same genre, roughly, 'pointing to a reference'. 
A resource very relevant to your question 

Where can I find a proof of this result in English?

is:
Fernando Lucatelli Nunes: Kan extensions and descent theory. Talk at the conference 'Category Theory', University of Aveiro, Portugal, 2015
an abstract of which contains 

In particular, in this presentation, we shall talk about the pseudo-Kan extensions and give a proof of the Bénabou-Roubaud theorem.

A reference even more relevant to the reference-request-part of your question (and in particular one which extensively clarifies the not-unproblematic assumption "We always assume that the pointwise right pseudo-Kan extensions exist." in the above talk) is:
Fernando Lucatelli Nunes: Pseudo-Kan extensions and descent theory.    arXiv:1606.04999
EDIT: old version of this answer: 
(
Strictly speaking I do not consider the following an answer, since it only gives what seems a possible way to what you are asking for, yet relevant, too large for the comment boxes, and apparently you seem not aware of it, so it seems useful to mention this.
There exists a blog, which however seems dormant since 2010, and which to directly link I find inappropriate, in which we read something directly relevant to your question:

As far as Benabou-Roubaud’s paper I indeed enjoyed the posts by Bunge and Benabou explaining the (sometimes subtle) differences from the known work of Beck (which fit into my earlier impressions).
  I have retyped few years ago the C.R. paper into LaTeX, translated into English; though I should still recheck for typoses. I intended to post it to the arXiv as it is short and historically and pedagogically important while unavailable online and I hereto ask Prof. Benabou for permission (after rechecking the file together for correctness).
  [I should remark that SGA1 is also on the arXiv, since 2002.]

You may try finding out who wrote this and contact them.
)
A: The following is a reasonably literal translation (made by me from the French original) of the published article: Jean Bénabou, Jacques Roubaud. Monades et descente. C. R. Acad. Sc. Paris, t. 270 (12 Janvier 1970), Série A, 96–98. [Edit by DR Apr 2020: additional notes moved to the bottom of the answer]
Beginning of reasonably literal translation.

ALGEBRA. -- Monads and descent.
  Note (${}^\ast$) by Jean Bénabou and Jacques Roubaud.
  Transmitted by Henri Cartan.
 By means of category theory, we interpret the 'descent data' in a simple and natural manner as 'algebras over a monad'.
        This allows one, in very general situations, to recognize whether a morphism is a descent morphism or an effective descent morphism. 
1. The bifibrations of Chevalley, and descent. -- In the following, $P\colon \textbf{M}\rightarrow \textbf{A}$ denotes a bifibrant functor $({}^1)$.
  If $A$ is an object of $\textbf{A}$ the fiber over $A$ is denoted $\textbf{M}(A)$.
  We assume that $A$ has all binary pullbacks.
1.1. The monad associated with a morphism. -- Let $a\colon A_1\rightarrow A_0$ be a morphism of $\textbf{A}$.
  We denote the inverse image functor (resp. direct image functor) by 
$a^\ast\colon\textbf{M}(A_0)\rightarrow\textbf{M}(A_1)\qquad$ (resp. $a_\ast\colon\textbf{M}(A_1)\rightarrow\textbf{M}(A_0)$) 
and we denote the canonical natural transformations which make $a_\ast$ a left-adjoint of $a^\ast$ by
$\eta^a\colon\quad 1_{\textbf{M}(A_1)}\rightarrow a^\ast a_\ast;\qquad$ $\varepsilon^a\colon\quad a_\ast a^\ast\rightarrow 1_{\textbf{M}(A_0)}$
This adjunction defines $({}^2)$ a monad $\textbf{T}^a=(T^a,\mu^a,\eta^a)$ on $\textbf{M}(A_1)$, where
$T^a = a^\ast a_\ast\colon\quad \textbf{M}(A_1)\rightarrow\textbf{M}(A_1)$ ${}\qquad$ and ${}\qquad$ $\mu^a=a^\ast\varepsilon^a a_\ast\colon\quad T^a\circ T^a\rightarrow T^a$.
We denote by $\textbf{M}^a$ the category $\textbf{M}(A_1)^{(\textbf{T}^a)}$ of algebras of the monad $\textbf{T}^a$, and by
$U^{\textbf{T}a}\colon\quad\textbf{M}^a\rightarrow\textbf{M}(A_1)$ ${}\quad$ and ${}\quad$ $\Phi^a\colon\quad\textbf{M}(A_0)\rightarrow\textbf{M}^a$
the canonical functors.
1.2. Chevalley condition. $({}^3)$. -- We say $P$ is a Chevalley functor if the following property (C) is satisfied:
(C) For every commutative diagram 
$\require{AMScd}$
\begin{CD}
\mathbf{M}'_0 @<\chi'<< \mathbf{M}'_1\\
@V k_0 V V @VV k_1 V\\
\mathbf{M}_0 @<<\chi< \mathbf{M}_1
\end{CD}
in $\textbf{M}$ whose image under $P$ is a pullback square of $\textbf{A}$, the following implication holds:
  if $\chi$ and $\chi'$ are cartesian and $k_0$ is cocartesian, then $k_1$ is cocartesian.
1.3. Characterization of descent data. -- In the sequel, $P\colon\textbf{M}\rightarrow\textbf{A}$ is a Chevalley functor.
Let $a\colon A_1\rightarrow A_0$ be a morphism of $\textbf{A}$; let us write $A_2$ for the fibered product $A_1\times_{A_0}A_1$ and $a_1$ and $a_2$ for the canonical 'projections' of $A_2$ to $A_1$.
  The property (C) permits to define, for each object $M_1$ de $\textbf{M}(A_1)$ a canonical bijection, 'natural' in $M_1$, of $\mathrm{Hom}_{\textbf{M}(A_2)}(a_1^\ast(M_1),a_2^\ast(M_1))$ onto $\mathrm{Hom}_{\textbf{M}(A_1)}(\textbf{T}^a(M_1),M_1)$, which we denote by $\varphi\mapsto K^a(\varphi)$.
Lemma. -- A morphism $\varphi\colon a_1^\ast(M_1)\rightarrow a_2^\ast(M_1)$ such that $\textbf{P}(\varphi)=1_{A_2}$
  is a descent datum if and only if $K^a(\varphi)$ is an algebra for the monad $\textbf{T}^a$.
Let us write $\textbf{D}(a)$ for the category of descent data relative to $a$, and
$\Psi^a\colon\textbf{M}(A_0)\rightarrow\textbf{D}(a)$ ${}\qquad$   and ${}\qquad$ $U^a\colon\textbf{D}(a)\rightarrow\textbf{M}(A_1)$
for the canonical functors.
Theorem. -- The correspondence $\varphi\mapsto K^a(\varphi)$ induces an equivalence of categories $K^a\colon\textbf{D}(a)\rightarrow \textbf{M}^a$ such that the following diagram commutes:

Proposition 1. -- The correspondence $\varphi\mapsto K^a(\varphi)$ is universal.
More precisely, let $b_0\colon A_0'\rightarrow A_0$ be a morphism of $\textbf{A}$.
Base change gives rise to the diagram

in $\textbf{A}$.
If $M_1$ is an object of $\textbf{M}(A_1)$ and $\varphi\colon a_1^\ast(M_1)\rightarrow a_2^\ast(M_1)$ is a morphism of $\textbf{M}(A_2)$, then
$K^{a'}(b_2^\ast(\varphi)) = b_1^\ast(K^a(\varphi))$.
If one in particular takes $A_0'=A_1$ and $b_0=a$, then the following implication holds: if $\varphi$ is a descent datum, then $b_2^\ast(\varphi)$ is an effective descent datum.
  The converse is true, since from the theorem and the proposition it follows that:
Corollary. -- A morphism $\varphi\colon a_1^\ast(M_1)\rightarrow a_2^\ast(M_1)\in\textbf{M}(A_2)$ is a descent datum if and only if its inverse image $b_2^\ast(\varphi)$ via the canonical base change $b_0=a\colon A_0'=A_1\rightarrow A$ is an effective descent datum.
This corollary allows to in the sequel avoid the use of the 'cocycle condition'
2. First applications. -- In view of the preceding theorem, a criterion of Beck (${}^2$) allows to give necessary and sufficient conditions for the functor $\Psi^a$ to be [severally] faithful, fully faithful, or an equivalence of categories, in terms of conditions which say that the inverse image functor $a^\ast$ reflects, or commutes with, certain cokernels.
  Let us give some applications.
Proposition 2. -- If the category $\textbf{M}(A_0)$ has all cokernel pairs, then the functor $\Psi^a$ has a left adjoint.
Proposition 3. -- The functor $\Psi^a$ is faithful if and only if $a^\ast$ is.
Proposition 4. -- If $a^\ast$ reflects cokernels, then $\Psi^a$ is fully faithful.
In particular, if all the fibers of $\textbf{M}$ are abelian, then
$\text{
$\Psi^a$ faithful $\Leftrightarrow$ $\Psi^a$ fully faithful $\Leftrightarrow$ $a^\ast$ faithful
  }$
Definition. -- We say that a morphism $a\colon A_1\rightarrow A_0$ is faithfully flat if the functor $a^\ast$ commutes with cokernels and reflects isomorphisms.
Proposition 5. -- If $a\colon A_1\rightarrow A_0$ is faithfully flat, and if $\textbf{M}(A_0)$ has all cokernels, then $\Psi^a$ is an equivalence of categories.
3. First examples of Chevalley functors.
3.1. If one takes for $\textbf{A}$ the dual of the category of commutative rings, and for $\textbf{M}$ the dual of the category of modules over [arbitrary] commutative rings, the evident functor $P\colon\textbf{M}\rightarrow\textbf{A}$ is a Chevalley functor.
3.2 If $\textbf{A}$ is a category with all binary pullbacks, and if $\textbf{M} = \mathrm{Fl}(\textbf{A})$ denotes the arrow category of $\textbf{A}$, the 'codomain' functor $\textbf{M}\rightarrow\textbf{A}$ is a Chevalley functor.
3.3. If $\textbf{P}\colon\textbf{M}\rightarrow\textbf{A}$ and $\textbf{Q}\colon\textbf{N}\rightarrow\textbf{M}$ are Chevalley functors, their composite $P\circ Q$ is.
3.4. If $\textbf{P}\colon\textbf{M}\rightarrow\textbf{A}$ is a Chevalley functor, and if $\textbf{II}$ [I think this is simply a misprint in the C.R.Acad.Sc. paper, and should rather be $\textbf{I}$] is any category, then the functor $P^{\textbf{I}}\colon \textbf{M}^{\textbf{I}}\rightarrow\textbf{A}^{\textbf{I}}$ is a Chevalley functor.
3.5. If in a pullback square 
\begin{CD}
\mathbf{M} @<\chi'<< f^*(\mathbf{M})\\
@V P V V @VV f^*(P) V\\
\mathbf{A} @<<f< \mathbf{X}
\end{CD}
the category $\textbf{X}$ has all finite pullbacks, then the functor $f$ commutes with pullbacks, and the functor $P$ is a Chevalley functor, hence $f^\ast(P)$ is a Chevalley functor.
In a later publication, we will give further examples of Chevalley categories,
  and also more precise criteria which allow to recognize whether $\Psi^a$ is faithful, fully faithful,
  or an equivalence of categories in situations where the fibers of $\textbf{M}$ are algebraic categories
  (categories of modules, for example).
(${}^\ast$) Session of January 5, 1970.
(${}^1$) A. Grothendieck, Catégories fibrées et descente. (Séminaire Bourbaki, 1959).
(${}^2$) Linton, Applied Functorial semantics. II, Springer lecture Notes no 80, 1969. 
(${}^3$) Chevalley, Séminaire sur la descente 1964--1965 (unpublished).
[postal adresses at end of the article omitted]

End of reasonably literal translation.
Addition 11 November 2017. The following is the review of op. cit. in Zbl 0287.18007:


 While I do think that I got it mostly right, and chose the modern technical terms conscientiously, I do not take any responsibility for this translation, neither for its form nor its content, and there might be a few places where it might be possible to improve the translation. 
    Do not take it to be a 'sworn translation', or anything like that. 
    If in doubt, consult the original article.
(0) I do not have anything against someone developing this answer further, if it is an on-topic improvement.
(1) I am mentioning (0) since:
(1.0) Translating is an art and a craft of its own, with its own professional associations customs, and translating well takes considerable work and knowledge of both the source- and target-language and the subject matter, and many translators would not like to see their work changed by others, so (0) does not go without saying. 
(1.1) It will not be possible for me to henceforth be responsible for this translation, let alone even check this thread at regular intervals.
Please consider my translation to be in the public domain, and please do not 'ping' me too much about it. 
 Please go ahead if you think you are sure that a relevant improvement should be made.
(2) In contrast to (0), I am not sure whether the authors of the translated article have something against expanding the translation here. 
The reason for that is that I think that then the result of the process will not be literal translation anymore. 
The boundaries between 'literal translation of' and 'some-sort-of-group-blog-exposition of' a given mathematical classic will blur. 
Maybe one should keep these two genres separate, I am not sure.
(3) Why I did I write this: simply because this question was asked and I think this is an answer to the OP.  Moreover, I myself have to work with similar things recently, and I had planned to understand descent-theory a little better anyway.
And now there appeared this request which harmonized with that. Incidentally, the comment to the effect that the author of the blog-post has been emailed the OP, which may lead to the OP getting another translation soon, was read by me only after my translation was almost finished.
Moreover, I can find little wrong with there being several translations of classics; there are several translations of, say, the classics of Latin poetry, too, so why should there not be multiple translations of French classics of category theory? 
A: Here is the copy of The Bénabou-Roubaud monadic descent theorem via string diagrams paper:
https://www.dropbox.com/s/236deicmr3636d5/draft.pdf?dl=0
Disclaimer: the papers was, and still is, just a draft. I hope to find some time soon to sort it out and make it available on ArXiv.
A: There is an excellent translation of the French article presenting the 
Benabou–Roubaud Theorem to English by Zoran Škoda which he certainly will provide on request.
On p.101 of Fibered Categories (à la Jean Bénabou) you find the original definition of descent maps in terms of fibrations
due to Grothendieck and Giraud.
The relation between this original formulation and the now common one
can be found in Prop.4.5 of Vistoli's excellent Notes on Grothendieck topologies, fibered categories and descent theory (arXiv:math/0412512).
