Are there presentations of set theory in terms of lambda-calculus?
There is a really interesting approach to a set theory-like foundational system that I am rather fond of: Grue's Map Theory. The basic idea is to take the (untyped!) $\lambda$-calculus as a base foundation, and to represent a set $S$ as a term $f$ such that

$$ S=\{f(x)\mid x\in\Phi\}$$
where $\Phi$ represents the well founded functions ($x\neq\bot$ in the Scott semantics). It doesn't look like there is any proof assistant based on it though, so I have no idea how it would work in practice.