Sound and Complete Type Inference for a Systems Programming Language

This paper introduces a new type system designed for safe systems programming. The type system features a new mutability model that combines unboxed types with a consistent typing of mutability. The type system is provably sound, supports polymorphism, and eliminates the need for alias analysis to determine the immutability of a location. A sound and complete type inference algorithm for this system is presented.

• Type: Conference
• Year: 2008
• Where: APLAS
• Authors: Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith
• Keywords: APLAS 2008, Mutability, Programming Languages, Type Inference Algorithm, Type System