---
paginate: true
_paginate: false
footer: Topics in Compilers and Concurrency · Julius Fischer · 10.06.2026
_footer: ""
style: |
  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
![h:450](img/map_dps.jpg)
[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

![](img/linear_works.jpg)
[1] Page 7

---

# Example for linear types
![](img/linear_fails.jpg)
[1] Page 8