Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems

Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems

We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. O...

Full description

Bibliographic Details
Main Authors: Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
Format: Article
Language:English
Published: Open Publishing Association 2012-02-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1202.2923v1
id doaj-377d50b72b4a4b8fa419a7776956326a
record_format Article
spelling doaj-377d50b72b4a4b8fa419a7776956326a2020-11-24T21:06:58ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-02-0176Proc. MSFP 201211216210.4204/EPTCS.76.9Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type SystemsVilhelm SjöbergChris CasinghinoKi Yung AhnNathan CollinsHarley D. Eades IIIPeng FuGarrin KimmellTim SheardAaron StumpStephanie WeirichWe present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. Our language design is strongly influenced by the choice of CBV evaluation, and by our novel treatment of propositional equality which has a heterogeneous, completely erased elimination form.http://arxiv.org/pdf/1202.2923v1
collection DOAJ
language English
format Article
sources DOAJ
author Vilhelm Sjöberg
Chris Casinghino
Ki Yung Ahn
Nathan Collins
Harley D. Eades III
Peng Fu
Garrin Kimmell
Tim Sheard
Aaron Stump
Stephanie Weirich
spellingShingle Vilhelm Sjöberg
Chris Casinghino
Ki Yung Ahn
Nathan Collins
Harley D. Eades III
Peng Fu
Garrin Kimmell
Tim Sheard
Aaron Stump
Stephanie Weirich
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Electronic Proceedings in Theoretical Computer Science
author_facet Vilhelm Sjöberg
Chris Casinghino
Ki Yung Ahn
Nathan Collins
Harley D. Eades III
Peng Fu
Garrin Kimmell
Tim Sheard
Aaron Stump
Stephanie Weirich
author_sort Vilhelm Sjöberg
title Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
title_short Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
title_full Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
title_fullStr Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
title_full_unstemmed Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
title_sort irrelevance, heterogeneous equality, and call-by-value dependent type systems
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2012-02-01
description We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must be careful to only erase terminating expressions. Our language design is strongly influenced by the choice of CBV evaluation, and by our novel treatment of propositional equality which has a heterogeneous, completely erased elimination form.
url http://arxiv.org/pdf/1202.2923v1
work_keys_str_mv AT vilhelmsjoberg irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT chriscasinghino irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT kiyungahn irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT nathancollins irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT harleydeadesiii irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT pengfu irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT garrinkimmell irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT timsheard irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT aaronstump irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
AT stephanieweirich irrelevanceheterogeneousequalityandcallbyvaluedependenttypesystems
_version_ 1716764110752841728

Similar Items