64 citations · 157 across the 11 of their papers we have counts for
Showing 2015Show all
3 papers · 1 filter
cs.LO2015★ 8 cited
A Framework for Dependent Types and Effects
Matthijs Vákár
We generalise Levy's call-by-push-value (CBPV) to dependent type theory, to gain a better understanding of how to combine dependent types with effects. We define a dependently type…
cs.LO2015★ 1 cited
Games for Dependent Types
Samson Abramsky, Radha Jagadeesan, Matthijs Vákár
We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and intensional Id-types, which is based on a slight variation of the category of AJM-games and history-free…
cs.LO2015
A Categorical Semantics for Linear Logical Frameworks
Matthijs Vákár
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear lo…