added slides

report/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}
+}

report/bibliography/acm_3158093.bib

@@ -0,0 +1,18 @@
+@article{lh_bernardy_2017,
+author = {Bernardy, Jean-Philippe and Boespflug, Mathieu and Newton, Ryan R. and Peyton Jones, Simon and Spiwack, Arnaud},
+title = {Linear Haskell: practical linearity in a higher-order polymorphic language},
+year = {2017},
+issue_date = {January 2018},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {2},
+number = {POPL},
+url = {https://doi.org/10.1145/3158093},
+doi = {10.1145/3158093},
+abstract = {Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility and code reuse across linear and non-linear users of a library. Only then can the benefits of linear types permeate conventional functional programming. Rather than bifurcate types into linear and non-linear counterparts, we instead attach linearity to function arrows. Linear functions can receive inputs from linearly-bound values, but can also operate over unrestricted, regular values. To demonstrate the efficacy of our linear type system — both how easy it can be integrated in an existing language implementation and how streamlined it makes it to write programs with linear types — we implemented our type system in ghc, the leading Haskell compiler, and demonstrate two kinds of applications of linear types: mutable data with pure interfaces; and enforcing protocols in I/O-performing functions.},
+journal = {Proc. ACM Program. Lang.},
+month = dec,
+articleno = {5},
+numpages = {29},
+keywords = {typestate, polymorphism, linear types, linear logic, laziness, Haskell, GHC}
+}

report/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}
+}

report/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}
+}

report/bibliography/all.tex

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

report/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}
+}

report/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}
+}
+

report/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}
+}