Why is Kripke semantics so effective?

Stream: Type theory

[Trebor Huang]

I learned about the Kripke models for modal logics and intuitionistic logic. But to me, it seems unreasonably good at solving problems -- The strong normalization property for STLC seems easily proved. Why is this happening? Is there some deep intuitive explanation of the Kripke-like structure lying in type theory?

[Reid Barton]

You might be interested in this:
https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html

[Thorsten Altenkirch]

Actually what you use here are presheaf models, which are Kripke models on steroids. My old talk may shed some light:
http://www.cs.nott.ac.uk/~psztxa/talks/nbe09.pdf