  The logic of constant domains is intuitionistic logic extended with the
so-called forall-shift axiom, a classically valid statement which implies the
excluded middle over decidable formulas. Surprisingly, this logic is
constructive and so far this has been proved by cut-elimination for ad-hoc
sequent calculi. Here we use the methods of natural deduction and Curry-Howard
correspondence to provide a simple computational interpretation of the logic.
