Other Writing
Revised version of the formal semantics from the
ESOP 2014 paper,
and a type erasure pass identifying which type-level information
is actually used at run time.
Lecture notes for a formal methods seminar
on work which grew into the
ARRAY 2018 paper.
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.