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, updated as exercises in F* tutorial
  • SF style, old but more(?): <fstar-priv>/courses/sb2015/hw/05-sol/

• LambdaOmega.fst

• System F-omega -- stratified and never as clean as LambdaOmega

Old micro-F* formalization by Simon

• MicroFStar.fst

• Simon's report

Normalization

• stlc-norm -- not very successful experiment

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