List of Papers

Patina: A Formalization of the Rust Programming Language

The core idea of the thesis comes from this paper. In consists of parts:

Pages 4-18 deals with heaps, variables and various judgments and theorems about them - mostly about reading them using paths/routes.
Pages 18-28 deals with lifetimes, loans, expressions and their evaluations.
Pages 29-33 deals with updates, statements and their evaluations.

A Linearly Typed Assembly Language

I have only skimmed the paper, but plan to read it more throughly. Two quotes of interest:

6 Implementation

We have implemented a typechecker and interpreter for LTAL and a certifying compiler from our source language to LTAL based on the translations described in Section 3. The implementation is written in OCaml 3.06 and consists of about 6000 lines of code. Our implementation includes recursive functions, lists, and a partial implementation of polymorphism as outlined in Sections 5. This is a toy implementation, intended as a proof of concept and to shake the bugs out of the type system, not to run real programs. Nevertheless, in the rest of this section, we describe experiments that suggest that LTAL programs are just as inefficient as we feared. We realize that this does not prove anything: anyone can write a bad compiler. However, we believe that these results shed enough light on the relevant issues to be worth presenting.

...

8 Summary and Conclusions

Linear TAL is a safe, low-level language that “stands on its own”: it does not require any outside run-time support from a garbage collector or operating system to guarantee safe execution within a fixed memory space. Moreover, LTAL is relatively simple, yet expressive enough to compile the functional core of ML. As far as we know, no other certified code technique combines these levels of transparency, independence and expressiveness.

But this independence comes at a steep price. LTAL’s linearity discipline prohibits any useful kind of sharing. This has disastrous consequences for naive compilation from high-level, non-linear functional languages, where the ability to copy is taken for granted. Furthermore, LTAL cannot ac- commodate language features like references or laziness that rely on sharing. We intend to generalize LTAL to support both sharing and safe low-level memory management in future work.