April 30 规划

@Mestway 形式化证明，研究subtype
@wky 词法语法分析， 信道传输数据的类型匹配 + 传输方向 

@featheryleaf  自己过来领任务

重点：提取usage(cap + ob), 列出限制，求解

待确认：
1. usage subtype relation -- 是否syntax directed
2. usage reduction -- 顺序，可能需要回溯，是否逐步求解

扩展
基本类型（int，bool，chan*）
基本表达式 if then else， + - x, < <= > >=
解释执行
