Irrelevance, heterogeneous equality, and call-by-value dependent type systems

Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D Eades, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich

Research output: Contribution to journalConference article

8 Citations (Scopus)

Abstract

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.

Original languageEnglish (US)
Pages (from-to)112-162
Number of pages51
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume76
DOIs
StatePublished - Feb 11 2012
Externally publishedYes
Event4th Workshop on Mathematically Structured Functional Programming, MSFP 2012 - Tallinn, Estonia
Duration: Mar 25 2012 → …

ASJC Scopus subject areas

  • Software

Cite this

Irrelevance, heterogeneous equality, and call-by-value dependent type systems. / Sjöberg, Vilhelm; Casinghino, Chris; Ahn, Ki Yung; Collins, Nathan; Eades, Harley D; Fu, Peng; Kimmell, Garrin; Sheard, Tim; Stump, Aaron; Weirich, Stephanie.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 76, 11.02.2012, p. 112-162.

Research output: Contribution to journalConference article

Sjöberg, V, Casinghino, C, Ahn, KY, Collins, N, Eades, HD, Fu, P, Kimmell, G, Sheard, T, Stump, A & Weirich, S 2012, 'Irrelevance, heterogeneous equality, and call-by-value dependent type systems', Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 76, pp. 112-162. https://doi.org/10.4204/EPTCS.76.9
Sjöberg, Vilhelm ; Casinghino, Chris ; Ahn, Ki Yung ; Collins, Nathan ; Eades, Harley D ; Fu, Peng ; Kimmell, Garrin ; Sheard, Tim ; Stump, Aaron ; Weirich, Stephanie. / Irrelevance, heterogeneous equality, and call-by-value dependent type systems. In: Electronic Proceedings in Theoretical Computer Science, EPTCS. 2012 ; Vol. 76. pp. 112-162.
@article{cd8f988ade194a0799a38eb262a75352,
title = "Irrelevance, heterogeneous equality, and call-by-value dependent type systems",
abstract = "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.",
author = "Vilhelm Sj{\"o}berg and Chris Casinghino and Ahn, {Ki Yung} and Nathan Collins and Eades, {Harley D} and Peng Fu and Garrin Kimmell and Tim Sheard and Aaron Stump and Stephanie Weirich",
year = "2012",
month = "2",
day = "11",
doi = "10.4204/EPTCS.76.9",
language = "English (US)",
volume = "76",
pages = "112--162",
journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Irrelevance, heterogeneous equality, and call-by-value dependent type systems

AU - Sjöberg, Vilhelm

AU - Casinghino, Chris

AU - Ahn, Ki Yung

AU - Collins, Nathan

AU - Eades, Harley D

AU - Fu, Peng

AU - Kimmell, Garrin

AU - Sheard, Tim

AU - Stump, Aaron

AU - Weirich, Stephanie

PY - 2012/2/11

Y1 - 2012/2/11

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84893481542&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84893481542&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.76.9

DO - 10.4204/EPTCS.76.9

M3 - Conference article

VL - 76

SP - 112

EP - 162

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

SN - 2075-2180

ER -