Abstract
Whether verified dynamically (at runtime) or statically (by prior analysis), typing is an essential aspect of high-level programming languages. The lecture explored the contributions of typing to software security, from the basic guarantees (value and memory safety) essential for software isolation to finer-grained integrity guarantees based on type abstraction and the static typing of resources and their ownership(ownership and borrowing, as in the Rust language). We then show how static typing can be applied to mobile code, by verifying intermediate code (such as Java's JVM bytecode ) or machine code, right up to the very general notion ofproof-carrying code.
