(1, 2, 3) Though Linton's *An outline of functorial semantics* does contain the essence of the results and proofs of the monad–theory correspondence (see in particular Theorems 8.1 and 9.1 – 9.3), it is true that the terminology and style make it difficult to extract the results as we would expect to see them today. I think it is appropriate to cite this paper as the original reference, though citing the following papers for modern statements would be complementary.

I shall give a brief outline of Linton's development as pertains to the monad–theory correspondence. (I shall use Linton's notation for ease of comparison.) The key lies in the construction of a general *semantics–structure adjunction* (Theorem 3.1): given a functor $j : A_0 \to A$, there is an adjunction $m^{(j)} : (A_0°/\mathrm{Cat})° \rightleftarrows \mathrm{Cat}/A : s^{(j)}$. One may then identify the fixed points of this adjunction: on the left-hand side, we have what Linton calls *clones over $A_0$*. This induces an adjunction by restricting to the clones over $A_0$, called the *operational semantics–operational structure adjunction* (Theorem 4.1).

Recall that the codensity monad of a right adjoint functor is precisely the monad induced by the adjunction. In Theorem 8.1, Linton proves that the Kleisli category of the codensity monad of the forgetful functor from a category of models for a clone coincides with the codomain of the clone, thus establishing that clones over $A_0$ correspond to a class of condensity monads (the class itself is given explicitly, without reference to preservation of colimits as we would expect now). That this relationship commutes with taking categories of models and algebras is proven in Theorem 9.3 (making use of Theorems 9.1 and 9.2).

Note that Linton does not present the relationship between clones and monads as an equivalence of categories: in particular, he does not appear to consider morphisms of clones or monads (though this extra step presents no difficulties). It is my understanding that this final step is due to Dubuc (below).

In the classical setting of algebraic theories, we are concerned with $j : \mathbb F \to \mathrm{Set}$, where $\mathbb F$ is the free cocartesian category on a single object. The clones over $A_0$ are then precisely finitary single-sorted algebraic theories in the modern sense, and the operational semantics–operational structure adjunction sends an algebraic theory to (the forgetful functor from) its category of models in $\mathrm{Set}$.

In the setting of large algebraic theories, we instead take $j : \mathrm{Set} \to \mathrm{Set}$. The clones over $\mathrm{Set}$ are large single-sorted algebraic theories.

(2, 3) As far as I can tell, the earliest reference in which the monad–theory correspondence appears in the modern form is Theorem III of Dubuc's [Enriched semantics–structure (meta) adjointness](http://www.inmabb.criba.edu.ar/revuma/pdf/v25n1y2/p005-026.pdf). Dubuc establishes an equivalence between (large) $\mathcal V$-theories and $\mathcal V$-monads on $\mathcal V$, which in particular implies the classical result. The correspondence with *all* monads, rather than just finitary or $\kappa$-ary, seems to have fallen out of favour, and many modern treatments elide this case.

(1, 3) For the finitary version, the result (again in the enriched setting) appears as Theorems 4.3, 3.4, and 4.2 of Power's [Enriched Lawvere theories](http://www.tac.mta.ca/tac/volumes/6/n7/6-07abs.html). I haven't found an earlier reference with proofs.

(1, 2, 3) As far as I am aware, the only paper in which both results follow directly is Lucyshyn-Wright's [Enriched algebraic theories and monads for a system of arities](https://arxiv.org/abs/1511.02920): in particular both the finitary and the large monad–theory correspondences follow from Theorems 11.8 and 11.14. Again, this all takes place in the $\mathcal V$-enriched setting.