Mechanized Metatheory in F* - FStarLang/FStar GitHub Wiki

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

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

Add a custom footer
⚠️ **GitHub.com Fallback** ⚠️