Intuitionistic type theory offers a new way of analyzing logic, mainly through its introduction of explicit proof objects. This provides a direct computational interpretation of logic, since there are computation rules for proof objects. As regards expressive power, intuitionistic type theory may be considered as an extension of first-order logic, much as higher order logic, but predicative.