Constructive mathematics in theory and programming practice

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


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.



    Upload a copy of this work     Papers currently archived: 91,998

External links

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

Through your library

Similar books and articles


Added to PP

93 (#184,721)

6 months
17 (#148,367)

Historical graph of downloads
How can I increase my downloads?

References found in this work

Intuitionism.Arend Heyting - 1956 - Amsterdam,: North-Holland Pub. Co..
Over de grondslagen der wiskunde..L. E. J. Brouwer - 1907 - Leipzig,: Maas & van Suchtelen.
Varieties of constructive mathematics.D. S. Bridges - 1987 - New York: Cambridge University Press. Edited by Fred Richman.
Intuitionism, an Introduction.A. Heyting - 1958 - Studia Logica 7:277-278.

View all 24 references / Add more references