Constructive mathematics in theory and programming practice

Philosophia Mathematica 7 (1):65-104 (1999)


The first part of the paper introduces the varieties of modern constructive mathematics, concentrating on Bishop's constructive mathematics (BISH). it gives a sketch of both Myhill's axiomatic system for BISH and a constructive axiomatic development of the real line R. The second part of the paper focusses on the relation between constructive mathematics and programming, with emphasis on Martin-L6f 's theory of types as a formal system for BISH.

Download options


    Upload a copy of this work     Papers currently archived: 72,694

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

72 (#163,348)

6 months
1 (#388,311)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Intuitionism an Introduction.Arend Heyting - 1956 - Amsterdam, Netherlands: North-Holland.
Varieties of Constructive Mathematics.D. S. Bridges - 1987 - Cambridge University Press.
Constructive Set Theory.John Myhill - 1975 - Journal of Symbolic Logic 40 (3):347-382.

View all 24 references / Add more references