Skip to content

Mechanized Metatheory in F*

Catalin Hritcu edited this page Jul 21, 2017 · 8 revisions

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

Clone this wiki locally