资 源 简 介
mymms aims at the implementation of
a high-ordered typed lambda calculus (CiC)
a proof editing mode
a set of certified decision procedure (mainly oracles for the type checking)
Require ocaml >= 3.10
No documentation yet, but there is a begining tutorial, please look at the README file in archive (Downloads)
