Strata

Fill-in proof for ProgramWF (#162)

Add Laurel, a language for compiling Java to, and in the future also other languages (#152)

Rearrange `sizeOf` to ease termination proofs (#133)

Update Lean toolchain to v4.24.0 (#172)

Improve efficiency of creating a Strata program from source string. (#171)