fstar-ni Using F* to prove non-interference for a well-typed subset of programs written in a small imperative language. Created by Asger Hautop Drewsen, Mads Svejstrup and Oskar Haarklou Veileborg