Conventions: So that I don't have to worry about, fix a field $k$ of characteristic zero, and always work over it. Categories of modules, etc., are always $\infty$-categories of dg modules. Algebras are "associative" in the coherent-homotopy sense. All tensor products are left-derived. Etc. I am of course always interested in hearing about subtleties and generalizations of such conventions, but for the sake of this question you may pretend that I understand this part of the story.

A construction: Let $A$ be an algebra and $V$ a left $A$-module. Write $V^\ast$ for the linear dual to $V$; then $V^\ast$ is a right $A$-module. Set $C = V^\ast \otimes_A V$. I claim that $C$ is a coalgebra, at least when $V$ satisfies some finiteness condition. Indeed, if $V$ satisfies a finiteness condition, then $\operatorname{End}_k(V) = V\otimes_k V^\ast$, and the action of $A$ on $V$ is encoded in a map $A \to \operatorname{End}_k(V)$, which by associativity is a map of $A$-$A$-bimodules. Then the comultiplication is:

$$ C = V^\ast \otimes_A V = V^\ast \otimes_A A \otimes_A V \to V^\ast \otimes_A (V \otimes_k V^\ast) \otimes_A V = C \otimes_k C $$

This is coassociative on account of the coassociativity of tensor products.

For $X$ any left $A$-module, there is a corresponding left $C$-comodule defined by $V^\ast \otimes_A X$; the comodule structure is

$$ V^\ast \otimes_A X = V^\ast \otimes_A A \otimes_A X \to V^\ast \otimes_A (V \otimes_k V^\ast) \otimes_A X = C \otimes_k (V^\ast \otimes_A X) $$

Aside: Let $C$ be any (coassociative) coalgebra, $Y$ a left $C$-comodule, and $Z$ a right $C$-comodule. Recall that the underived cotensor product is the 1-categorical equalizer of the two maps $Z \otimes Y \rightrightarrows Z \otimes C \otimes Y$. The (derived) cotensor product $Z \Box_C Y$ is the right-derived version thereof (cotensor is left-exact, if I haven't made an error); it should also be the $\infty$-categorical equalizer.

At least in the 1-categorical non-dg setting cotensor products of bi-comodules and so on are not always associative. But they are associative when all coalgebras are flat over whatever ground ring you're working over, and we're working over a field, so this is not an issue. I don't know what the correct statement is in the dg $\infty$-categorical level.

The construction, continued: In a similar way, $V$ is a right $C = V^\ast \otimes_A V$ comodule, and so for any left $C$-comodule $Y$, I can define a left $A$-module $V \Box_C Y$.

All together, I've constructed functors

$$V^\ast \otimes_A: A\text{-mod} \leftrightarrow C\text{-comod} :V \Box_C.$$

One composition of these functors (the one from $C$-comod to $C$-comod) is the identity:

$$ V^\ast \otimes_A V \Box_C = C \Box_C $$

The other composition cannot always be the identity — just imagine what would happen if I took $V$ to be the zero module!

Question: A statement that perhaps deserves to be called Koszul duality is that these two functors are an equivalence of $\infty$-categories. Of course, that seems almost nonsense to me, because in the non-dg-$\infty$ world categories of modules and categories of comodules seem quite different. So part of my question is to clarify the statement of the statement. But the bulk of my question is: What conditions do I need to add in the above exposition to have the statement I'd like? For example, I would like to identify $\operatorname{End}_k(V) = V \otimes_k V^\ast$, and so I would expect to need some "finiteness" condition on $V$, or I would expect to need some topology.

Note that what many people call "Koszul duality" consists also of taking the dual $C^\ast$ to the coalgebra $C$, so as to get an algebra. Every left comodule of $C$ is a left module of $C^\ast$, but there are generically more of the latter, at least in the 1-categorical version of the story. Given that many discussions of Koszul duality use the (derived) $\operatorname{End}_A(V,V)$, which is an algebra that should be essentially the same as $C^\ast$, I worry that maybe the algebra-to-algebra version is more robust. But I'm not sure.

Bonus question and further reading: Sometime soon I will be writing up a construction related to the one above, as part of a larger project. I picked up the above ideas from discussions with various people. But I would like to give credit where it's due, so I would like to hear about any particular papers I should be sure to cite.

For further reading, you might check out this question from the first month of MathOverflow, and also perhaps Jacob Lurie's ICM address.