What’s the internal language of the opposite of a Cartesian closed category?


I have heard the simply typed lambda calculus is the internal language of Cartesian closed categories.

What’s the internal language of the opposite type of category?

I have the intuition the opposite category would correspond to continuation passing style or pattern matching but the opposite typing rules seem very strange and hard to figure out.