initial commit

.gitignore

@@ -0,0 +1 @@
+out

bibliography/acm_3122948.3122949.bib

@@ -0,0 +1,17 @@
+@inproceedings{shaikhha_array_dps_2017,
+author = {Shaikhha, Amir and Fitzgibbon, Andrew and Peyton Jones, Simon and Vytiniotis, Dimitrios},
+title = {Destination-passing style for efficient memory management},
+year = {2017},
+isbn = {9781450351812},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/3122948.3122949},
+doi = {10.1145/3122948.3122949},
+abstract = {We show how to compile high-level functional array-processing programs, drawn from image processing and machine learning, into C code that runs as fast as hand-written C. The key idea is to transform the program to destination-passing style, which in turn enables a highly-efficient stack-like memory allocation discipline.},
+booktitle = {Proceedings of the 6th ACM SIGPLAN International Workshop on Functional High-Performance Computing},
+pages = {12–23},
+numpages = {12},
+keywords = {Array Programming, Destination-Passing Style},
+location = {Oxford, UK},
+series = {FHPC 2017}
+}

bibliography/acm_3720423.bib

@@ -0,0 +1,18 @@
+@article{bagrel_dp_2025,
+author = {Bagrel, Thomas and Spiwack, Arnaud},
+title = {Destination Calculus: A Linear $𝜆$-Calculus for Purely Functional Memory Writes},
+year = {2025},
+issue_date = {April 2025},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {9},
+number = {OOPSLA1},
+url = {https://doi.org/10.1145/3720423},
+doi = {10.1145/3720423},
+abstract = {Destination passing —aka. out parameters— is taking a parameter to fill rather than returning a result from a function. Due to its apparently imperative nature, destination passing has struggled to find its way to pure functional programming. In this paper, we present a pure functional calculus with destinations at its core. Our calculus subsumes all the similar systems, and can be used to reason about their correctness or extension. In addition, our calculus can express programs that were previously not known to be expressible in a pure language. This is guaranteed by a modal type system where modes are used to manage both linearity and scopes. Type safety of our core calculus was proved formally with the Coq proof assistant.},
+journal = {Proc. ACM Program. Lang.},
+month = apr,
+articleno = {89},
+numpages = {27},
+keywords = {Destination Passing, Functional Programming, Linear Types, Pure Language}
+}

bibliography/all.tex

@@ -0,0 +1 @@
+\bibliography{bibliography/acm_3122948.3122949,bibliography/acm_3720423,bibliography/minamide}

bibliography/minamide.bib

@@ -0,0 +1,16 @@
+@inproceedings{minamide_holes_1998,
+author = {Minamide, Yasuhiko},
+title = {A functional representation of data structures with a hole},
+year = {1998},
+isbn = {0897919793},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+url = {https://doi.org/10.1145/268946.268953},
+doi = {10.1145/268946.268953},
+abstract = {Data structures with a hole, in other words data structures with an uninitialized field, are useful to write efficient programs: they enable us to construct functional data structures flexibly and write functions such as append and map as tail recursive functions. In this paper we present an approach to introducing data structures with a hole into call-by-value functional programming languages like ML. Data structures with a hole are formalized as a new form of λ-abstraction called hole abstraction. The novel features of hole abstraction are that expressions inside hole abstraction are evaluated and application is implemented by destructive update of a hole. We present a simply typed call-by-value λ-calculus extended with hole abstractions. Then we show a compilation method of hole abstraction and prove correctness of the compilation.},
+booktitle = {Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+pages = {75–84},
+numpages = {10},
+location = {San Diego, California, USA},
+series = {POPL '98}
+}

main.tex

@@ -0,0 +1,90 @@
+% 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 by 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}.
+
+\input{./bibliography/all.tex}
+\bibliographystyle{splncs04}
+\end{document}

makefile

@@ -0,0 +1,11 @@
+.PHONY: clean bib
+
+all: clean bib compile
+
+bib:
+	@files=$$(ls -1 bibliography/*.bib | sed 's/\.bib//' | paste -sd, -); \
+	echo "\\bibliography{$$files}" > ./bibliography/all.tex;
+clean:
+	rm -rf ./out ./bibliography/all.tex
+compile: bib
+	latexmk -lualatex -output-directory=out main.tex

readme.md

@@ -0,0 +1,11 @@
+# Paper notes
+
+## Main paper
+
+- a destination is always linear and of finite age
+- Evaluation context is
+    - a stack that keeps track of the term in focus
+    - typed with rules, similar to the term typings
+    - A nice thing to express small step semantics (I can see how the proof gets easy with progress being a given here)
+
+- Small step semantics need some special renaming semantics for holes (maybe worth looking into)