摘要
一、引言近几年来,类型理论和基于类型理论的软件开发方法受到计算机界,特别是理论计算机科学界的广泛关注,吸引了不少研究人员,也取得了丰硕的成果。
Type theory and type-theorotic approaches to software development are currently active research areas in computer science.ELF(Edinburgh Logic Framework)is one of the representative results in these fields.The goal of ELF is to build a general theory of defining a wide class of logics,and to set up a valid foundation for developing logic-independent software tools. This paper gives a briefly introduction to the main idea of ELF and basic methods to define logics.Other type theories,such as Martin-L(?)f's intuit- ionistic type theory,Nuprl type theory and ALT type theory proposed by Prof.Li are compared with ELF.
出处
《计算机科学》
CSCD
北大核心
1992年第2期20-24,共5页
Computer Science