The TypesNSemantics directory has been added to the top level of the repository. If you latex main then you get a formal description of the syntax and type-checking rules of a subset of Grace. Comments/corrections are welcome. Kim