Eric Marion
I design programming languages with restricted dependent types. Sleight pairs Kernel-style dynamism with static types: multiplicities on every binder, a termination check with no escape, and LLMs as intended authors. It is self-hosting and compiles to OCaml. Pledge, loosely based on Sleight, is a small teaching language whose browser editor shows what the type checker knows at every point of a program.
Projects
Pledge
A small language for learning restricted dependent types. It runs in the browser, with a tutorial
that goes from Nat to proofs about addition and multiplication.
Sleight
An s-expression language with restricted dependent types, a multiplicity on every binder
(erased, many or unique), and a termination check with no escape.
It has a reference implementation in OCaml, a self-hosting compiler to OCaml, and a Lean model of a fragment.