An Effectful Treatment of Dependent Types

Matthijs Vákár

We extend Levy's call-by-push-value (CBPV) analysis from simple to dependent type theory (DTT) in order to study the interaction between computational effects and dependent types.…