- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Formalizing Rust traits
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Formalizing Rust traits Milewski, Jonatan
Abstract
Rust is a new systems programming language designed with a focus on bare metal performance, safe concurrency and memory safety. It features a robust abstraction mechanism in the form of traits, which provide static overloading and dynamic dispatch. In this thesis, we present MiniRust—a formal model of a subset of Rust. The model focuses on the trait system and includes some advanced features of traits such as associated types and trait objects. In particular, we discuss the notion of object safety—the suitability of a particular trait for creating trait objects—and we formally determine very general conditions under which it can be guaranteed. To represent the runtime semantics of MiniRust programs, we develop an explicitly-typed internal language RustIn, for which we prove type safety, and we show that well-typed MiniRust programs can be translated to well-typed RustIn programs. Finally, we adapt the informally-described Rust trait coherence rules to our model and we show that they are sufficient to ensure that overloads are always well-determined, even in the presence of library extensions.
Item Metadata
Title |
Formalizing Rust traits
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
2015
|
Description |
Rust is a new systems programming language designed with a focus on bare metal performance, safe concurrency and memory safety. It features a robust abstraction mechanism in the form of traits, which provide static overloading and dynamic dispatch. In this thesis, we present MiniRust—a formal model of a subset of Rust. The model focuses on the trait system and includes some advanced features of traits such as associated types and trait objects. In particular, we discuss the notion of object safety—the suitability of a particular trait for creating trait objects—and we formally determine very general conditions under which it can be guaranteed. To represent the runtime semantics of MiniRust programs, we develop an explicitly-typed internal language RustIn, for which we prove type safety, and we show that well-typed MiniRust programs can be translated to well-typed RustIn programs. Finally, we adapt the informally-described Rust trait coherence rules to our model and we show that
they are sufficient to ensure that overloads are always well-determined, even in the presence of library extensions.
|
Genre | |
Type | |
Language |
eng
|
Date Available |
2015-12-01
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
Attribution-NonCommercial-NoDerivs 2.5 Canada
|
DOI |
10.14288/1.0220521
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
2016-02
|
Campus | |
Scholarly Level |
Graduate
|
Rights URI | |
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivs 2.5 Canada