Home Tags Contact Projects

Fall 2020 Plans 2020-09-04

RIP, 5 month gap.

Short-Term Plans (Next Semester)

Long-Term Plans (Thesis?)

Algebraic Effects in Stahl

I think either linear types (or one of its extensions, such as quantitative type theory) or /maybe/ coinduction might be able to fix the soundness issues? I don't know how to do the proofs of soundness for MLTT (or dependent type theories in general), so I'd need to learn to do those first.

Cubical Levitation

Even if I get the Stahl eliminators item above working, Stahl still won't have everything present in most HoTT/Cubical type theories. The biggest item is higher inductive types (HITs). I don't think these should actually be too incredibly hard to work in, but I don't know what soundness problems exist with HITs, and I should like, actually learn the mathematical model behind cubical type theory.

Formally Verifying StahlOS

The parts of the implementation that (in my opinion at least) it makes sense to formally verify are:

This notably excludes the serial driver and the bootloader, but I think I'd like to try and verify everything from when the bootloader hands off to the kernel on.

I think this would probably have me learning separation logic, and possibly one of the theorem provers with better support for calling an SMT solver (e.g. Isabelle, though I remember a paper about extending Coq with one).