 for all formulae C of that theory. Principles similar to the three above are also often validated in another type of computational interpretation of intuitionistic theories known as realizability. Thus it appears that they are intrinsically related to computational interpretations of such theories.