Add Granule

appendix/bibliography/bibliography.bib

@@ -351,4 +351,23 @@ @inproceedings{HeuleKassiosMuellerSummers13
   pages={451-476},
   url         = {https://doi.org/10.1007/978-3-642-39038-8_19},
   urltext     = {[Publisher]}
+}
+
+@article{Granule,
+author = {Orchard, Dominic and Liepelt, Vilem-Benjamin and Eades III, Harley},
+title = {Quantitative program reasoning with graded modal types},
+year = {2019},
+issue_date = {August 2019},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {3},
+number = {ICFP},
+url = {https://doi.org/10.1145/3341714},
+doi = {10.1145/3341714},
+abstract = {In programming, some data acts as a resource (e.g., file handles, channels) subject to usage constraints. This poses a challenge to software correctness as most languages are agnostic to constraints on data. The approach of linear types provides a partial remedy, delineating data into resources to be used but never copied or discarded, and unconstrained values. Bounded Linear Logic provides a more fine-grained approach, quantifying non-linear use via an indexed-family of modalities. Recent work on coeffect types generalises this idea to graded comonads, providing type systems which can capture various program properties. Here, we propose the umbrella notion of graded modal types, encompassing coeffect types and dual notions of type-based effect reasoning via graded monads. In combination with linear and indexed types, we show that graded modal types provide an expressive type theory for quantitative program reasoning, advancing the reach of type systems to capture and verify a broader set of program properties. We demonstrate this approach via a type system embodied in a fully-fledged functional language called Granule, exploring various examples.},
+journal = {Proc. ACM Program. Lang.},
+month = {jul},
+articleno = {110},
+numpages = {30},
+keywords = {linear types, implementation, graded modal types, coeffects}
 }

appendix/full-rules-set.typ

@@ -156,5 +156,3 @@ All the following rules are to be considered for a given program $P$, where fiel
   If, "",
   Return-p, "",
 )
-
-// IMPROVE: derivation tree for the examples in chapter 5?

chapters/3-Related-Work.typ

@@ -72,6 +72,8 @@ 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.
 
+Finally, Granule @Granule is a language designed with a focus on fine-grained resource management. Its type system combines linear types, indexed types (lightweight dependent types), and graded modal types to enable advanced quantitative reasoning. This combination offers strong guarantees for memory management and aliasing, ensuring strict control over when and how resources can be accessed. Granule aims to demonstrate the reasoning power of combining linear, graded, and indexed types, particularly in the context of common language features such as data types, pattern matching, and recursion.
+
 == 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/6-Encoding.typ

@@ -120,7 +120,7 @@ For example, passing a unique reference to a function expecting a shared (non-bo
 
 #figure(
   caption: "Extra statements added for functions call encoding",
-  image("../images/calls-graph.svg", width: 60%)
+  image("../images/calls-graph.svg", width: 50%)
 )<call-graph>
 
 #v(1em)

structure.typ

@@ -11,6 +11,9 @@
 #counter(page).update(1)
 #set heading(numbering: "1.1", supplement: [Chapter])
 
+// TODO: decide whether to have this or not
+// #set par(first-line-indent: 1em)
+
 #include "./chapters/1-Introduction.typ"
 #include "./chapters/2-Background.typ"
 #include "./chapters/3-Related-Work.typ"