Since you explicitly asked for the most interesting and obscure ones:
You can extend C-H to many interesting logics and formulations of logics to obtain a really wide variety of correspondences. Here I’ve tried to focus on some of the more interesting ones rather than on the obscure, plus a couple of fundamental ones that haven’t come up yet.
evaluation | proof normalisation/cut-elimination
variable | assumption
S K combinators | axiomatic formulation of logic
pattern matching | left-sequent rules
subtyping | implicit entailment (not reflected in expressions)
intersection types | implicit conjunction
union types | implicit disjunction
open code | temporal next
closed code | necessity
effects | possibility
reachable state | possible world
monadic metalanguage | lax logic
non-termination | truth in an unobservable possible world
distributed programs | modal logic S5/Hybrid logic
meta variables | modal assumptions
explicit substitutions | contextual modal necessity
pi-calculus | linear logic
EDIT: A reference I’d recommend to anyone interested in learning more about extensions of C-H:
“A Judgmental Reconstruction of Modal Logic” http://www.cs.cmu.edu/~fp/papers/mscs00.pdf – this is a great place to start because it starts from first principles and much of it is aimed to be accessible to non-logicians/language theorists. (I’m the second author though, so I’m biased.)