17 citations · 23 across the 2 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2022★ 6 cited
Program Adverbs and Tlön Embeddings
Yao Li, Stephanie Weirich
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support…
cs.PL2012★ 17 cited
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn +7
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 studi…