Comparison to PCC [Necula & Lee]
In principle, PCC is more expressive:
- better code for arrays
- desired security properties (e.g., memory safety) may be weaker than type safety
-
but for KML -> x86, we would need:
(1) a very sophisticated, higher-order logic
(2) a detailed encoding of properties implied by types (e.g., memory safety, GC invariants, etc.)
(3) some way to recover parametricity?