final 3

main.tex

@@ -7,7 +7,7 @@
 \usepackage[T1]{fontenc}
 % T1 fonts will be used to generate the final print and online PDFs,
 % so please use T1 fonts in your manuscript whenever possible.
-% Other font encondings may result in incorrect characters.
+% Other font encodings may result in incorrect characters.
 %
 \usepackage{graphicx}
 % Used for displaying a sample figure. If possible, figure files should
@@ -60,36 +60,36 @@
 \section{Introduction}
 In their work Bagrel and Spiwack \cite{bagrel_dp_2025} build on many prior contributions,
 both directly in their calculus grammar and semantics, but also in their structural approach regarding typing and evaluation contexts.
-From now on the calculus introduced in this specific paper will be referred to as \lad.
+From now on, the calculus introduced in this specific paper will be referred to as \lad.
-This report will highlight a number of select works, which are of significance to the $lambda_d$ calculus.
+This report will highlight a number of select works, which are of significance to the \lad calculus.
 
 \section{A Functional Representation of Data Structures with a Hole - Y. Minamide\cite{minamide_holes_1998}}
 This paper contributes fundamental work on holes in functional languages. 
 It introduces a hole abstraction $\hat\lambda x. T$ to formalize data structures with a single hole. 
-Which, while syntactically different, in principle remains similar to the \lad calculus.
+This, while syntactically different, in principle remains similar to the \lad calculus.
 Both utilize holes as the core features, where \lad has a type $T_1 \ltimes T_2$ to represent a
 structure that is missing $T_1$ to complete a $T_2$, Minamide's calculus features $(T_1, T_2) hfun$.
 In general Minamide focuses more on the similarity of his hole abstraction to the regular $\lambda$ abstraction
-and the similarity of a structure containing a hole, to a function that returns an type $T_2$, when applied argument to an argument $T_1$.
+and the similarity of a structure containing a hole, to a function that returns a type $T_2$, when applied to an argument of type $T_1$.
-Notably both calculi contain linearity constraints on holes, but Bagrel's work elevates some of those constraints by allowing for weakening.
+Notably both calculi contain linearity constraints on holes, but Bagrel's work relaxes some of those constraints by allowing for weakening.
 Overall Minamide lays a lot of groundwork, and influences that can be seen in the \lad formulation and in its discussion, as
 similar benefits regarding tail recursion are addressed.
 
 \section{Destination-Passing Style for Efficient Memory Management - Shaikhha et al. \cite{shaikhha_array_dps_2017}}
 While Bagrel mostly theorizes on the advantages of the \lad calculus,
-this paper give empirical evidence on runtime and memory improvements of Destination Passing Style (DPS) in a functional language.
+this paper gives empirical evidence on runtime and memory improvements of Destination Passing Style (DPS) in a functional language.
 Shaikhha et al. demonstrate the benefits of implementing a DPS-transformation step into the compilation of an array-programming language.
-The authors chose to not give any direct memory control to the programmer, but their intermediate language '\dpsf' still feature
+The authors chose to not give any direct memory control to the programmer, but their intermediate language '\dpsf' still features
 some similarity to \lad.
 \dpsf is typed using a shape type, which contains the dimensions of the array, which will be written to a memory location/ destination.
-Because of to the array-programming nature of the language, the shape type is fit only to arrays, but displays some flexibility, 
+Because of the array-programming nature of the language, the shape type is fit only to arrays, but displays some flexibility, 
 which, in a way, is more akin to the constructors used in \lad than to the holes used by Minamide \cite{minamide_holes_1998}.
 
 \section{Tail Modulo Cons - \cite{bour_et_al_tmc_2021}}
-This paper proposes a annotation controlled, compile time transformation of OCaml into a DPS intermediate language.
+This paper proposes a annotation-controlled, compile time transformation of OCaml into a DPS intermediate language.
 The intermediate language only features structures with single holes/ single destinations.
 The driving goal of Tail Modulo Cons (TMC) is, as the name suggests, to elevate the issues of constructors wrapping a recursive call.
-Particularly TMC allows for tail recursion, even if the recursive call is hidden behind a data constructor.
+Particularly, TMC allows for tail recursion, even if the recursive call is hidden behind a data constructor.
 While TMC is an intermediate language it allows for some source level control, as only annotated functions are converted into DPS.
 
 
@@ -99,8 +99,8 @@ Bernardy et al. give deeper insight into linear typing as it is the sole focus o
 They focus on implementing linear typing in Haskell but give good intuition on linear types as a whole.
 Though unrestricted types are not a core language feature but implemented in the language itself, the type system is
 very similar to \lad, in fact the calculi even share syntax for the linear function.
-Bernardy et al discuss many benefits of linear typing and \lad in it's whole bases on the idea of linear types to make
+Bernardy et al. discuss many benefits of linear typing and \lad in its whole is based on the idea of linear types to make
-multiple writes on data impossible.
+multiple writes to data impossible.
 
 \section{A Unified View of Modalities in Type Systems - Abel and Bernardy \cite{abel_bernardy_2020}}
 \lad includes a notion of modality using the exponential $!_mT$, of which the ground work is laid by Abel and Bernardy in this work.