Type lambda calculi are an abstract framework for studing the main properties of various kinds of (constructive) set theories.

Present works include studing the main metamathematical properties of the calculi (normalization, confluence, ...) and their expressive capability.