School of Computing

Are subsets necessary in Martin-Lof type theory?

Simon Thompson

In J. P. Myers Jr. and M. J. O'Donnell, editors, Constructivity in Computer Science, volume 613 of Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, January 1992.

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.

Download publication 128 kbytes (PostScript)

Bibtex Record

@conference{202,
author = {Simon  Thompson},
title = {Are subsets necessary in {M}artin-{L}of type theory?},
month = {January},
year = {1992},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1992/202},
    ISBN = {3-540-55631-1},
    booktitle = {Constructivity in Computer Science},
    editor = {J. P. Myers Jr. and M. J. O'Donnell},
    publisher = {Springer-Verlag},
    refereed = {yes},
    series = {Lecture Notes in Computer Science},
    volume = {613},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014