Fix related systems

appendix/bibliography/bibliography.bib

@@ -189,25 +189,6 @@ @misc{FormVerPlugin
   url = {https://github.com/jesyspa/kotlin/tree/formal-verification/plugins/formal-verification},
 }
 
-@article{Rust,
-author = {Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek},
-title = {RustBelt: securing the foundations of the Rust programming language},
-year = {2017},
-issue_date = {January 2018},
-publisher = {Association for Computing Machinery},
-address = {New York, NY, USA},
-volume = {2},
-number = {POPL},
-url = {https://doi.org/10.1145/3158154},
-doi = {10.1145/3158154},
-abstract = {Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.},
-journal = {Proc. ACM Program. Lang.},
-month = {dec},
-articleno = {66},
-numpages = {34},
-keywords = {Rust, concurrency, logical relations, separation logic, type systems}
-}
-
 @book{Aliasing-OOP,
 editor = {Clarke, Dave and Noble, James and Wrigstad, Tobias},
 title = {Aliasing in Object-Oriented Programming: types, analysis, and verification},

chapters/3-Related-Work.typ

@@ -31,12 +31,20 @@ Aliasing prevention alone is not sufficient because aliasing is unavoidable in c
 
 == Systems for controlling Aliasing 
 
-In recent decades, extensive research has been conducted to address the issue of aliasing. The book "Aliasing in Object-Oriented Programming" @Aliasing-OOP provides a comprehensive survey of the latest techniques for managing aliasing in object-oriented programming.
+In recent decades, extensive research has been conducted to address the issue of aliasing. The book _Aliasing in Object-Oriented Programming_ @Aliasing-OOP provides a comprehensive survey of the latest techniques for managing aliasing in object-oriented programming.
 
 === Controlling aliasing with uniqueness
 
-A uniqueness type system distinguishes values referenced no more than once from values that can be referenced multiple times in a program. Harrington's "uniqueness logic" @uniqueness-logic provides a formalization of concept of uniqueness.
-The common trait of all systems based on uniqueness is that a reference declared as unique points to an object that is not accessible by any other unknown reference. Moreover, the unique status of a reference can be dropped at any point of the program.
+// TODO: decidere se usare virgolette o corsivo per linear logi, uniqueness locic ecc.
+
+A uniqueness type system distinguishes values referenced no more than once from values that can be referenced multiple times in a program. Harrington's _Uniqueness Logic_ @uniqueness-logic provides a formalization of the concept of uniqueness.
+
+Uniqueness logic might seem similar to the more well-known _Linear Logic_.
+_Linearity and Uniqueness: An Entente Cordiale_ @An-Entente-Cordiale describes the differences between linearity and uniqueness and shows how they can coexist.
+
+#v(1em)
+
+The common trait of all systems based on uniqueness is that a reference declared as unique points to an object that is not accessible by any other unknown reference. Moreover, the unique status of a reference can be dropped at any point in the program.
 
 #v(1em)
 
@@ -68,19 +76,15 @@ The system requires few annotations to be provided by the user:
 Furthermore, the system provides flexibility for uniqueness by permitting local variable aliasing, as long as this aliasing can be precisely determined.
 A uniqueness invariant is defined as follows: "a unique object is stored at most once on the heap. In addition, all usable references to a unique object from the local environment are precisely inferred".
 
-Latte's analysis produces at each program point an *alias graph*, that is an undirected graph whose nodes are syntactic paths and distinct paths $p_1$ and $p_2$ are connected iff $p_1$ and $p_2$ are aliased. Moreover a directed graph whose nodes are syntactic path called *reference graph* is also produced for every program point. Intuitively, having an edge from $p_1$ to $p_2$ in the reference graph means that the annotation of $p_1$ requires to be updated when $p_2$ is updated.
-
-=== Controlling aliasing with linear types
-
-// TODO: write it based on the content of the paper
+Latte's analysis produces at each program point an "alias graph", that is an undirected graph whose nodes are syntactic paths and distinct paths $p_1$ and $p_2$ are connected iff $p_1$ and $p_2$ are aliased. Moreover a directed graph whose nodes are syntactic path called "reference graph" is also produced for every program point. Intuitively, having an edge from $p_1$ to $p_2$ in the reference graph means that the annotation of $p_1$ requires to be updated when $p_2$ is updated.
 
-*Rust* @Rust and its "Shared XOR Mutable" principle. 
+=== Programming languages that control aliasing
 
-@An-Entente-Cordiale describes the difference between linearity and uniqueness.
-// Rust @Rust is a programming language that prioritizes safety and performance, offering some unique tools for managing memory. One of its principles is the "Shared XOR Mutable" rule, which maintains that any given piece of data can either have any number of readers or exactly one writer at any given time. This principle is key in preventing data races, as it ensures safe concurrency. With this principle, Rust provides the advantages of thread safety without necessitating a garbage collector, delivering an optimal balance between performance and security.
+*TODO: decide whether to include this section or not*
 
-// TODO: decide whether to include or not swift
+- *Rust* and its "Shared XOR Mutable" principle.
 
+- *Swift*
 
 == Tools for verification with Viper