An alternative formal logical system for predicative constructive mathematics is Myhill and Aczel’s  constructive Zermelo-Fraenkel set theory  (CZF). This theory, which is based on intuitionistic first-order predicate logic and weakens some of the axioms of classical Zermelo-Fraenkel Set Theory, has a natural interpretation in intuitionistic type theory. Martin-Löf’s meaning explanations thus also indirectly form a basis for CZF.