This repository contains a F* development made during my M2 internship at Inria Paris.

It contains implementations of basic data structures in Low* and Steel and an alternative verification method for Steel programs, using the generation of a functional translation. It does not work with recent versions of F* and it uses a custom version of F* after c37b4fe.