A collection of papers that I've read or plan to read.

• Linear Logic

• Linear Types Can Change The World!

• Separation Logic: A Logic for Shared Mutable Data Structures (LCS '02): a survey paper on separation logic. Must read.

• Separation and Information Hiding (POPL '04)

• Separation Logic and Abstraction (POPL '05)

• Separation Logic, Abstraction and Inheritance (POPL '08

• Promises: Limited Specifications for Analysis and Manipulations (ICSE '98)

• Data groups: specifying the modification of extended state (OOPSLA '98)

• An Object-Oriented Effects System (ECOOP '99)

• Alias burying: Unique variables without destructive reads

• Modular Typestate Checking of Aliased Objects (OOPSLA '07): a modular typestate checking tool based on a concept called access permissions, which is high-level abstraction of Fractional Permissions and is used to capture different patterns of them.

• Capabilities for Uniqueness and Borrowing (ECOOP '10): Haller and Odersky designed and implemented a type system which uses capabilities to model uniqueness and borrowing. It offers "external uniqueness", which is a more strict uniqueness in which the only access path to all references inside an unique object is through the object itself. In other words, no "shared" references are allowed inside an unique object. Atomic operations are offered for transfering unique values and merging unique values.

• A Type System for Borrowing Permissions (POPL '12): This type system covers different types of permissions such as unique, none, immutable, local immutable, etc. A particular kind of permission called "local permission" is supported by this system, which is useful for permission splitting and combining. The system also supports "changing permissions", which is part of a method's contract, and is similar to the input and output permissions specified for a method type in Fractional Permissions.

• A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language (PLDI '07)

• A Verified Compiler for an Impure Functional Language (POPL '10)

• Soft Typing (PLDI 1991)

• Gradual Typing for Functional Languages (SFP '06)

• Gradual Typing for Objects (ECOOP '07): combining static and dynamic typing for OO languages. Type annotation is optional, and in case it is missing, a ? type is used. During type checking, type equality is replaced with type consistency, which can also be combined with subtyping. A gradual type system, (which is based on the object calculus from Abadi and Cardelli) and its semantics are given in the paper. The system is proven sound using machine-checked proofs.