2016/03/14 by Matthijs Vákár, Vákár, Matthijs · 1 citation
Computer Science · #Advanced Database Systems and Queries #FOS: Computer and information sciences #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.1603.04298
openalex publication_date 2016/03/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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. We define the naive system of dependently typed CBPV, dCBPV-, and its extension with a principle of Kleisli extensions for dependent functions, dCBPV+. We investigate these systems from the points of view of syntax, categorical semantics, concrete models and operational semantics, in presence of a range of effects. We observe that, while the expressive power of dCBPV+ is needed if we want well-defined call-by-value (CBV) and call-by-name (CBN) translations of DTT, it is a less straightforward system than dCBPV-, in presence of some effects. Indeed, to be able to construct specific models and to retain the subject reduction property in the operational semantics, we are required to impose certain subtyping conditions, the idea being that the type of a computation may only become more (not less) specified as certain effects are executed.