Constructive Mathematics and Computer-Assisted Reasoning Systems

The relationship between constructive mathematics and computer science has been noticed for a long while. But it is rather recent that live interactions between constructive mathematics and computer science began. In theoretical aspects, metamathematics of constructive mathematics are utilized to give semantics of higher order functional programming languages. Researches of constructive mathematics in computer science are not just theoretical. Quite a few systems based on constructive mathematics have been designed and implemented. They are program verification systems, program extraction systems, and high-level programming languages. These developments of systems need theoretical investigations as well and so give new insights into constructive mathematics. Applications of constructive mathematics to semantics of programming languages have begun to produce significant feedbacks to constructive mathematics and related areas, see Hyland (1987), Longo and Moggi (1988+α). Although researches on constructive systems have not yet been used to unvail new aspects of constructive mathematics, there are clues of possible applications of computer systems to theoretical researches in constructive mathematics Coquand (1986), Howe (1987). It is reasonable to imagine that constructive mathematicians a decade later will be helped by computer systems as mathematicians are now helped by computer algebra systems like REDUCE. In this paper, we will give a survey of existing systems based on constructive mathematics to show the readers how constructive theories are used in actual systems.