final

bibliography/acm_3408972.bib

@@ -0,0 +1,18 @@
+@article{abel_bernardy_2020,
+author = {Abel, Andreas and Bernardy, Jean-Philippe},
+title = {A unified view of modalities in type systems},
+year = {2020},
+issue_date = {August 2020},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {4},
+number = {ICFP},
+url = {https://doi.org/10.1145/3408972},
+doi = {10.1145/3408972},
+abstract = {We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose.},
+journal = {Proc. ACM Program. Lang.},
+month = aug,
+articleno = {90},
+numpages = {28},
+keywords = {subtyping, modal logic, linear types}
+}

bibliography/all.tex

@@ -1 +1 @@
-\bibliography{bibliography/acm_3122948.3122949,bibliography/acm_3720423,bibliography/minamide}
+\bibliography{bibliography/acm_3122948.3122949,bibliography/acm_3158093,bibliography/acm_3408972,bibliography/acm_3720423,bibliography/bour_et_al_2021,bibliography/diss,bibliography/minamide}

bibliography/bour_et_al_2021.bib

@@ -0,0 +1,8 @@
+@article{bour_et_al_tmc_2021,
+  title={Tail Modulo Cons},
+  author={Fr{\'e}d{\'e}ric Bour and Basile Cl{\'e}ment and Gabriel Scherer},
+  journal={ArXiv},
+  year={2021},
+  volume={abs/2102.09823},
+  url={https://api.semanticscholar.org/CorpusID:231967558}
+}

bibliography/diss.bib

@@ -0,0 +1,17 @@
+@ARTICLE{bagrel_thesis_2025,
+       author = {{Bagrel}, Thomas},
+        title = "{Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings}",
+      journal = {arXiv e-prints},
+     keywords = {Programming Languages},
+         year = 2026,
+        month = jan,
+          eid = {arXiv:2601.08529},
+        pages = {arXiv:2601.08529},
+          doi = {10.48550/arXiv.2601.08529},
+archivePrefix = {arXiv},
+       eprint = {2601.08529},
+ primaryClass = {cs.PL},
+       adsurl = {https://ui.adsabs.harvard.edu/abs/2026arXiv260108529B},
+      adsnote = {Provided by the SAO/NASA Astrophysics Data System}
+}
+

main.tex

@@ -35,7 +35,7 @@
 \author{Julius Fischer}
 %
 %
-\institute{Student at Univerity of Freiburg (ALU)\\
+\institute{Student at University of Freiburg (ALU)\\
     \email{julius.fischer@email.uni-freiburg.com}\\
     Matriculation Number: 5317202
     }
@@ -63,37 +63,61 @@ both directly in their calculus grammar and semantics, but also in their structu
 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.
 
-\section{A Functional Representation of Data Structures with a Hole by Y. Minamide\cite{minamide_holes_1998}}
+\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.
 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 generael Minamide focusses more on the similarity of his hole abstraction to the regular $\lambda$ abstraction
+In general Minamide focuses more on the similarity of his hole abstraction to the regular $\lambda$ abstraction
-and the similarity of a strucutre 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 an type $T_2$, when applied argument to an argument $T_1$.
-Notably both calculi contain linearity constraints on holes, but Bagrel's work eliviates some of those constraints by allowing for weakening.
+Notably both calculi contain linearity constraints on holes, but Bagrel's work elevates some of those constraints by allowing for weakening.
 Overall Minamide lays a lot of ground work, and influences that can be seen in the \lad formulation and in its discussion, as
-similar benefits regarding tail recursion are adressed.
+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 emprical evidence on runtime and memory improvements of Destination Passing Style (DPS) in a functional language.
+this paper give 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
 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 langauge, the shape type is fit only to arrays, but displays some flexibility, 
+Because of to 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.
+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.
+While TMC is an intermediate language it allows for some source level control, as only annotated functions are converted into DPS.
+
+
 \section{Linear Haskell: practical linearity in a higher-order polymorphic language - Bernardy et al. \cite{lh_bernardy_2017}}
 Linear logic/ typing stands at the core of the \lad type system, and its concrete form is massively influenced by Linear Haskell.
 Bernardy et al. give deeper insight into linear typing as it is the sole focus of this paper. 
-They focus on implementing linear typing in haskell but give good intuition on linear types as a whole.
+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 lienar types to make
+Bernardy et al discuss many benefits of linear typing and \lad in it's whole bases on the idea of linear types to make
 multiple writes on 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.
+They discuss modalities not exclusively for linear types in rigorous formality, diving into the precise algebraic and logical background.
+In fact this paper shows a generalization of the modes used in \lad's type system, to ensure linearity.
+The main strategy, which is used in \lad, is including the modality in an algebraic structure of the calculus (by indexing the modality $!_m$).
+Bagrel claims this approach "greatly simplif[ies] [the] context management (especially in the computer-mechanized proofs)" \cite{bagrel_dp_2025} (Page 11).
+
+
+
+\section{Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings - \cite{bagrel_thesis_2025}}
+Another honorable mention is Bagrel's dissertation, in which the author not only includes the findings of the original paper but 
+also goes into further detail regarding linear typing and the entire intuition behind \lad.
+It includes a more comprehensive explanation for most of which is covered in the article, as well as further on the usefulness of \lad
+and an application of it.
+
+
 \input{./bibliography/all.tex}
 \bibliographystyle{splncs04}
 \end{document}

main.tex.bak

@@ -0,0 +1,123 @@
+% This is samplepaper.tex, a sample chapter demonstrating the
+% LLNCS macro package for Springer Computer Science proceedings;
+% Version 2.21 of 2022/01/12
+%
+\documentclass[runningheads]{llncs}
+%
+\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.
+%
+\usepackage{graphicx}
+% Used for displaying a sample figure. If possible, figure files should
+% be included in EPS format.
+%
+% If you use the hyperref package, please uncomment the following two lines
+% to display URLs in blue roman font according to Springer's eBook style:
+%\usepackage{color}
+%\renewcommand\UrlFont{\color{blue}\rmfamily}
+%\urlstyle{rm}
+%
+
+% My packages:
+\usepackage{unicode-math}
+\usepackage{hyperref}
+
+\begin{document}
+%
+\title{Topics in Compilers and Concurrency \\ Seminar Report on\\ Background Materials and Related Work}
+%
+%\titlerunning{Abbreviated paper title}
+% If the paper title is too long for the running head, you can set
+% an abbreviated paper title here
+%
+\author{Julius Fischer}
+%
+%
+\institute{Student at Univerity of Freiburg (ALU)\\
+    \email{julius.fischer@email.uni-freiburg.com}\\
+    Matriculation Number: 5317202
+    }
+
+
+%
+\maketitle              % typeset the header of the contribution
+%
+%\begin{abstract}
+%The abstract should briefly summarize the contents of the paper in
+%150--250 words.
+%
+%\keywords{First keyword  \and Second keyword \and Another keyword.}
+%\end{abstract}
+%
+%
+%
+
+\newcommand{\lad}{$\lambda_d$}
+\newcommand{\dpsf}{DPS-$\tilde{F}$}
+
+\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.
+This report will highlight a number of select works, which are of significance to the $lambda_d$ 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.
+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 generael Minamide focusses more on the similarity of his hole abstraction to the regular $\lambda$ abstraction
+and the similarity of a strucutre containing a hole, to a function that returns an type $T_2$, when applied argument to an argument $T_1$.
+Notably both calculi contain linearity constraints on holes, but Bagrel's work eliviates some of those constraints by allowing for weakening.
+Overall Minamide lays a lot of ground work, and influences that can be seen in the \lad formulation and in its discussion, as
+similar benefits regarding tail recursion are adressed.
+
+\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 emprical 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
+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 langauge, 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 controled, compile time transformation of OCaml into a DPS itermediate 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 eliviate 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.
+While TMC is an intermediate langauge it allows for some source level control, as only annotated functions are converted into DPS.
+
+
+\section{Linear Haskell: practical linearity in a higher-order polymorphic language - Bernardy et al. \cite{lh_bernardy_2017}}
+Linear logic/ typing stands at the core of the \lad type system, and its concrete form is massively influenced by Linear Haskell.
+Bernardy et al. give deeper insight into linear typing as it is the sole focus of this paper. 
+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 lienar types to make
+multiple writes on 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.
+They discuss modalities not exlusively for linear types in rigorous formality, diving into the precise algebraic and logical background.
+In fact this paper shows a generilization of the modes used in \lad's type system, to ensure linearity.
+The main strategy, which is used in \lad, is including the modality in an algebraic structure of the calculus (by indexing the modality $!_m$).
+Bagrel claims this approach "greatly simplif[ies] [the] context management (especially in the computer-mechanized proofs)" \cite{bagrel_dp_2025} (Page 11).
+
+
+
+\section{Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings - \cite{bagrel_thesis_2025}}
+Another honorable mention is Bagrel's dissertation, in which the author not only includes the findings of the original paper but 
+also goes into further detail regarding linear typing and the entire intuition behind \lad.
+It includes a more comprehensive explanation for most of which is convered in the article, as well as further on the usefulness of \lad
+and an application of it.
+
+
+\input{./bibliography/all.tex}
+\bibliographystyle{splncs04}
+\end{document}

readme.md

@@ -24,5 +24,5 @@
 - Google scholar
 - scienceos.ai
 
-- Peton Jones How to write a great research paper
+- Payton Jones How to write a great research paper
 - Mal Plagiatsding lesen auf Wikipedia