论文部分内容阅读
通过类型理论使得程序语言在静态可以检查是否出错,这给程序语言带来许多优势。类型理论中的重要性质包括：弱化规则、删除规则、强化规则等。首先给出了结构归纳法、良基归纳法、规则归纳法和余归纳法的形式化定义。在给出PA4WS进程代数的语法、语义的基础上给出了其类型定义。在此基础上给出了归纳法在PA4WS类型理论性质证明的应用。