Polonsky, Andrew
Extensionality of lambda-*
Abstract
We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that in type theory the notion of extensional equality be identified with the logical equivalence relation defined by induction on type structure.
BibTeX - Entry
@InProceedings{polonsky:LIPIcs:2015:5499,
author = {Andrew Polonsky},
title = {{Extensionality of lambda-*}},
booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)},
pages = {221--250},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-88-0},
ISSN = {1868-8969},
year = {2015},
volume = {39},
editor = {Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5499},
URN = {urn:nbn:de:0030-drops-54995},
doi = {10.4230/LIPIcs.TYPES.2014.221},
annote = {Keywords: Extensionality, logical relations, type theory, lambda calculus, reflection}
}
|
Keywords: |
|
Extensionality, logical relations, type theory, lambda calculus, reflection |
|
Seminar: |
|
20th International Conference on Types for Proofs and Programs (TYPES 2014)
|
|
Issue date: |
|
2015 |
|
Date of publication: |
|
2015 |
2015
