Fix todo

chapters/1-Introduction.typ

@@ -11,8 +11,6 @@ Indeed, when $x$ and $y$ are aliased, the formula is not valid, and most of the
 On the other hand, ensuring disjointness of the heap enables the verification of such formulas. For instance, in separation logic @separationLogic1 @separationLogic2 @separationLogic3, it is possible to prove the correctness of the following formula. $ {(x |-> "true") * (y |-> -)} space y := "false" {(x |-> "true") * (y |-> "false")} $ 
 This verification is possible because separation logic allows to express that $x$ and $y$ are not aliased by using the separating conjunction operator "$*$". Similarly, programming languages can incorporate annotation systems @aldrich2002alias @boyland2001alias @zimmerman2023latte or built-in constructs @swift-parameter-modifiers @rustlang to provide similar guarantees regarding aliasing, thereby simplifying any verification process.
 
-// TODO: aggiungere altre citazioni a @rustlang se dovessi aggiungere altro per swift, rust, ocaml
-
 == Contributions
 
 This work demonstrates how controlling aliasing through an annotation system can enhance the formal verification process performed by SnaKt @FormVerPlugin, an existing plugin for the Kotlin language @KotlinSpec @Kotlin. SnaKt verifies Kotlin using Viper @ViperWebSite @Viper, an intermediate verification language developed by ETH Zurich. Viper is designed to verify programs by enabling the specification of functions with preconditions and postconditions, which are then checked for correctness. This verification is performed using one of two back-ends: symbolic execution @MuellerSchwerhoffSummers16b or verification condition generation @HeuleKassiosMuellerSummers13, both of which rely on an SMT solver to validate the specified conditions.

chapters/3-Related-Work.typ

@@ -41,15 +41,13 @@ In recent decades, extensive research has been conducted to address the issue of
 
 === Controlling Aliasing through Uniqueness<cap:control-alias-unique>
 
-// TODO: decide whether to use quote-unquote or italic for linear logic, uniqueness logic 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.
 While it may initially appear similar to the more widely known _Linear Logic_ @linear-logic, Marshall et al. @An-Entente-Cordiale clarify the differences between these two approaches and demonstrate how they can coexist.
 
 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 reference, unless such references are explicitly tracked by the system. Moreover, the unique status of a reference can be dropped at any point in the program.
 
-A first approach to ensuring uniqueness consists of using destructive reads. Aldrich et al. @aldrich2002alias have developed a system called _AliasJava_ for controlling aliasing which uses this approach.
-_AliasJava_ is characterized by a strong uniqueness invariant asserting that "at a particular point in dynamic program execution, if a variable or field that refers to an object `o` is annotated unique, then no other field in the program refers to `o`, and all other local variables that refer to `o` are annotated lent".
+A first approach to ensuring uniqueness consists of using destructive reads. Aldrich et al. @aldrich2002alias have developed a system called AliasJava for controlling aliasing which uses this approach.
+AliasJava is characterized by a strong uniqueness invariant asserting that "at a particular point in dynamic program execution, if a variable or field that refers to an object `o` is annotated unique, then no other field in the program refers to `o`, and all other local variables that refer to `o` are annotated lent".
 This invariant is maintained by the fact that unique references can only be read in a destructive manner, meaning that immediately being read, the value `null` is assigned to the reference.
 
 Boyland @boyland2001alias proposes a system for controlling aliasing in Java that does not require to use destructive reads.
@@ -74,10 +72,6 @@ A key feature of Rust is its ownership-based type system @rustlang, which guaran
 Swift is another language that has introduced constructs to manage aliasing effectively @swift-parameter-modifiers @swift-ownership-manifesto. By default, function arguments in Swift are passed by value, which means any modifications made within the function do not affect the original argument in the caller. However, parameters marked as `inout` behave differently. When a function is called with an `inout` parameter, the argument's value is copied. The function then works with this copy, and when it returns, the modified copy is assigned back to the original argument. Swift guarantees memory exclusivity, meaning that accessing an `inout` value from two different references simultaneously is prohibited, thereby preventing aliasing issues.
 In addition to `inout`, Swift provides two other parameter modifiers to manage ownership more precisely. The `borrowing` modifier indicates that the function temporarily accesses the parameter's value without taking ownership, leaving the caller responsible for the object's lifetime. This approach minimizes overhead when the function uses the object only transiently. Conversely, the `consuming` modifier indicates that the function takes full ownership of the value, including the responsibility for either storing or destroying it before the function returns.
 
-// - *TODO: Ocaml???*
-//   - https://blog.janestreet.com/oxidizing-ocaml-locality/
-//   - https://blog.janestreet.com/oxidizing-ocaml-ownership/
-
 == Viper Verification Tools
 
 Several verifiers have been built on top of Viper. The most relevant tools for this work are: Prusti, a verifier for the Rust programming language, Gobra, used to verify code written in Go, and Nagini, which can be used to verify Python programs.

chapters/4-Annotations-Kotlin.typ

@@ -194,8 +194,6 @@ fun manipulateList(xs: List<Int>): List<Int> {
   ```
 )<manipulate-list>
 
-// TODO: static garbage collection?
-
 == Stack Example<cap:kt-stack>
 
 To conclude the overview of the uniqueness system, a more complex example is provided in @kt-stack. The example shows the implementation of an alias-free stack, a common illustration in the literature for showcasing uniqueness systems in action @aldrich2002alias @zimmerman2023latte. 

chapters/5-Annotation-System.typ

@@ -7,9 +7,6 @@
 
 #pagebreak(to:"odd")
 
-// TODO: decide whether to put call, if ecc. in italic
-// TODO: decide whether to put rule names in italic
-
 = Annotation System<cap:annotation-system>
 
 This chapter formalizes the uniqueness system that was introduced in @cap:annotations-kt.
@@ -386,8 +383,8 @@ $ \_ triangle.filled.small.l \_ : Delta -> Delta -> Delta $
   Unify, ""
 )
 
-Finally, the unify function groups the two functions described before. This function will be fundamental to type if-statements.
-In particular, $unify(Delta, Delta_1, Delta_2)$ can be used to type an if-statement: when $Delta$ is the context at the beginning of the statement while $Delta_1$ and $Delta_2$ are the resulting contexts of the two branches of the statement.
+Finally, the unify function groups the two functions described before. This function will be fundamental to type `if` statements.
+In particular, $unify(Delta, Delta_1, Delta_2)$ can be used to type an `if` statement: when $Delta$ is the context at the beginning of the statement while $Delta_1$ and $Delta_2$ are the resulting contexts of the two branches of the statement.
 
 $ "unify" : Delta -> Delta -> Delta -> Delta $
 
@@ -722,12 +719,12 @@ Ensuring inaccessibility after reading borrowed fields and restricting their rea
 
 #display-rules(If, "")
 
-Once the unification function is defined, typing an _if_ statement is straightforward. First it is necessary to be sure that paths appearing in the guard are accessible in the initial context. The _then_ and the _else_ branches are typed separately and their resulting contexts are unified to get the resulting context of the whole statement.
+Once the unification function is defined, typing an `if` statement is straightforward. First it is necessary to be sure that paths appearing in the guard are accessible in the initial context. The `then` and the `else` branches are typed separately and their resulting contexts are unified to get the resulting context of the whole statement.
 
-The system does not allow to have _null_ or a _method call_ in the guard of an _if_ statement, as these constructs can be easily desugared.
+The system does not allow to have `null` or a method call in the guard of an `if` statement, as these constructs can be easily desugared.
 
 #example[
-  Desugaring for _if_ statements containing expressions different from paths within the guard.
+  Desugaring for `if` statements containing expressions different from paths within the guard.
   $ fi (p == null) ... equiv var "fresh" ; "fresh" = null ; fi(p == "fresh") ... $
   $ fi (p == m(...)) ... equiv var "fresh" ; "fresh" = m(...) ; fi(p == "fresh") ... $
 ]
@@ -762,7 +759,7 @@ fun f(@Unique a: A, @Borrowed c: C) {
 
 #display-rules(Return-p, "")
 
-By the construction of the grammar, a return statement is designed to be the final statement executed within a method. As such, there is no need to maintain a resulting context after the return statement has been typed. However, several important conditions must be satisfied when returning.
+By the construction of the grammar, a `return` statement is designed to be the final statement executed within a method. As such, there is no need to maintain a resulting context after the return statement has been typed. However, several important conditions must be satisfied when returning.
 
 First, the annotation of the path being returned must be lower than or equal to ($rel$) the annotation of the return value of the method. This ensures that a method cannot return a value with greater aliasing than what was specified in the method’s signature, effectively preventing borrowed values from being returned (@ret-bor).
 
@@ -772,7 +769,7 @@ Finally, all parameters that are shared or borrowed (or both) must remain in the
 
 These conditions are essential for maintaining the modularity, allowing each method to be typed without knowing the implementation of the other methods.
 
-The system does not allow returning a null value or a method call, since these cases can be easily desugared, as shown in @ret-desugar. Similarly, functions that do not return a value can be represented by having them return a call to the `Unit` constructor.
+The system does not allow returning `null` or a method call, since these cases can be easily desugared, as shown in @ret-desugar. Similarly, functions that do not return a value can be represented by having them return a call to the `Unit` constructor.
 
 #example[
   Given the following program:

structure.typ

@@ -28,5 +28,4 @@
 #set heading(numbering: "A.1", supplement: "Appendix")
 #counter(heading).update(0)
 
-#include("./appendix/full-rules-set.typ")
-// #include("./appendix/stack-proof.typ")
+#include("./appendix/full-rules-set.typ")