User loginNavigation 
Linear types for aliased resources
Linear types for aliased resources. Chris Hawblitzel.
Type systems that track aliasing can verify statedependent program properties. For example, such systems can verify that a program does not access a resource after deallocating the resource. The simplest way to track aliasing is to use linear types, which on the surface appear to ban the aliasing of linear resources entirely. Since banning aliasing is considered too draconian for many practical programs, researchers have proposed type systems that allow limited forms of aliasing, without losing total control over statedependent properties. This paper describes how to encode one such system, the capability calculus, using a type system based on plain linear types with no special support for aliasing. Given welltyped capability calculus source programs, the encodings produce welltyped target programs based on linear types. These encodings demonstrate that, contrary to common expectations, linear type systems can express aliasing of linear resources. The prose is slightly confusing, but the code examples help. Sections 1 & 2 should be enough for those who only want to understand the problem with aliasing, and get a glimpse of what linear types are. 
Browse archives
Active forum topics

Recent comments
2 weeks 22 hours ago
2 weeks 5 days ago
2 weeks 6 days ago
2 weeks 6 days ago
3 weeks 5 days ago
4 weeks 1 day ago
4 weeks 1 day ago
4 weeks 1 day ago
5 weeks 3 days ago
5 weeks 4 days ago