Has somebody worked out a typed higher order logic? I mean something like type theory but not with this intuitionistic touch. Is there a natural deduction system for this logic?
Russell & Whiteheads theory is perhaps a bit on the heavy side, but here are some references to support Andreas Blass' comment:
An early formulations of classical higher-order logic was given by Alonzo Church in A formulation of the Simple Theory of Types, see also the Princeton Encyclopedia of Philosophy entry on Church's Type Theory.
Proof assistants from the HOL family typically use classical type theories similar to those of Church, see for instance HOL light, see this HOL Light overview for a quick description of the underlying type theory.
In general most kinds of intuitionistic type theory are agnostic about excluded middle and you can simply turn them into classical theories by postulating excluded middle.