Martin-Lof's type theory is the foundation (or inspiration) for quite a few modern proof assistants. It is also an elegant non-set based foundation for constructive mathematics.