An Effectful Treatment of Dependent Types∗
Matthijs Vákár1
1

University of Oxford, Dept. Computer Science, matthijs.vakar@cs.ox.ac.uk

arXiv:1603.04298v1 [] 14 Mar 2016

Abstract
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.
1998 ACM Subject Classification F.3.2 Semantics of Programming Languages
Keywords and phrases Dependent types, effects, call-by-push-value, linear dependent types
Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

1

Introduction

Dependent types [1] are slowly being taking up by the functional programming community and
are in the transition from a quirky academic hobby to a practical approach to building certified
software. Purely functional dependently typed languages like Coq [2] and Agda [3] have
existed for a long time. If the technology is to become more widely used in practice, however,
it is crucial that dependent types can be smoothly combined with the wide range of effects
that programmers make use of in their day to day work, like non-termination and recursion,
mutable state, input and output, non-determinism, probability and non-local control.
Although some languages exist which combine dependent types and effects, like Cayenne
[4], ΠΣ [5], Zombie [6], Idris [7], Dependent ML [8] and F? [9], there have always been
some strict limitations. For instance, the first four only combine dependent types with first
class recursion (although Idris has good support for emulating other effects), Dependent ML
constrains types to depend only on static natural numbers and F? does not allow types to
depend on effectful terms at all (including non-termination). Somewhat different is Hoare
Type Theory (HTT) [10], which defines a programming language for writing effectful programs
as well as a separation logic encoded in a system of dependent types for reasoning about these
programs. We note that the programming fragment is not merely an extension of the logical
one, which would be the elegant solution suggested by the Curry-Howard correspondence.
The sentiment of most papers discussing the marriage of these ideas seems to be that
dependent types and effects form a difficult though not impossible combination. However, as
far as we are aware, treatment has so far been on a case-by-case basis and no general theoretical
analysis has been given which discusses, on a conceptual level, the possibilities, difficulties
and impossibilities of combining general computational effects and dependent types.
∗

Data types, that is. The applicability of the results of this paper to the care of individuals with a
dependent personality disorder may be rather limited.

© Matthijs Vákár;
licensed under Creative Commons License CC-BY
Conference title on which this volume is based on.
Editors: Billy Editor and Bill Editors; pp. 1–15
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

2

An Effectful Treatment of Dependent Types

In a somewhat different vein, there has long been an interest in combining linearity and
dependent types. This was first done in Cervesato and Pfenning’s LLF [11]. Recently, a
semantic analysis of LLF was given by the author in [12, 13] which has proved important e.g.
in the development of a game semantics for dependent types. One aspect that this abstract
semantics as well as the study of particular models highlight is - more so than in the simply
typed case - the added insight and flexibility obtained by decomposing the !-comonad into
an adjunction1 . This corresponds to working with dependently typed version of Benton’s
LNL-calculus [14] rather than Barber and Plotkin’s DILL [15], as was done in [16].
Similarly, it has proved problematic to give a dependently typed version of Moggi’s
monadic metalanguage [17]. We hope that this paper illustrates that also in this case a
decomposed adjunction perspective, like that of CBPV [18], is more flexible than a monadic
perspective. Recall from [19] that if we decompose both linear logic and the monadic
metalanguage into an adjunction, we can see the former to be a restricted case of the latter
which only describes (certain) commutative effects.
In this paper, we show that the analysis of linear DTT of [13, 16, 12] generalises straightforwardly to general (non-commutative) effects to give a dependently typed CBPV calculus that
we call dCBPV-, which allows types to depend on values (including thunks of computations)
but which lacks a Kleisli extension (or sequencing) principle for dependent functions. This
calculus is closely related to Harper and Licata’s dependently typed polarized intuitionistic
logic [20]. Its categorical semantics is obtained from that for linear dependent types, by
relaxing a condition on the adjunction which would normally imply, among other things, the
commutativity of the effects described. It straightforwardly generalises Levy’s adjunction
models for CBPV [21] (from locally indexed categories to more general comprehension categories [22]) and, in a way, simplifies Moggi’s strong monad models for the monadic metalanguage
[17], as was already anticipated by Plotkin in the late 80s: in a dependently typed setting
the monad strength follows straightforwardly from the natural demand that its adjunction
is compatible with substitution and, similarly, the distributivity of coproducts follows from
their compatibility with substitution. In fact, we believe the categorical semantics of CBPV
is most naturally understood as a special case of a that of dCBPV-. Particular examples of
models are given by models of linear DTT and by Eilenberg-Moore adjunctions for strict2
indexed monads on models of pure DTT. The small-step operational semantics for CBPV of
[18] transfers to dCBPV- without any difficulties with the expected subject reduction and
(depending on the effects considered) strong normalization and determinacy results.
When formulating candidate CBV- and CBN-translations of DTT into dCBPV-, it
becomes apparent that the latter is only well-defined if we work with the weak (non-dependent)
elimination rules for positive connectives, while the former is ill-defined altogether. To obtain
a CBV-translation and the CBN-translation in all its glory, we have to add a principle of
Kleisli extensions (or sequencing) for dependent functions to dCBPV-. We call the resulting
calculus dCBPV+, to which we can easily extend our categorical and operational semantics.
Normalization and determinacy results for the operational semantics remain the same.
However, depending on the effects we consider, we may need to add extra coercion rules to
the calculus to salvage subject reduction. These embody the idea that a computation can only
obtain a more (not less) precise type after certain effects, like non-deterministic branching,

1
2

Indeed, connectives seem to be most naturally formulated one either the linear or cartesian side: Σ- and
Id-constructors operate on cartesian types while Π-constructors operate on linear types.
For brevity, from now on we shall drop the modifier "strict" for indexed structures. For instance, if we
mention an indexed honey badger, we shall really mean a strict indexed honey badger.

M. Vákár

are executed. We analyse on a case-by-case basis the principle of dependent Kleisli extensions
in dCBPV- models of a range of effects. This leads us to the same subtyping conditions.
Before concluding, we discuss of the possibility of adding some additional connectives. In
particular, we address the matter of a dependently typed enriched effect calculus (EEC) [23].
One the one hand, we hope this analysis gives a helpful theoretical framework in which we
can study various combinations of dependent types and effects from an algebraic, denotational
and operational point of view. It gives a robust motivation for the equations we should
expect to hold in both CBV- and CBN-versions of effectful DTT, through their translations
into dCBPV, and it guides us in modelling dependent types in effectful settings like game
semantics. Moreover, it explains why combinations of dependent types and effects are slightly
more straightforward in CBN than in CBV, as dependent Kleisli extensions are not required.
On the other, noting that not all effects correspond to sound logical principles, an expressive system like CBPV or a monadic language, with fine control over where effects occur, is an
excellent combination with dependent types as it allows us to use the language both for
writing effectful programs and pure logical proofs about these programs. Similar to HTT in
aim, but different in implementation, we hope that dCBPV can be expanded in future to an
elegant language, serving both for writing effectful programs and for reasoning about them.

2

A Very Brief Recap of Simple Call-by-Push-Value

We briefly recall the spirit of Levy’s CBPV analysis of simple type theory [18, 24, 21]. The
long version of this paper [25] includes a detailed exposition, aimed at generalising smoothly
to dependent types. CBPV roughly gives an adjunction decomposition of Moggi’s monadic
metalanguage [17]. This allows one to not only fully and faithfully encode Moggi’s metalanguage and with that CBV λ-calculi, but also CBN ones. CBPV has a natural small-step
operational semantics, satisfying subject reduction and, depending on the effects considered,
determinism at each step and strong normalization. For terms of ground type, this reproduces
the usual CBV and CBN operational semantics in presence of a wide range of effects.
CBPV makes a clear distinction between the worlds of value types (inhabited by values)
and computation types (the home of stacks and, in particular, computations), between which
we have an adjunction of half-modalities F a U , which yield as special cases Moggi’s modality
T = U F and the linear logic exponential ! = F U . F A can be read as the type of computations
that can return values of type A and U B as the type of thunks of computations of type B.
By only including positive type formers like inductive types on value types and negative ones
like coinductive types on computation types, one is able to retain the entire βη-equational
theory even in the presence of effects. As a consequence, we obtain an elegant categorical
semantics in terms of adjunctions of locally indexed categories.

3

A Syntax for Dependently Typed Call-by-Push-Value (dCBPV)

We generalise CBPV, allowing types to depend on values, but not computations (cf. linear [11]
or polarised [20] DTT, where types can only depend on cartesian or positive terms, respectively). dCBPV makes the following judgements: well-formedness of contexts ` Γ; ∆ ctxt,
where Γ is a list of distinct identifier declarations of value types and ∆ is a list of declarations of
computation type (writing · for the empty list and Γ as a shorthand for Γ; ·), well-formedness
of value types Γ ` A vtype and computation types Γ ` B ctype (sometimes underlined to be
explicit), typing of values Γ `v V : A, computations Γ `c M : B and stacks Γ; ∆ `k K : B,
equality judgements for contexts, types (in context) and (typed) terms (in context).
As types can depend on terms in a dependently typed system, we define both in one
inductive definition. A discussion of the syntactic subtleties of DTT can be found in [1].

3

4

An Effectful Treatment of Dependent Types

To start with, we have rules, which we shall not list, stating that all judgemental
equalities are equivalence relations and that all term, type and context constructors as well as
substitutions respect judgemental equality. In similar vein, we have conversion rules, stating
that we may swap contexts and types for judgementally equal ones in all judgements. To
form contexts, we have the rules of figure 1 and, to form types, those of figure 2.
` Γ; · ctxt
Γ ` B ctype
` Γ; B ctxt

` Γ; ∆ ctxt
Γ ` A vtype
` Γ, x : A; ∆ ctxt

·; · ctxt

Figure 1 Rules for contexts of dCBPV, where x is assumed to be a fresh identifier.
Γ, x : A, Γ0 ` A0 vtype
Γ `v V : A
Γ, Γ0 [V /x] ` A0 [V /x] vtype

Γ ` B ctype
Γ ` U B vtype

Γ `v V : A
Γ `v V 0 : A
0
Γ ` IdA (V, V ) vtype

` Γ ctxt
Γ ` 1 vtype

{Γ ` Ai vtype}1≤i≤n
Γ ` Σ1≤i≤n Ai vtype

Γ, x : A ` A0 vtype
Γ ` Σx:A A0 vtype

Γ, x : A, Γ0 ` B ctype

Γ ` A vtype
Γ ` F A ctype

{Γ ` Bi ctype}1≤i≤n

Γ, x : A ` B ctype
Γ ` Πx:A B ctype

Γ `v V : A

Γ, Γ0 [V /x] ` B[V /x] ctype

Γ ` Π1≤i≤n Bi ctype

Figure 2 Rules for forming the types of dCBPV.

For these types, we consider the values and computations formed using the rules of figure 3,
to which we could add the obvious admissible weakening and exchange rules.
` Γ, x : A, Γ0 ctxt
Γ, x : A, Γ0 `v x : A

Γ, x : A, Γ0 `v/c R : B

Γ `v V : A
0

Γ, Γ [V /x] `

Γ, z : U F A, Γ0 ` B ctype
0

Γ `c M : F A

v/c

let x be V in R : B[V /x]

Γ, x : A, Γ0 [tr x/z] `c N : B[tr x/z]

c

Γ, Γ [thunk M/z] ` M to x in N : B[thunk M/z].
Γ `c M : B
Γ ` thunk M : U B
v

Γ `v V : U B
Γ `c force V : B

Γ `v V : 1

` Γ ctxt
Γ `v hi : 1

Γ`

Γ `v Vi : Ai
Γ ` hi, Vi i : Σ1≤i≤n Ai

Γ `v V : Σ1≤i≤n Ai

Γ `v V1 : A1
Γ `v V2 : A2 [V1 /x]
Γ `v hV1 , V2 i : Σx:A1 A2

Γ `v V : Σx:A1 A2

Γ `v V : A
Γ `v refl V : IdA (V, V )

Γ `v V : IdA (V1 , V2 )

v

v/c

Γ `v/c R : B[hi/z]

pm V as hi in R : B[V /z]

{Γ, x : Ai `v/c Ri : B[hi, xi/z]}1≤i≤n

Γ `v/c pm V as hi, xi in Ri : B[V /z]

v/c

Γ`

v/c

Γ`

{Γ `c Mi : Bi }1≤i≤n

Γ `c M : Π1≤i≤n Bi

Γ `c λi Mi : Π1≤i≤n Bi

Γ `c i‘M : Bi

Γ, x : A1 , y : A2 `v/c R : B[hx, yi/z]
pm V as hx, yi in R : B[V /z]
Γ, x : A `v/c R : B[x/x0 , refl x/p]

pm V as (refl x) in R : B[V1 /x, V2 /x0 , V /p]

Γ, x : A `c M : B
Γ `c λx M : Πx:A B

Γ `v V : A
Γ `c M : Πx:A B
Γ `c V ‘M : B[V /x]

Figure 3 Values and computations of dCBPV+. Those of dCBPV- are obtained by demanding
the side condition that z is not free in Γ0 ; B in the rule for forming M to x in N . A rule involving
`v/c is a shorthand for two rules: one with `v and one with `c in both the hypothesis and conclusion.
Indices i are a slight abuse of notation: e.g. λi Mi is an abbreviation for λ(1,...,n) (M1 , . . . , Mn ).

As anticipated by Levy [18], the only rule that requires care is that for forming a sequenced
computation M to x in N . He suggested that z should not be free in the context Γ0 ; B. We
call the resulting system with this restriction dCBPV- and the more permissive system where
we drop this restriction and allow Kleisli extensions of dependent functions dCBPV+. We
leave the discussion of stacks until section 6.

M. Vákár

5

We generate judgemental equalities for values and computations through the rules of
figure 4. Note that we are using extensional Id-types, in the sense of Id-types with an η-rule.
This is only done for the aesthetics of the categorical semantics. They may not be suitable for
an implementation, however, as they make type checking undecidable for the usual reasons
[1]. The syntax and semantics can just as easily be adapted to intensional Id-types, the
obvious choice to for an implementation.
(return V ) to x in M = M [V /x]
force thunk M = M

M = M to x in return x
V = thunk force V

pm hi, V i as hi, xi in Ri = Ri [V /x]
pm hi as hi in R = R

R[V /z] = pm V as hi, xi in R[hi, xi/z]
R[V /z] = pm V as hi in R[hi/z]

pm hV, V 0 i as hx, yi in R = R[V /x, V 0 /y]

R[V /z] = pm V as hx, yi in R[hx, yi/z]

pm (refl V ) as (refl x) in R = R[V /x]
i‘λj Mj = Mi

R[V1 /x, V2 /y, V /z] = pm V as (refl w) in R[w/x, w/y, (refl w)/z]
M = λi i‘M

V ‘λx M = M [V /x]

M = λx x‘M

let x be V in R = R[V /x]

(M to x in N ) to y in N 0 = M to x in (N to y in N 0 )

M to x in λi Ni = λi (M to x in Ni )

#x

#x,y

#w

#x

#x

#y

M to x in λy N = λy (M to x in N )

Figure 4 Equations of dCBPV. These should be read as equations of typed terms: we impose
them if we can derive that both sides of the equation are terms of the same type (in context). We
#x1 ,...,xn

write
=
to indicate that for the equation to hold, the identifiers x1 , . . . , xn should, in both
terms being equated, be replaced by fresh identifiers, in order to avoid unwanted variable bindings.

Figures 5 and 6 show the natural candidate CBV- and CBN-translations of DTT with
some of the usual connectives into dCBPV: we treat sums, projection products, pattern
matching dependent products and unit types, dependent function types and identity types.
We can define the translations for projection dependent products as we have for their simple
relatives, if we add projection dependent products to dCBPV as is sketched in section 8.
It turns out that without Kleisli extensions for dependent functions, the CBV-translation
is not well-defined as it results in untypable terms. The CBN-translation is, but only
if we restrict to the weak (non-dependent) elimination rules for Σ1≤i≤n -, 1-, Σ- and Idtypes, meaning that the type we are eliminating into does not depend on the type being
eliminated from. One would expect the CBV-translation to factorise as a translation into
a dependently typed version of Moggi’s monadic metalanguage without dependent Kleisli
extensions, followed by a translation of this into dCBPV-. While the latter is definable, the
former is ill-defined3 . Perhaps this is a (partial) explanation of why all (CBV) dependently
typed languages with effects have encapsulated the effects in a monad. The exceptions are
non-termination and recursion. As we shall see in section 6, dependent Kleisli extensions are
straightforward in that case without imposing subtyping conditions, which means we can
treat these as a first class effects and do not have to encapsulate them in a monad.
It seems likely that one could obtain soundness and completeness results for these
translations with respect to the correct equational theories for CBV- and CBN-DTT. As
we are not aware of any such equational theories being described in literature, we propose
to define these through their translations into dCBPV. Both translations might result in a
broken η-law for Id-types, in presence of effects, even if we assume one in dCBPV.

3

Although, this may remind the reader of the situation of dependently typed dual intuitionistic linear
logic (a comonadic language), where the Girard translation (essentially the CBN-translation) from DTT
fails, we appear to be observing a qualitatively different phenomenon rather than a mere mirror image.

6

An Effectful Treatment of Dependent Types

CBV type
Γ ` A type

CBPV type
U F Γv ` Av vtype

Σ1≤i≤n Ai

Σ1≤i≤n Avi

Π1≤i≤n Ai

U Π1≤i≤n F Avi

Πx:A A0

U (Πx:Av F A0v [tr x/z])

1

1

Σx:A A0

Σx:Av A0v [tr x/z]

IdA (M, N )

IdU F Av (thunk M v ,
thunk N v )

CBV term
x1 : A1 , . . . , xm : Am
`M :A
x
let x be M in N
hi, M i
pm M as hi, xi in Ni
λi Mi
i‘N
λx M
M ‘N
hi
pm M as hi in N
hM, N i
pm M as hx, yi in N
refl M
pm M as (refl x) in N

CBPV term
x1 : Av1 , . . . , xm : Avm [. . . tr xi /zi . . .]
`c M v : F (Av [tr x1 /z1 , . . . , tr xn /zn ])
return x
M v to x in N v
M v to x in return hi, xi
M v to z in (pm z as hi, xi in Niv )
return thunk (λi Miv )
N v to z in (i‘force z)
return thunk λx M v
M v to x in (N v to z in (x‘force z))
return hi
M v to z in (pm z as hi in N v )
M v to x in (N v to y in return hx, yi)
M v to z in (pm z as hx, yi in N v )
M v to z in return refl tr z
M v to z in (pm z as (refl y) in
(force y to x in N v ))

Figure 5 A translation of dependently typed CBV into dCBPV. We write tr as an abbreviation
for thunk return and U F Γ := z1 : U F A1 , . . . , zn : U F An for a context Γ = x1 : A1 , . . . , xn : An .
CBN type
Γ ` B type

CBPV type
U Γn ` B n ctype

Σ1≤i≤n B i

F Σ1≤i≤n U B n
i

Π1≤i≤n B i

Π1≤i≤n B n
i

Πx:B B 0

Πx:U B n B 0

1

F1

Σx:B B 0

F (Σx:U B n U B 0 )

IdB (M, M 0 )

F (IdU B (thunk M n ,
thunk M 0n ))

n

n

CBN term
x1 : B 1 , . . . , x m : B m ` M : B
x
let x be M in N
hi, M i
pm M as hi, xi in Ni
λ i Mi
i‘M
λx M
N ‘M
hi
pm M as hi in N
hM, N i
pm M as hx, yi in N
refl M
pm M as (refl x) in N

CBPV term
n
c
n
n
x1 : U B n
1 , . . . , xm : U B m ` M : B
force x
let x be (thunk M n ) in N n
return hi, thunk M n i
M n to z in (pm z as hi, xi in Nin )
λi Min
i‘M n
λx M n
(thunk N n )‘M n
return hi
M n to z in (pm z as hi in N n )
return hthunk M n , thunk N n i
M n to z in (pm z as hx, yi in N n )
return refl thunk M n
M n to z in (pm z as (refl x) in N n )

Figure 6 A translation of dependently typed CBN into dCBPV. We write U Γ := x1 :
U A1 , . . . , xn : U An for a context Γ = x1 : A1 , . . . , xn : An .

4

Abstract Categorical Semantics

We have reached the point in the story that was our initial motivation to study dCBPV: its
very natural categorical semantics. To formulate our dCBPV models, we recall the notion of
an indexed category with full and faithful democratic comprehension, which is equivalent to
Jacobs’ notion of a split full democratic comprehension category with unit [22].
C

I Definition 1 (Comprehension Axiom). Let B op −→ Cat be an indexed category (a functor
f

to the category Cat of small categories). Given B 0 −→ B in B, let us write the change of
base functor C(B) −→ C(B 0 ) as −{f }. Recall that C satisfies the comprehension axiom if
B has a terminal object · and all fibres C(B) have terminal objects 1B that are stable
under change of base;

M. Vákár

7

f
the presheaves (B 0 −→ B) - C(B 0 )(1, C{f }) on B/B are representable: we have rephf,−i

pB,C

resenting objects B.C −→ B and natural bijections C(B 0 )(1, C{f }) −→ B/B(f, pB,C ).
Write vB,C for the (universal) element of C(B.C)(1, C{pB,C }) corresponding to idpB,C . Define
B.C

diagB,C := hidB.C , vB,C i

C(B)(C 0 , C)

pB,−

}i
- B.C.C{pB,C }, B 0 .C{f } qf,C := hpB ,C{f } ; f, vB ,C{fB.C and
:= hpB,C 0 , vB,C 0 ; −{pB,C 0}i
B/B(pB,C 0 , pB,C ). When these last maps pB,−
0

0

are full and faithful for all B, we call the comprehension full and faithful, respectively. When
∼ B, we call it democratic.
the comprehension induces an equivalence C(·) =
I Definition 2 (dCBPV- Model). By a dCBPV- model, we shall mean the following data.
C
An indexed category B op −→ Cat with full and faithful democratic comprehension;
D
An indexed category B op −→ Cat;
An indexed adjunction F a U : D  C (adjunctions compatible with change of base);
Π-types in D: right adjoints −{pA,B } a ΠB : D(A.B)  D(A) satisfying the right
Beck-Chevalley condition (a technical condition, compatibility with substitution [22]);
Finite products (Π1≤i≤n Di ) in the fibres of D, stable under change of base;
Σ-types in C: objects ΣC D of C(B) such that pB,ΣC D = pB.C,D ; pB,C ;
Id-types in C: objects IdC of C(B.C.C) such that pB.C.C,IdC = diagB,C ;
0, +-types in C: finite coproducts (Σ1≤i≤n Ci ) in the fibres of C, stable under change of
base, such that the following canonical morphisms are bijections, for E ∈ {C, D},
E(C.Σ1≤i≤n Ci )(X, Y ) −→ Π1≤i≤n E(C.Ci )(X{pC,hi,idCi i }, Y {pC,hi,idCi i });
I Definition 3 (dCBPV+ Model). By a dCBPV+ model, we mean a dCBPV- model with
(−)∗

specified maps C(Γ.A.Γ0 {pΓ,ηA })(1, U B{qpΓ,ηA ,Γ0 }) −→ C(Γ.U F A.Γ0 )(1, U B), called dependent Kleisli extensions, where η is the unit of F a U , such that (−)∗ agrees with the usual
Kleisli extensions of F a U and is compatible with η and −{−} in the obvious sense.
I Remark. Note that, for both notion of model, we retrieve (up to equivalence) Levy’s
adjunction models for CBPV if we restrict to C = self(B), where self(B)(B)(B 0 , B 00 ) := B(B ×
B 0 , B 00 ), and D that are locally B-indexed in the sense that change of base is the identity on
objects and we drop the requirement of identity types (which then corresponds to objects 1/B
such that 1/B × B ∼
= 1). In particular, stability of the adjunction under change of base then
implies the strength of the monad T = U F and stability of coproducts becomes distributivity.
sA,B
More generally, in a dCBPV- model, we can define a strength ΣA T B −→ T ΣA B, while a
s0A,B

tA,B

costrength ΣT A B −→ T ΣA T B{pΓ,ηA } (hence a pairing ΣT A T B −→ T ΣA B{pΓ,ηA }) can
only be defined in dCBPV+ models.
This semantics is sound and complete.
I Theorem 4 (dCBPV Semantics). We have a sound interpretation of dCBPV- in a dCBPVmodel and of dCBPV+ in a dCBPV+ model, where we also give the interpretation of the
stack judgement of section 6 (together with the obvious interpretation of terms, e.g. interpreting M to x in N using Kleisli extensions, which we leave to the imagination of the reader):
[[·]] = ·
[[Γ, x : A]] = [[Γ]].[[A]]
[[Γ `v A]] = C([[Γ]])(1, [[A]])
[[Γ `c B]] = D([[Γ]])(F 1, [[B]])
[[Γ; B `k C]] = D([[Γ]])([[B]], [[C]])

[[A[V /x]]] = [[A]]{hhid[[Γ]] , [[V ]]i, id[[Γ0 [V /x]]] i}
[[B[V /x]]] = [[B]]{hhid[[Γ]] , [[V ]]i, id[[Γ0 [V /x]]] i}
[[IdA (V, V 0 )]] = Id[[A]] {hhid[[Γ]] , [[V ]]i, [[V 0 ]]i}
[[Σ1≤i≤n Ai ]] = Σ1≤i≤n [[Ai ]]
[[Σx:A A0 ]] = Σ[[A]] [[A0 ]]

[[1]] = 1
[[Π1≤i≤n B i ]] = Π1≤i≤n [[B i ]]
[[Πx:A B]] = Π[[A]] [[B]]
[[F A]] = F [[A]]
[[U B]] = U [[B]].

The interpretations in such categories are complete: an equality of values or computations holds in all interpretations iff it is provable in the syntax of dCBPV. In fact, if we add
the obvious (admissible) weakening and exchange rules to dCBPV, the interpretation defines

8

An Effectful Treatment of Dependent Types

an onto correspondence between categorical models and syntactic theories in dCBPV which
satisfy mutual soundness and completeness results. This correspondence becomes 1-1 and we
obtain completeness for the stack judgement if we include complex stacks.
Proof (sketch). The proof goes almost entirely along the lines of the soundness and completeness proofs for linear DTT in [12]. For completeness result, we build a syntactic category,
after conservatively extending our syntax with complex stacks as in [21].
J

5

Concrete Models

We can first note that if we restrict to the identity adjunction, both dCBPV- and dCBPV+
reduce to a reformulation of Jacobs’ notion of a full split democratic comprehension category
with Σ-, Σ1≤i≤n -, Π- and extensional Id-types, which is a standard notion of model of pure
DTT [22]. An example is the usual families of sets model Fam(Set) of pure DTT. (Recall
that Fam(Set) is defined as the restriction to Setop ⊆ Catop of the Cat-enriched hom-functor
into Set.) In particular, this shows consistency of the calculi.
I Theorem 5. Both dCBPV- and dCBPV+ are consistent.
More interestingly, any model of linear DTT supporting the appropriate connectives [12, 13]
gives rise to a model of dCBPV-, modelling commutative effects.
I Theorem 6. The notion of a model given by [12] for the dependently typed linear-nonlinear logic of [16] with the additional connectives of finite additive disjunctions is precisely a
dCBPV- model such that we have symmetric monoidal closed structures on the fibres of D,
stable under change of base, s.t. F consists of strong monoidal functors (sending nullary and
binary products in C to I and ⊗ in D) and which supports Σ⊗
F − -types (see section 8).
By analogy with the simply typed case, models of DTT on which we have an indexed monad
are again a source of dCBPV- models (indexing of the monad corresponding to a strength).
C

I Theorem 7. Let B op −→ Cat be a model of pure DTT (as above) on which we have an
indexed monad T (a family of monads, stable under change of base). Then, the indexed
Eilenberg-Moore adjunction C  C T gives a model of dCBPV-.
Proof (sketch). As in the simply typed setting, a product of algebras is just the product of
their carriers equipped with the obvious algebra structure. Indeed, it is a basic fact from
category theory that the forgetful functor from the Eilenberg-Moore category creates limits.
k
Given an object T B −→ B of C T (Γ.A), we note that we also obtain a canonical T -algebra
structure on Π-types of carriers (starting from the identity on ΠA B), our definition of ΠA k:
T

C(Γ)(ΠA B, ΠA B) ∼
= C(Γ.A)((ΠA B){pΓ,A }, B) −→ C(Γ.A)(T ((ΠA B){pΓ,A }), T B)
−;k
∼
= C(Γ.A)((T ΠA B){pΓ,A }, T B) −→ C(Γ.A)((T ΠA B){pΓ,A }, B) ∼
= C(Γ)(T ΠA B, ΠA B).

We leave the verification of the T -algebra axioms to the reader.

J

A concrete example to which we can apply the previous theorem is obtained for any
monad T on Set. Indeed, we can lift T (pointwise) to an indexed monad on Fam(Set). In
a different vein, given a model C of pure DTT, the usual exception, global state, reader,
writer and continuation monads (which we form using objects of C(·)) give rise to indexed
monads, hence we obtain models of dCBPV-. More exotic examples are the many indexed
monads that arise from homotopy type theory, like truncation and cohesion (shape and sharp)

M. Vákár

modalities [26, 27, 28]. A caveat there is that the identity types are intensional and that
many equations are often only assumed up to propositional rather than judgemental equality.
Models of dCBPV+ are harder to come by. Not every dCBPV- model generated by
theorem 7 admits dependent Kleisli extensions. Their existence needs to be assessed on a
case-by-case basis. Moreover, one indexed monad might be given dependent Kleisli extensions
in several inequivalent ways. Therefore, we treat some dCBPV- models for common effects
and discuss the (im)possibility of dependent Kleisli extensions.
Fortunately, the exceptions (and divergence) monads (−) + E on Set admit dependent
Kleisli extensions, hence give rise to models of dCBPV+. Indeed, for a dependent function
f ∈ Πa∈A B(a) + E, we can define f ∗ ∈ Πx∈A+E B(x) + E by setting f ∗ (a) := f (a) for a ∈ A
and else f ∗ (e) := e. (Generally, it suffices to give dependent Kleisli extensions for B = F A0 .)
Similarly, the domain semantics of DTT with recursion of [29] yields a model of dCBPV+
with intensional Id-types. C is defined to be an indexed category of continuous families of
Scott predomains (disjoint unions of Scott domains) with continuous functions. Σ-types
are interpreted as the usual set theoretic way and are endowed with the product order,
Σ1≤i≤n -types are disjoint unions and IdA (x, y) := {z ∈ A | z ≤ x, y} with the induced order
from A. D is defined to be the indexed category over the category of Scott predomains of
continuous families of Scott domains with strict continuous functions. U is defined to be
the usual inclusion, while F is the lift. ΠA B is defined to be the set of continuous sections
pA,U B
of ΣA U B −→ A with the pointwise order. We note that for f ∈ ΠA U B, we can define
f ∗ (a) := f (a) for a ∈ A and f ∗ (⊥) = ⊥.
By contrast, a non-trivial writer monad M × − (for a monoid M ) on Set does not admit
dependent Kleisli extensions. Indeed, we could take B to be a predicate on M × A such that
B(1M , a) = {∗} and otherwise B(m, a) = ∅ (which expresses that nothing is being written).
∗ ∈ Πa∈A B(1m , a) does not have a dependent Kleisli extension unless A = ∅.
Similarly, a non-trivial reader monad (−)S on Set does not admit dependent Kleisli
extensions. Indeed, we can define predicates B to specify that all s ∈ S yield the same value.
An analogous argument applies to non-trivial global state monads (S × −)S on Set.
−
For a continuation monad R(R ) on Set, one would hope to define dependent Kleisli
B(eva )
)
extensions for f ∈ Πa∈A R(R
as f ∗ (t)(k) := t(λa f (a)(k)). However, this is only wellB(c,t)
defined if we have ∀a∈A(c) R
⊆ RB(c,eva ) . In particular, we would have that B(c, evA ) =
0
B(c, evA0 ) for all a, a ∈ A(c).
Somewhat dubiously, we can define dependent Kleisli extensions for the erratic choice
S
monad P on Set as f ∗ (t) := ( a∈t f (a)) ∩ B(t), for f ∈ Πa∈A PB(a). This might not
correspond to the desired operational behaviour: indeed, non-deterministic branching is not
accumulated if it contradicts typing.
Many of the non-examples above of dCBPV+ models, could be mended by restricting
the class of predicates we consider, which would involve passing to a less simplistic model of
dependent types than mere families of sets. For example, for the writer monad, we want to
demand for types B depending on M × A the inclusion B(1M , a) ⊆ B(m, a). We will see this
idea reflected in the subject reduction property of the operational semantics of dCBPV+.

6

Operational Semantics

Importantly, CBPV admits a natural operational semantics that, for ground terms, reproduces
the usual operational semantics of CBV and CBN under the specified translations into CBPV
[18]. This can easily be extended to dCBPV.
We define the operational semantics on dCBPV terms not involving complex values which
unnecessarily complicate the presentation of the operational semantics. Complex values are

9

10

An Effectful Treatment of Dependent Types

defined to be values containing pm as in - and let be in -constructs. As the normalization of
values do not produce effects, all reasonable evaluation strategies for them are observationally
indistinguishable and we could choose our favourite. However, we may still want to allow
complex values to occur in types, as this greatly increases the expressivity of our type system.
To make sure we lose no expressive power while expressive power when excluding complex
values, we add the rule of figure 7 to dCBPV. We note that this rule introduces no new
terms to dCBPV, at least up to judgemental equality, as M to x in N = return V to x in N =
let x be V in N . This means that it is invisible to the categorical semantics. It allows us
to define the operational semantics for a wider range of terms, however. It allows us to
eliminate complex values from computations (even at types built with complex values!).
Γ `c M = return V : F A
Γ, x : A, Γ0 `c N : B
Γ, Γ0 [V /x] `c M to x in N : B[V /x]

Figure 7 An extra rule to add to dCBPV which does not introduce any new terms.

I Theorem 8 (Redundancy of Complex Values for Computations). For any dCBPV- or
f : B (of dCBPV- or
dCBPV+ computation Γ `c M : B, there is a computation Γ `c M
f : B.
dCBPV+, respectively) which does not contain complex values, such that Γ `c M = M
Moreover, both the CBV- and CBN-translations only produce complex-value-free computations.
We present a small-step operational semantics for (complex value-free) dCBPV computations
in terms of a simple abstract machine that Levy calls the CK-machine. The configuration of
such a machine consists of a pair M, K where Γ `c M : B is a complex value-free computation
and Γ; B `k K : C is a compatible (simple) stack. We call C the type of the configuration.
Stacks4 are formed according to the rules of figure 8.
` Γ; C ctxt
k

Γ; C ` nil : C

Γ, x : A `c M : B
k

Γ; Bj `k K : C

Γ; B `k K : C

Γ; F A ` [·] to x in M :: K : C

k

Γ; Π1≤i≤n Bi ` j :: K : C

Γ `v V : A

Γ; B[V /x] `k K : C

Γ; Πx:A B `k V :: K : C

Figure 8 The rules for forming (simple) stacks.

The initial configurations, transitions (which embody directed versions of the β-rules
of our equational theory) and terminal configurations in the evaluation of a computation
Γ `c M : C on the CK-machine are specified by figure 9.
The operational semantics of dCBPV- and dCBPV+ satisfy the following basic properties.
I Theorem 9 (Pure dCBPV Operational Properties). For every configuration of the CKmachine, at most one transition applies. No transition applies precisely when the configuration
is terminal. Every configuration of type C reduces, in a finite number of transitions, to a
unique terminal configuration of type C.
Proof (sketch). The proof for dCBPV- is no different from the simply typed situation [18],
as the transitions are defined on untyped configurations and are easily seen to preserve types.
Note that types only depend on values, which never get reduced in our transitions.
Only the subject reduction property for dCBPV+ requires some thought. Suppose we
start from a configuration M, K with Γ `c M : B and Γ; B `k K : C. What could conceivably

4

To be precise, these are what Levy calls simple stacks [18]. Analogous to complex values, one can also
conservatively extend the calculus with so-called complex stacks, e.g. by allowing pattern matching into
stacks. This gives us a 1-1 correspondence between categorical models and syntactic theories.

M. Vákár

Initial Configuration
M
, nil

Terminal Configurations
return V
, nil
λi Mi
, nil
λx M
, nil
force z
, K
pm z as hi, xi in Mi , K
pm z as hi in M
, K
pm z as hx, yi in M
, K
pm z as (refl x) in M , K

11

Transitions
let V be x in M
M to x in N
return V
force thunk M
pm hj, V i as hi, xi in Mi
pm hi as hi in M
pm hV, W i as hx, yi in M
pm (refl V ) as (refl x) in M
j‘M
λi Mi
V ‘M
λx M

,
,
,
,
,
,
,
,
,
,
,
,

K
K
[·] to x in N :: K
K
K
K
K
K
K
j :: K
K
V :: K

M [V /x]
M
N [V /x]
M
Mj [V /x]
M
M [V /x, W/y]
M [V /x]
M
Mj
M
M [V /x]

,
,
,
,
,
,
,
,
,
,
,
,

K
[·] to x in N :: K
K
K
K
K
K
K
j :: K
K
V :: K
K

Figure 9 The behaviour of the CK-machine in the evaluation of a computation Γ `c M : C.

happen during a transition is that the resulting configuration M 0 , K 0 can be given types
Γ `c M 0 : B 0 and Γ0 ; B 00 `k K 0 : C, but not Γ ` B 0 = B 00 .
The only transition that can possibly cause this problem is the one for initial computation
return V (see figure 9). Indeed, what could have happened is that we started from a
configuration M to x in N, K, with Γ `c M to x in N : B[thunk M/z], which transitions
to M, [·] to x in N :: K. After this, we continue reducing M , until we end up in a
configuration return V, [·] to x in N :: K. It is now critical when we apply one more transition
(the dangerous one) that for the resulting configuration N [V /x], K we again have that
Γ ` N [V /x] : B[thunk M/z], while we know that Γ ` N [V /x] : B[tr V /z].
This is indeed the case in pure dCBPV+, as all minimal sequences of transitions of the
shape M, K
M 0 , K just consist of an application of a directed version (left to right) of one of
the judgemental equalities of figure 4, hence M = return V so Γ ` N [V /x] : B[thunk M/z]. J

7

Adding Effects

We show by example how one adds effects to dCBPV, focussing on the operational semantics.
Figure 10 gives examples of effects one could consider: divergence, recursion, printing elements
m of some monoid M, erratic choice from finitely many alternatives, errors e from some set
E, writing a global states s ∈ S and reading a global state to s. The framework fits many
more examples like probabilistic erratic choice, local references and control operators [18].
Γ `c diverge : B
Γ `c error e : B

Γ, z : U B `c M : B
Γ ` c µz M : B

Γ `c M : B
Γ `c print m . M : B

{Γ `c Mi : B}1≤i≤n
Γ `c choosei (Mi ) : B

Γ `c M : B
Γ `c write s . M : B

{Γ `c Ms : B}s∈S
Γ `c readtos (Ms ) : B

Figure 10 Some examples of effects we could add to CBPV.

For the operational semantics of printing and state, we need to add some hardware to our
machine. Therefore, a configuration will now consist of a quadruple M, K, m, s where M, K
are as before, m is an element of a printing monoid (M, , ∗) modelling some channel for
output and s is an element of a finite pointed set of states (S, s0 ) holding the current value of
our storage cell. We lift the operational semantics of all existing language constructs to this
setting by specifying that they do not modify m and s, that terminal configurations can have
any value of m and s and that initial configurations always have value m =  and s = s0 for
the fixed initial state s0 . Figure 11 specifies the operational semantics for our effects.
We extend the results of the previous section to this effectful setting. While we will have
to add some extra rules to dCBPV+, dCBPV- satisfies theorem 10 without any further rules.

12

An Effectful Treatment of Dependent Types

Transitions
diverge
µz M
choosei (Mi )
print n . M
write s0 . M
readtos0 (Ms0 )

,
,
,
,
,
,

K
K
K
K
K
K

,
,
,
,
,
,

m
m
m
m
m
m

,
,
,
,
,
,

s
s
s
s
s
s

diverge
M [thunk µz M/z]
Mj
M
M
Ms

,
,
,
,
,
,

K
K
K
K
K
K

,
,
,
,
,
,

m
m
m
m∗n
m
m

,
,
,
,
,
,

s
s
s
s
s0
s

Terminal Configurations
error e , K , m , s

Figure 11 The operational semantics for divergence, recursion, erratic choice, errors, printing
and writing and reading global state.

I Theorem 10 (Effectful dCBPV Operational Properties). Transitions respect the type of the
configuration. None applies precisely if we are in a terminal configuration. In absence of
erratic choice, at most one transition applies to each configuration. In absence of divergence
and recursion, every configuration reduces to a terminal one in a finite number of steps.
As highlighted by the proof of theorem 9, to guarantee subject reduction for dCBPV+, we
again need to establish that for every transition M, K, m, s
M 0 , K, m0 , s0 of figure 10,
c
0
c
Γ ` N : B[thunk M /z] implies that Γ ` N : B[thunk M/z]. A sufficient condition, would
be to add equations M = M 0 . For divergence and errors, these equations would be vacuous,
and for recursion, it gives us the usual equation µz M = M [thunk µz M/z]. For printing,
erratic choice and global state, however, these equations are not reasonable to demand.
Γ `c N : B[thunk M 0 /z]
Instead, for these effects, we suggest to add explicitly the rules
.
c
0
Γ ` N : B[thunk (M )/z]

Specifically, we see that a computation type in which we substitute (the thunk of) a
computation with multiple branches (erratic choice, reading state) has to contain each of the
types obtained by substituting any of the branches instead. Similarly, a type in which we
substitute (the thunk of) a computation which writes (printing, writing a state) and then
performs a computation M has to contain the type obtained by just substituting M . In
short: a type can only shrink as the computation unfolds. As anticipated, these rules restore
the subject reduction property for effectful dCBPV+ and make theorem 10 hold for it too.
We can extend the CBV- and CBN-translations to the effectful setting following figure
12. By analogy with the simply typed situation, this should induce the expected operational
semantics, at least for terms of ground type, although we are not aware of such an operational
semantics ever being outlined in literature.
CBV Term M
op(M1 , . . . , Mm )
µx M

CBPV Term M v
v
op(M1v , . . . , Mm
)
µz (force z to x in M v )

CBN Term M
op(M1 , . . . , Mm )
µz M

CBPV Term M n
n
op(M1n , . . . , Mm
)
n
µz M

Figure 12 The CBV- and CBN-translations for effectful terms. Here, we treat all algebraic
effects (in particular, divergence, errors, erratic choice, printing and global state) uniformly by
letting op range over their operations. z is assumed to be fresh in the CBV-translation µx M .

I Remark (Type Checking). One could argue that a type checker is as important an operational
aspect to the implementation of a DTT as a small-step semantics. We leave the description of
a type checking algorithm to future work. We note that the core step in the implementation
of a type checker is a normalization algorithm for directed versions (from left to right) of the
judgemental equalities, as this would give us a normalization procedure for types. We hope
to be able to construct such an algorithm for dCBPV- using normalization by evaluation
by combining the techniques of [30] and [31]. Our hope is that this will lead to a proof
of decidable type checking of the system at least in absence of the η-law for Id-types and
without recursion. We note that the complexity of a type checking algorithm can vary widely

M. Vákár

13

depending on which equations we include for effects. The idea is that one only includes
a basic set of program equations (perhaps including algebraicity equations for effects) as
judgemental equalities to be able to decide type checking and to postulate other equations
(like the Plotkin-Power equations for state) as propositional equalities, which can be used
for manual or tactic-aided reasoning about effectful programs. Type checking for effectful
dCBPV+ seems more challenging, as the system essentially features a form of subtyping.

8

More Connectives?

We very briefly outline how to add more connectives to dCBPV.
A first class of connectives we consider are projection dependent products, or Σ-types
on computations. Given a context Γ, z1 : U B1 , . . . , zn : U Bn , we can form these types
Γ ` Πdep
1≤i≤n Bi ctype and we construct and destruct their terms using the rules of figure 13.
{Γ `c Mi : Bi [thunk M1 /z1 , . . . , thunk Mi−1 /zi−1 ]}1≤i≤n
c

Γ ` λi Mi :

Πdep
1≤i≤n Bi

Γ `c M : Πdep
1≤i≤n Bi
c

Γ ` i‘M : Bi [thunk 1‘M/z1 , . . . , thunk (i − 1)‘M/zi−1 ]

Figure 13 Rules for projection dependent products, to which we add the obvious β- and η-laws.

Their categorical semantics corresponds to having strong n-ary Σ-types in D in the sense of
objects Πdep
1≤i≤n Bi such that pΓ,U Πdep
Bi = pΓ.U B1 .··· .U Bn−1 ,U Bn ; . . . ; pΓ,U B1 . In particular,
1≤i≤n

∼
we see that U Πdep
1≤i≤2 B i = ΣU B 1 U B 2 . Similarly, we can define equivalents of the other positive
connectives R like Σ1≤i≤n - and Id-types on computation types in the sense of connectives
R0 (B 1 , . . . , B n ) such that U R0 (B 1 , . . . , B n ) ∼
= R(U B 1 , . . . , U B n ). These correspond to e.g.
additive Σ- and Id-types in linear DTT. In all cases, we give an operational semantics where
destructors push to the stack and constructors pop the stack and substitute.
Another connective from linear DTT that generalizes to dCBPV is the multiplicative
Σ-type Γ ` Σ⊗
F A B ctype, for Γ, x : A ` B ctype. These type formers are dependently typed
generalizations of the F (−) ⊗ −-connective of the EEC (there written !(−) ⊗ −). Their
categorical semantics, as in linear DTT, is given by left adjoint functors Σ⊗
F A a −{pΓ,A } to
change of base in D, satisfying the left Beck-Chevalley condition. In particular, they satisfy
the equation F ΣA A0 ∼
= ΣF A F A0 .
Finally, to build a practically useful system, strong type forming mechanisms like inductive
families and induction-recursion (including universes) should probably be added to dCBPV
as constructions on value types. While it seems believable that we then still get a CBVand CBN-translation in dCBPV+ for inductive families, the situation for universes is less
straightforward. Another question is if such translations are desirable or if we are better off
working with the simpler system dCBPV- in the first place.

9

Future Work

In this paper, we gave an extension to the realm of dependent types of Levy’s CBPV analysis
of CBV- and CBN-λ-calculi. We hope, one the one hand, that this can shed some light
on the theoretical puzzle of how the relationship between effects and dependent types can
be understood. On the other hand, we hope it can provide some guidance in the daunting
but worthwhile challenge of combining dependent types with effects in a system which is
simultaneously mathematically elegant and practically useful for writing certified real world
software. To further achieve these two goals, we have the following future work in mind.
A first priority is the implementation of a type checker for dCBPV- (and perhaps
dCBPV+). A second question to be addressed is what needs to be done to make dCBPV into

14

An Effectful Treatment of Dependent Types

a practically useful language for certified effectful programming. Does dCBPV- suffice for
this or do we need to turn to dCBPV+? Thirdly, the recent CBN game semantics for DTT
of [32], which can be extended to model recursion, local ground store and control operators,
should give rise to a model of dCBPV+. Fourthly, we want to investigate if the CBV- and
CBN-translations into dCBPV+ extend to more expressive type forming mechanisms like
inductive families and inductive-recursive definitions like type universes. In particular, we
hope this will lead to a better understanding of the rather enigmatic nature of CBV-type
dependency. Finally, it remains to be seen what the status is of subject reduction in dCBPV+
in presence of other effects like control operators, local state and general references. We hope
the game semantics of DTT can be of use here.
Related Work This paper is based on the preprint [25], which provides more context, proofs
and discussion. Since this appeared, independent work by Ahman, Ghani and Plotkin [33]
has been made public which partly overlaps with sections 3 and 4 of this paper. It describes a
dependently typed EEC, closely related to dCBPV- extended with complex stacks and Σ⊗
F −types, and its categorical semantics which - modulo details - is a fibrational reformulation of
our semantics for this calculus. Additionally, our sections 3 and 4 consider a more expressive
calculus dCBPV+ where we can substitute effectful computations in dependent functions.
This allows us to define CBV- and CBN-translations into it. Also relevant is the work on
linear [16, 13] and polarised [20] DTT and on domain and game semantics for DTT [29, 32].
Acknowledgements I want to thank Tim Zakian, Alex Kavvos and Sam Staton for many
interesting discussions and Paul Blain Levy for his explanations. I am grateful to Samson
Abramsky for his support. The author is funded by the EPSRC and the Clarendon Fund.
References
1
2
3
4
5

6
7
8

9

10

Martin Hofmann. Extensional Constructs in Intensional Type Theory. Springer, 1997.
The Coq development team. The Coq proof assistant reference manual. LogiCal Project,
2004. Version 8.0.
Ulf Norell. Towards a practical programming language based on dependent type theory,
volume 32. Chalmers University of Technology, 2007.
Lennart Augustsson. Cayenne — a language with dependent types. In ACM SIGPLAN
Notices, volume 34, pages 239–250. ACM, 1998.
Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury. πσ: Dependent types without the sugar. In Functional and Logic Programming, pages 40–55. Springer
Berlin Heidelberg, 2010.
Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining proofs and programs
in a dependently typed language. ACM SIGPLAN Notices, 49(1):33–45, 2014.
Edwin Brady. Idris, a general-purpose dependently typed programming language: Design
and implementation. Journal of Functional Programming, 23(05):552–593, 2013.
Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Proceedings
of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages,
pages 214–227. ACM, 1999.
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud,
Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, et al. Dependent types and multi-monadic effects in f*, 2015.
Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in
hoare type theory. In ACM SIGPLAN Notices, volume 41, pages 62–73. ACM, 2006.

M. Vákár

11
12
13
14
15
16

17
18
19

20
21
22
23
24
25
26
27
28
29
30

31
32
33

Iliano Cervesato and Frank Pfenning. A linear logical framework. In LICS’96. Proceedings.,
pages 264–275. IEEE, 1996.
Matthijs Vákár. Syntax and semantics of linear dependent types. arXiv preprint
arXiv:1405.0033, 2014.
Matthijs Vákár. A categorical semantics for linear logical frameworks. pages 102–116, 2015.
P Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Computer
Science Logic, pages 121–135. Springer, 1995.
Andrew Barber and Gordon Plotkin. Dual intuitionistic linear logic. University of Edinburgh, Department of Computer Science, 1996.
Neelakantan R Krishnaswami, Pierre Pradic, and Nick Benton. Integrating linear and
dependent types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages, pages 17–30. ACM, 2015.
Eugenio Moggi. Notions of computation and monads. Information and computation,
93(1):55–92, 1991.
Paul Blain Levy. Call-by-push-value: A Functional/imperative Synthesis, volume 2.
Springer Science & Business Media, 2012.
Nick Benton and Philip Wadler. Linear logic, monads and the lambda calculus. In Logic
in Computer Science, 1996. LICS’96. Proceedings., Eleventh Annual IEEE Symposium on,
pages 420–431. IEEE, 1996.
Daniel R Licata and Robert Harper. Positively dependent types. In Proceedings of the 3rd
workshop on Programming languages meets program verification, pages 3–14. ACM, 2009.
Paul Blain Levy. Adjunction models for call-by-push-value with stacks. Theory and Applications of Categories, 14(5):75–110, 2005.
Bart Jacobs. Comprehension categories and the semantics of type dependency. Theoretical
Computer Science, 107(2):169–207, 1993.
Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. Enriching an effect calculus with
linear types. In CSL, volume 5771, pages 240–254. Springer, 2009.
Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. HigherOrder and Symbolic Computation, 19(4):377–414, 2006.
Matthijs Vákár.
A framework for dependent types and effects.
arXiv preprint
arXiv:1512.08009, 2015.
U HoTTbaki.
Homotopy Type Theory: Univalent Foundations of Mathematics.
http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory.
arXiv preprint arXiv:1509.07584, 2015.
Urs Schreiber and Michael Shulman. Quantum gauge field theory in cohesive homotopy
type theory. arXiv preprint arXiv:1408.0054, 2014.
Erik Palmgren and Viggo Stoltenberg-Hansen. Domain interpretations of Martin-Löf’s
partial type theory. Annals of Pure and Applied Logic, 48(2):135–196, 1990.
Andreas Abel, Klaus Aehlig, and Peter Dybjer. Normalization by evaluation for martin-löf
type theory with one universe. Electronic Notes in Theoretical Computer Science, 173:17–
39, 2007.
Danel Ahman and Sam Staton. Normalization by evaluation and algebraic effects. Electronic Notes in Theoretical Computer Science, 298:51–69, 2013.
Samson Abramsky, Radha Jagadeesan, and Matthijs Vákár. Games for dependent types.
In Automata, Languages, and Programming, pages 31–43. Springer, 2015.
Danel Ahman, Neil Ghani, and Gordon Plotkin. Dependent types and fibred computational
effects. Springer, 2016. To appear in Foundations of Software Science and Computation
Structures, available at http://homepages.inf.ed.ac.uk/s1225336/.

15

