diff --git a/main.tex.bak b/main.tex.bak deleted file mode 100644 index af0acdf..0000000 --- a/main.tex.bak +++ /dev/null @@ -1,123 +0,0 @@ -% 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} diff --git a/bibliography/acm_3122948.3122949.bib b/report/bibliography/acm_3122948.3122949.bib similarity index 100% rename from bibliography/acm_3122948.3122949.bib rename to report/bibliography/acm_3122948.3122949.bib diff --git a/bibliography/acm_3158093.bib b/report/bibliography/acm_3158093.bib similarity index 100% rename from bibliography/acm_3158093.bib rename to report/bibliography/acm_3158093.bib diff --git a/bibliography/acm_3408972.bib b/report/bibliography/acm_3408972.bib similarity index 100% rename from bibliography/acm_3408972.bib rename to report/bibliography/acm_3408972.bib diff --git a/bibliography/acm_3720423.bib b/report/bibliography/acm_3720423.bib similarity index 100% rename from bibliography/acm_3720423.bib rename to report/bibliography/acm_3720423.bib diff --git a/bibliography/all.tex b/report/bibliography/all.tex similarity index 100% rename from bibliography/all.tex rename to report/bibliography/all.tex diff --git a/bibliography/bour_et_al_2021.bib b/report/bibliography/bour_et_al_2021.bib similarity index 100% rename from bibliography/bour_et_al_2021.bib rename to report/bibliography/bour_et_al_2021.bib diff --git a/bibliography/diss.bib b/report/bibliography/diss.bib similarity index 100% rename from bibliography/diss.bib rename to report/bibliography/diss.bib diff --git a/bibliography/minamide.bib b/report/bibliography/minamide.bib similarity index 100% rename from bibliography/minamide.bib rename to report/bibliography/minamide.bib diff --git a/main.tex b/report/main.tex similarity index 100% rename from main.tex rename to report/main.tex diff --git a/makefile b/report/makefile similarity index 100% rename from makefile rename to report/makefile diff --git a/slides/makefile b/slides/makefile new file mode 100644 index 0000000..09b30b9 --- /dev/null +++ b/slides/makefile @@ -0,0 +1,8 @@ +.PHONY: clean bib + +all: clean bib compile + +clean: + rm -rf ./out +compile: + marp src.md --theme ./themes/academic.css -o out/presentation.html diff --git a/slides/src.md b/slides/src.md new file mode 100644 index 0000000..d3af208 --- /dev/null +++ b/slides/src.md @@ -0,0 +1,18 @@ +--- +theme: dracula +paginate: true +_paginate: false +footer: Mini-Haskell · Julius Fischer · 19.11.2024 +_footer: "" +--- + +# Destination Calculus: +## A Linear 𝜆-Calculus for Purely Functional Memory Writes +### Technische Fakultät Freiburg +#### Julius Fischer + +###### 10. Juni 2026 + +--- + +# Referenes