Destination calculus: A linear λ-calculus for purely functional memory writes
summary
Presents a concrete calculus that compiles destination‑passing into pure functional code and shows nontrivial examples: a tail‑recursive map implemented with in‑place list growth and a breadth‑first numbering of a tree using a functional queue built from destinations. Defines a destination calculus and a modal type system that tracks linearity plus numeric scope ages to prevent escapes. Type safety is mechanically proved in Coq proof, artifacts and reproducible results accompany the paper (DOI provided).
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:42Tail-recursive map in pure FP
- 2:06Mutation solves map elegantly
- 3:331990s linear continuations
- 4:59Linear types vs reference counting
- 6:03Functions as ampars and destinations
- 8:11Linear types insufficient for destinations
- 9:40New type system for destinations
- 11:05Summary
- 11:34Q&A
related talks
30mLambda Calculus: The Origins of Functional Programming
22mA Calculus of Inductive Linear Constructions
36mDependently Typed Multi-Stage Programming, Revisited
21mTail Modulo Cons, OCaml, and Relational Separation Logic
30mThe Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi...
26mTemporal refinements for Call-By-Push-Value with fixpoint
19mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…)
16mSoundly Handling Linearity