Constructive Mathematics and Computer-Assisted Reasoning Systems

Susumu Hayashi
Additional contact information
Susumu Hayashi: Kyoto University, Research Institute for Mathematical Sciences

A chapter in Mathematical Logic, 1990, pp 43-52 from Springer

Abstract: Abstract 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.

Keywords: Type Theory; Springer Lecture Note; Constructive Mathematic; Lambda Calculus; Equality Judgement (search for similar items in EconPapers)
Date: 1990
References: Add references at CitEc
Citations:

There are no downloads for this item, see the EconPapers FAQ for hints about obtaining it.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:sprchp:978-1-4613-0609-2_4

Ordering information: This item can be ordered from
http://www.springer.com/9781461306092

DOI: 10.1007/978-1-4613-0609-2_4

Access Statistics for this chapter

More chapters in Springer Books from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().