Brendan Zabarauskas brendanzab

Note to readers: This document is an early draft of a model for memory-safe references that I've been working on for the last ~2 years. While I think it is quite promising, the design is unfinished. The "regions" that I present in this document have not been given a formal semantics, and I have not explained where they originate from. My goal is merely to convince you that the design is promising, and that if seen to completion, it would advance the frontier of zero-cost memory safety.

Update March 2025: I am working on a newer version of this proposal, that aims to simplify the model substantially. When I have finished that proposal, I will put a link here.

Update August 2025: Verdagon has written an awesome blog post that explains this proposal at a high level. I recommend you check it out!

Abstract

In this document, I present a novel model for memory-safe references that aims to significantly improve upon the Rust-inspired model that Mojo c

description	Inversion hell.

Lightweight region memory management in a two-stage language

Intro
Basics
- Stage inference
Regions
- Bit-stealing
- Using regions
Eager regions

Basic setup for formalizing elaboration

First attempts

Elaboration is, broadly speaking, taking user-written syntax and converting it to "core" syntax by filling in missing information and at the same time validating that the input is well-formed.

I haven't been fully happy with formalizations that I previously used, so I make a new attempt here. I focus on a minimal dependently typed case.

A somewhat brief overview of typechecking System F

This document comprises an example of typechecking a type system based on System F, in a small ML-like language.

You can skip the below section if you already understand System F itself.

A brief overview of System F

System F is the name given to an extension of the simply typed lambda calclus.

	-- Polarized lambda calculus to A-normal form
	-- With eta-expansion and call-saturation

	type Ix = Int
	type Lvl = Int

	data Ty = TInt
	deriving (Show)
	data TFun = TFun [Ty] Ty
	deriving (Show)

	type never = \|
	type ('a, 'b) equal = Refl : ('x, 'x) equal

	type ('l, 'r) dec_equal =
	\| D_refl : ('l, 'l) dec_equal
	\| D_neq : (('l, 'r) equal -> never) -> ('l, 'r) dec_equal

	let ( let* ) v f = Option.bind v f

	module Nat = struct

	Set Implicit Arguments.
	Require Import List Program FunctionalExtensionality.

	(** Proof of syntactic type safety for call-by-value STLC extended with ℕ. *)

	(** Names/Variables will be identified with a natural number.
	λx.λy.y x is represented as λλ0 1 *)
	Definition var : Type := nat.

	(** There is a need for partial maps, e.g., to keep track of what variable

	{-# OPTIONS --without-K #-}

	-- version 1, conversion is indexed over conversion
	module IndexedConv where

	data Con : Set
	data Ty : Con → Set
	data Sub : Con → Con → Set
	data Tm : ∀ Γ → Ty Γ → Set
	data Con~ : Con → Con → Set