LSS.thy contains a complete implementation of our paper's type inference algorithm as well as a fully-mechanized proof of Theorem 4.1 from our paper (named ti_program_correct in LSS.thy). It is written in Isabelle/HOL (https://isabelle.in.tum.de).
ROOT specifies the Isabelle "session" for this directory. That is, an object-logic plus the collection of theories in the directory to be built/verified by Isabelle. In this case, the session, VerifyLSS, consists of the object-logic HOL plus our LSS theory, contained in LSS.thy.
To build/verify our proof, simply run
isabelle build -c -D .
in this directory. That will build the VerifyLSS session specified in ROOT.
On our machine it takes approximately a minute to complete verification, but it may take several minutes on your machine.
One can sanity check verification by breaking any part of LSS.thy and observing that the build fails. For instance, if one changes line 334 from < Suc (size_list (size_prod (\<lambda>x. 0) size_AS) cases + to > Suc (size_list (size_prod (\<lambda>x. 0) size_AS) cases +, building will print Failed to finish proof (line 337 of "~/LSSIsabelle/LSS.thy").
Note that we use the -c flag to ensure that Isabelle re-verifies our proof even if the hash of LSS.thy has not changed since the last time it was built. Also, note that isabelle -c -D . does not verify the object-logic, HOL. To verify everything, run isabelle build -f -D .. This will take significantly longer than isabelle build -c -D ..