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

doi:10.4204/EPTCS.76.9

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 journal › Conference article › peer-review

16 Scopus citations

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 language	English (US)
Pages (from-to)	112-162
Number of pages	51
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	76
DOIs	https://doi.org/10.4204/EPTCS.76.9
State	Published - Feb 11 2012
Externally published	Yes
Event	4th Workshop on Mathematically Structured Functional Programming, MSFP 2012 - Tallinn, Estonia Duration: Mar 25 2012 → …

ASJC Scopus subject areas

Software

Access to Document

10.4204/EPTCS.76.9

Cite this

@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",

note = "Publisher Copyright: {\textcopyright} Sj{\"o}berg et al.; 4th Workshop on Mathematically Structured Functional Programming, MSFP 2012 ; Conference date: 25-03-2012",

year = "2012",

month = feb,

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 - https://www.scopus.com/pages/publications/84893481542

UR - https://www.scopus.com/pages/publications/84893481542#tab=citedBy

U2 - 10.4204/EPTCS.76.9

DO - 10.4204/EPTCS.76.9

M3 - Conference article

AN - SCOPUS:84893481542

SN - 2075-2180

VL - 76

SP - 112

EP - 162

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 4th Workshop on Mathematically Structured Functional Programming, MSFP 2012

Y2 - 25 March 2012

ER -

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

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this