You could model C in a dependently-typed language by embedding the C abstract machine and C program expressions in it. Then you could use the Poincaré principle applied to C-program fragments to perform any "abstract interpretation" of them and derive any property you might care about. So it looks like the Poincaré's principle (as it was named by Barendegt) is the actual "missing link" that would enable you to generalize from purely syntax-based analysis (as in the traditional definition of type systems/type checks) to "interpretation" of a more general sort.