topics_compiler/slides/main.md

paginate, _paginate, footer, _footer, style

paginate	_paginate	footer	_footer	style
true	false	Topics in Compilers and Concurrency · Julius Fischer · 10.06.2026		h1 { position: absolute; top: 60px; left: 75px; right: 75px; }

\def\leftcirc{{\triangleleft\kern-0.1em\circ}}
\def\myor{{\;|\;}}
\def\dest{{\rightarrow}}
\def\lad{\lambda_d\;}
\newcommand{\htype}[1]{{\lfloor #1 \rfloor}}
\newcommand{\ampar}[3]{{\;_#1\langle #2 \;_{\tiny \land} \; #3 \rangle}}
\newcommand{\mapstom}[1]{{\sideset{_#1}{}\mapsto}}

Destination Calculus:

A Linear 𝜆-Calculus for Purely Functional Memory Writes

Thomas Bagrel, Arnaud Spiwack

Topics in Compiler and Concurrency

Julius Fischer

10. Juni 2026

---

What are Destinations?

• Destination Passing Style
  • Imperative
  • Function takes destination instead of returning structure

---

Example in C

int* vec_add(int v1[], int v2[], int size) {
    int* res =  malloc(size * sizeof(int));
    for (int i = 0; i < size; i++) {
        res[i] = v1[i] + v2[i];
    }
    return res;
}

• Add an 'out parameter'

void dps_vec_add(int res[], int v1[], int v2[], int size) {
    for (int i = 0; i < size; i++) {
        res[i] = v1[i] + v2[i];
    }
}

---

Motivation for DPS

• Typical functional map implementation

map f (x:xs) = (f x : map f xs1)
> (f x : map f xs) 
> (map f x1 : (f x2 : map f xs2)) 
> ...

• Not tail recursive
  • Performance issue
  • Inefficient stack growth

map f (x:xs) dest = map f xs (push dest (f x))
> map f xs1 (push dest (f x1))
> map f xs2 (push dest (f x2))

---

DPS in functional languages

• Just add pointers to mutable data?
  • Int \mapsto Int \mapsto \textcolor{red}{T}
  • \textcolor{red}{T *}\mapsto Int \mapsto Int \mapsto \dots
• Multiple issues with this
  • Memory safety
  • Multilpe writes on shared memory
  • Purity

---

Destination Calculus: Terminology

• Holes Values h_1, h_2, \dots
• Destination \dest h_1 \dest h_2, \dots
• Ampars \ampar{H}{v_1}{v_2}, i.e. \ampar{{\{h\}}}{(h, 15)}{\dest h}
• v_1 "value with holes"
• v_2 "value of destinations"

---

Destination Calculus: Terms in \lad

• Basic FP terms

t, u := x \myor t' t \;|\; t ; t' \;|\; \dots

• Case for all datatypes

\begin{align}
    \dots \myor 
    &case\;t\;of\;(v_1, v_2) \mapsto u \myor\\
    &case\;t\;of\;(Inl\;v_1) \mapsto u \myor \dots
\end{align}

• Additions for destination passing

\begin{align}
    \dots \myor
    &
    new_\ltimes \myor
    from_\ltimes t \myor
    to_\ltimes t \myor
    upd_\ltimes \; t \; with \; x \mapsto t' \myor\\
    &
    t \blacktriangleleft t' \myor
    t  \leftcirc t' \myor
    t \triangleleft () \myor
    t \triangleleft Inl \myor
    t \triangleleft (,) \myor \dots
\end{align}

---

Destination Calculus: Constructors

• Usually constructors are required Inl, Inr, (a, b), \lambda x \mapsto t
• In \lad we simply 'refine' holes Inl \; t \triangleq from_\ltimes' (upd_\ltimes\; new_\ltimes\; with \; d \mapsto d \triangleleft Inl \blacktriangleleft t) \lambda x \mapsto t \; \triangleq from_\ltimes' (upd_\ltimes\; new_\ltimes\; with \; d \mapsto d \triangleleft (\lambda x \mapsto t))

---

Destination Calculus: Map example

[1] Thomas Bagel

---

Destination Calculus: Linearity and Modality

• Double writes are an issue
  • If a hole is used more than once (dest \blacktriangleleft v_1; dest \blacktriangleleft v_2; \dots)
  • In types like \htype{\htype{T}}
• Solved using modality of Multiplicity and Age m = p \cdot a p = 1 \myor \omega a =\; \uparrow^k \myor \infty for k \in \mathbb{N}_0
• With 1 \underset{\raise{0.4em}{\leftarrow}}{<}^p \omega, \uparrow^k \underset{\raise{0.4em}{\leftarrow}}{<}^a \infty

---

Destination Calculus: Linearity and Modality

• Add modalities to variable bindings

\begin{align}
    \dots \myor 
    &case_m\;t\;of\;(v_1, v_2) \mapsto u \myor\\
    &case_m\;t\;of\;(Inl\;v_1) \mapsto u \myor\\
    &\lambda x\; \mapstom{m} \; t \myor \dots
\end{align}

• And add add exponential modality to weaken constraints

\begin{align}
    \dots \myor 
    &Mod_m\; t \myor \dots
\end{align}

---

Destination Calculus: Typing

• Mostly standard

---

Referenes and Further Reading

---

Extra Slides If needed

---

Example for linear types

[1] Page 7

---

Example for linear types

[1] Page 8