uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Reference and Computation in Intuitionistic Type Theory
Uppsala University, Teknisk-naturvetenskapliga vetenskapsområdet, Mathematics and Computer Science, Department of Mathematics.
2008 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Three topics, namely, computer science, philosophical logic, and mathematics, meet in intuitionistic type theory, which thus simultaneously is a programming language, a philosophy of language, and a foundation of mathematics. The present thesis compares, relates, and equates two concepts, one from philosophical logic and one from computer science, viz., reference and computation. In mathematical practice, we are used to viewing mathematical expressions as referring to their value or object, as 2 + 2 refers to 4: it is the responsibility of the foundations of mathematics to explain exactly what these objects are and how the expressions refer to them.

The nature of mathematics, and related issues, such as reference and computation, have been debated a long time, in particular around the turn of the last century. The position defended in this thesis is that intuitionism, i.e., the philosophy behind intuitionistic type theory, provides a satisfactory answer to these questions, with the additional benefit of increasing the applicability of mathematics. Of course, these benefits do not come for free: some modern mathematical practices have to be given up, most notably the nonconstructive existence proofs.

In addition to critical discussions of the topics mentioned above, the main contributions of this thesis are that computations are brought into the language of intuitionistic type theory, and that intuitionistic type theory is adopted to eager evaluation. The latter contribution is of particular importance in computer science.

Place, publisher, year, edition, pages
Uppsala: Universitetsbiblioteket , 2008. , 234 p.
Uppsala Dissertations in Mathematics, ISSN 1401-2049 ; 60
Keyword [en]
mathematical logic, intuitionism, type theory, foundations of mathematics
URN: urn:nbn:se:uu:diva-9522ISBN: 978-91-506-2042-9OAI: oai:DiVA.org:uu-9522DiVA: diva2:173104
Public defence
2009-01-16, Polhemsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 13:15
Available from: 2008-12-19 Created: 2008-12-19Bibliographically approved

Open Access in DiVA

No full text

By organisation
Department of Mathematics

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 835 hits
ReferencesLink to record
Permanent link

Direct link