纯函数式I/O的操作语义

目前被人们广泛采用的处理函数式I／O的机制有三种：Monad，Dialogue，CPS．本文采用CCS的理论和方法，把互模拟等价作为I／O程序的相等关系，描述了这三种I／O机制的操作语义，推导出这三种I／O机制相互之间的转换关系，从而证明了这三种I／O机制在语义上是等价的．

合成型语言FOPL的语义研究

函数式面向对象程序设计语言ＦＯＰＬ，是笔者设计并实现的一种同时支持函数式程序设计和面向对象程序设计的合成型智能语言，本文在一个全称抽象域上描述了它的指称语义，进而讨论了一个和该指称语义计算一致的按值调用的操作语义。

函数式语言中赋值语句(之二)

为了能够较好地处理函数式程序设计语言中的I/O问题 ,通过采用Monad方法将I/O加入到函数式程序设计语言中 ,来保持函数式程序设计语言的优点 .本文探讨了在函数式I/O系统中加入赋值操作与其引用透明性的问题 .

基于逻辑框架LF的语义性质之验证

本文对基于类型理论逻辑框架(LF)的语义性质验证加以研究,针对函数式语言 LAZY-PCF+SHAR,利用计算机辅助推理方法和技术给出相应的形式化描述及相关性质证明,从而提倡严格的和计算机辅助的证明在语义性质验证方面的应用。同时,考察了 LF 以及其实现系统 Plastic 的能力。