Abstract
Whether verified dynamically (at runtime) or statically (by prior analysis), typing is an essential aspect of high-level programming languages. In this lecture, we will study the contributions of typing to software security, from the basic guarantees (value and memory safety) essential for software isolation to finer-grained guarantees based on type abstraction. We'll also talk about types for resource management (uniqueness types, linear types, possession and borrowing) and their possible uses for security.
