parsing:  list of tokens into higher-order abstract syntax
          mix left and right recursion

 foll.cfg       -- parsing of first-order formulae into HOAS
 arithml.cfg    -- parsing of arithmetic expressions, functions
                   and function application into HOAS

 tab.cfg        -- recognition and parsing (example from 
                   D.S. Warren: "Programming in tabled Prolog",
                   CH 5, illustrates efficient implementation 
                   of recognizers and parsers.

refine : refinement types (Pfenning, Davies ICFP00)
         for binary number representations.

         extended with type zero

mini-ml : evaluation semantics as a rewrite system

cr      : lambda-calculus
          simple rewriting and conversions

           
subtype1: subtyping for the fragment of Mini-ML 
          which does not have functions. 
        
subtype : subtyping for full Mini-ML
          (there might be infinitely many types)
     

poly    : polymorphic type inference 
          (doesn't run currently -- needs abstraction)

ccc     : cartesian closed categories. 
          (doesn't run currently -- needs abstraction)

tests   : some simple testing programs,
          graph reachability, etc.