We present System F°, an extension of System F that uses kinds to distinguish between
linear and unrestricted types, simplifying the use of linearity for general-purpose …

Making software reliable is one of the most important technological challenges facing our
society today. This thesis presents a new type system that addresses this problem by …

This paper presents the first practical static analysis tool that can find memory leaks and
double deletions of objects held in polymorphic containers. This is especially important …

Linear typing schemes guarantee single-threadedness and so the soundness of in-place
update with respect to a functional semantics. But linear schemes are restrictive in practice …

Security-typed languages enforce secrecy or integrity policies by type-checking. This paper
investigates continuation-passing style (CPS) as a means of proving that such languages …

Software plays a pivotal role in our daily lives, yet software glitches and security
vulnerabilities continue to plague us. Existing techniques for ensuring the quality of software …

Traditional approaches to enforcing memory safety of programs rely heavily on run-time
checks of memory accesses and on garbage collection, both of which are unattractive for …

Proof-carrying code (PCC) is a general framework for verifying the safety properties of
machine-language programs. PCC proofs are usually written in a logic extended with …

Type systems usually characterize the shape of values but not their free variables. However,
there are many desirable safety properties one could guarantee if one could track how …

We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a
novel static discipline of duplicable and affine permissions, which controls aliasing and …