Mechanized Metatheory in F*

Current formalizations

• StlcStrongDbParSubst.fst strong reduction + parallel substitutions (scales best)

• StlcCbvDbParSubst.fst variant for CBV + parallel substitutions (awkward special case)

• STLC SF style from tutorial (might correspond to one of the below?)

• StlcCbvDbPntSubstNoLists.fst variant for CBV + point substitutions (SF style?)

• StlcCbvDbPntSubstLists.fst variant for CBV + point substitutions + lists for environments (SF style? awkward)

• STLC + ints/pairs/sub/letrec (SF style, old) <fstar-priv>/courses/sb2015/hw/05-sol/

• LambdaOmega.fst

• [System F-omega](https://github.com/FStarLang/FStar/blob/stratified_last/examples/metatheory/FOmega.fst) -- stratified and never as clean as LambdaOmega

Old micro-F* formalization by Simon

• MicroFStar.fst

• Simon's report

Directions

System F, LF, CC, CC-omega, CIC, ..., EMF*, ..., F*

https://github.com/FStarLang/FStar/wiki/Project-topics-on-F%2A#mechanized-metatheory-in-f