Are subsets necessary in Martin-Lof type theory?

Thompson, Simon (1992) Are subsets necessary in Martin-Lof type theory? In: Myers Jr, J.P. and O'Donnell, M.J., eds. Constructivity in Computer Science Summer Symposium. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 46-57. ISBN 978-3-540-55631-2. E-ISBN 978-3-540-47265-0. (doi:10.1007/BFb0021082) (KAR id:21078)

PDF Language: English
Download this file (PDF/178kB)	Preview
Request a format suitable for use with assistive technology e.g. a screenreader
Postscript Language: English
Download this file (Postscript/131kB)	Preview
Request a format suitable for use with assistive technology e.g. a screenreader
Official URL: http://dx.doi.org/10.1007/BFb0021082

Abstract

After introducing Martin-Lof's type theory, the paper introduces the rules proposed by various authors for adding subset types to the system, and the justification given for their addition. These justifications are examined, and it is argued that by a combination of lazy evaluation and transformation using the Axiom of Choice that subsets need not be added to the system to make it usable.

Item Type:	Book section
DOI/Identification number:	10.1007/BFb0021082
Additional information:	Document Type: Proceedings Paper Conference Information: 1991 SUMMER SYMP ON CONSTRUCTIVITY IN COMPUTER SCIENCE
Uncontrolled keywords:	constructivity Martin-Lof computational irrelevance subsets
Subjects:	Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions:	Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User:	Mark Wheadon
Date Deposited:	07 Aug 2009 22:15 UTC
Last Modified:	05 Nov 2024 09:58 UTC
Resource URI:	https://kar.kent.ac.uk/id/eprint/21078 (The current URI for this page, for reference purposes)

University of Kent Author Information

Thompson, Simon.

Creator's ORCID:	https://orcid.org/0000-0002-2350-301X
CReDIT Contributor Roles:

Depositors only (login required):

Altmetric

Download Statistics

Total unique views for this document in KAR since July 2020. For more details click on the image.