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 (280kB)
Preview
|
|
|
|
Postscript
Language: English |
||
|
Download (131kB)
Preview
|
|
|
| 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: | Faculties > Sciences > School of Computing > Theoretical Computing Group |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 07 Aug 2009 22:15 UTC |
| Last Modified: | 23 Jan 2020 04:04 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/21078 (The current URI for this page, for reference purposes) |
| Thompson, Simon: |  https://orcid.org/0000-0002-2350-301X |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Altmetric
Altmetric