Comonads理论及其在计算机科学中的应用研究

作为Monads的范畴对偶概念，Comonads理论是理论计算机科学新兴的研究领域之一，也是目前范畴论和共代数研究中的一个前沿热点，在计算机科学中具有广阔的应用前景。本项目拟在项目组前期对范畴论、Monads理论、共代数及双代数研究的基础上，结合域理论、函数式程序语言和代数方法等相关理论，对Comonads理论的范畴论理论基础及与共代数的结合进行深入的研究，探讨Comonads在形式语义、程序语言设计、类型理论、代数和双代数等计算机科学领域中的应用。在此基础上，进一步结合具体的程序语言进行验证和完善，从而为促进Comonads理论在计算机科学中的广泛应用，并最终建立一套基于Comonads的形式语义及程序设计方法做一些前期的探索工作。本项目对于形式语义及程序语言设计等众多领域的研究具有十分重要的理论意义和应用价值，并且可以与Monads理论形成互补，促进范畴论和共代数在计算机科学中的应用。

共发表15篇论文，其中一级学报《计算机研究与发展》3篇，EI源刊《华南理工大学学报》6篇，SCI-E源刊Information（IF：0.25）1篇，教学论文1篇，其他核心期刊论文4篇，技术报告4篇，软件著作权3项；共培养博士生4名，硕士生14名，本科生25名，开设博士生专业课《形式语义》1门，并已为23名博士生授课。指导国家大学生创新实验项目3项，中央高校基本科研业务费项目1项，广东省大学生创新实验项目1项。获2012年中国教育部IBM优秀教师及2013年IBM优秀合作伙伴称号。.主要工作包括：（1）利用共代数研究共归纳数据类型，分析了终结共代数和共归纳原理在类型理论中的应用，并发表部分相关文章。这是国内最早介绍和研究共归纳数据类型研究的文章。（2）研究参数化范畴数据类型及共归纳数据类型上的各种共递归及计算律，特别是带固定和累积参数的共递归和hylomorphisms，相关论文先后发表在《华南理工大学学报》和《计算机研究与发展》。（3）利用双代数描述范畴数据类型上的观察与构造操作，并结合分配律探讨构造与行为、递归与共递归间的关系和性质。相关论文发表在《计算机研究与发展》、《INFORMATION》和《华南理工大学学报》。这是目前国内关于双代数及其在类型理论上的应用研究的主要文献。（4）研究CDT上的子类型关系，给出抑制射下的代数子类型和共代数子类型的定义、语义解释和定型规则，并将其扩展到双代数中，同时从范畴论的角度分析双代数中各种子类型和定型规则。相关论文发表在《华南理工大学学报》。（5）利用Haskell给出comonads的coKleisli三元组及其范畴的具体实现，结合实例说明如何将其应用于各种范畴数据类型的上下文依赖计算的抽象描述和推理中，并研究了comonads与monads间的分配律，指出如何通过分配律将副作用计算与上下文依赖计算有机地融合起来。另外，利用comonads给出共归纳数据类型的抽象描述。相关论文发表在《华南理工大学学报》。（6）撰写技术报告《类型理论中的归纳及共归纳数据类型》、《计算机科学中的范畴数据类型及其应用研究》和《Comonads理论及在软件设计中的应用》等，并作为博士生课程的辅助教材。.总地来说，本项目完成大部分原定目标，但在高水平论文方面仍存在许多不足，特别是SCI论文。本人承诺将在2015年完成原定的SCI论文指标。