类型是编程语言中的一个很重要的概念，它定义了一个变量的内存布局和这个变量可以使用的运算符。类型在实际程序中，特别是面向对象程序中具有重要意义。经典分离逻辑是一种可应用于包含共享可操作数据结构程序的形式化证明系统，但它仅对程序中的数据值定义了推导方式，而并没有支持程序中的类型属性及其推导。为了扩展分离逻辑对于类型推导的支持，本文将在经典分离逻辑的基础上定义一种支持类型的分离逻辑。　　该支持类型的分离逻辑将扩展所能描述的基础变量类型集（包括字符型、浮点类型等），并提供其上的指针类型和数组类型的支持;增加对和类型相关的命令的支持（包括变量声明、强制类型转换、自定义类型转换方式等）;提供了对类型别名的处理方式。　　本文定义了一种类C语言Cmini，该语言支持以上所扩展的和类型相关的描述与功能。然后分别定义了Cmini语言程序中表达式和命令的操作语义和指称语义，并定义了相关的断言语言，然后给出了描述Cmini语言程序的支持类型的分离逻辑的霍尔规则。　　该支持类型的分离逻辑是一个严格的逻辑证明系统，能够对程序进行严格地形式化推导，并将类型和分离逻辑有机地结合在一起，可同时对程序中变量的类型和值进行描述。并且该支持类型的分离逻辑可对类型别名、自定义类型转化方式和强制类型转换等进行处理。