My thesis proposal lays out both the work done so far and a plan for near-future work. At this point in time, I had dynamic semantics, a type system with a soundness proof, a sketch of a local type inference algorithm, and a type-directed process for translating to a language with explicit iteration. So the remaining research problems necessary to bring Remora into a fully working state are a constraint solver for array shapes, a more general term calculus, and optimizations to cut down on materializing large arrays.

Lecture notes for a seminar on type systems, giving an overview of affine and region typing in Cyclone, relaxing linear type discipline in Vault, and enforced channel-based communication protocols in Sing#.

Lecture notes for a seminar on type systems, covering linear, affine, and relevant types; their interactions with conventional type system features (e.g., polymorphism and mutable references); algorithmic type checking; and how to state and prove type soundness.