Are there presentations of set theory in terms of lambda-calculus? I am planning to implement in software a set theory language, based on a binary function, which in set theory is the so called adjunction operation: $f(x, y) = x \cup$ {y}. Therefore, a presentation of set theory in terms of lambda-calculus will really help. Are there such presentations or attempts to do it?
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.