Dependent Types from Counterexamples ∗Tachio Terauchi
Tohoku University
terauchi@ecei.tohoku.ac.jp

Abstract
Motivated by recent research in abstract model checking, we
present a new approach to inferring dependent types. Unlike manyof the existing approaches, our approach does not rely on programmers to supply the candidate (or the correct) types for the recursivefunctions and instead does counterexample-guided refinement toautomatically generate the set of candidate dependent types. The
main idea is to extend the classical fixed-point type inference routine to return a counterexample if the program is found untypablewith the current set of candidate types. Then, an interpolating theorem prover is used to validate the counterexample as a real typeerror or generate additional candidate dependent types to refute thespurious counterexample. The process is repeated until either a realtype error is found or sufficient candidates are generated to prove
the program typable. Our system makes non-trivial use of “linear”
intersection types in the refinement phase.
The paper presents the type inference system and reports on theexperience with a prototype implementation that infers dependent
types for a subset of the Ocaml language. The implementation
infers dependent types containing predicates from the quantifierfree theory of linear arithmetic and equality with uninterpretedfunction symbols.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification—Model checking; F.3.1 [Logics and Meaning of Programs]: Specifying and Verifying and Reasoning about Programs—Mechanical verification; F.3.2 [Logics
and Meaning of Programs]: Semantics of Programming Languages—
Program analysis; F.3.3 [Logics and Meaning of Programs]: Studies of Program Constructs—Type structure
General Terms

Algorithms, Languages, Theory, Verification

Keywords Dependent types, Intersection types, Interpolation,
Counterexamples, Type inference

1. Introduction
This paper follows the work on applying dependent types to checking complex properties of programs that are beyond the reach of
conventional type systems like ML types. In this paper, by dependent types, we mean refinement types [14] that embed first-order∗ This work was supported by MEXT KAKENHI 20700019 and 20240001.

Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. To copy otherwise, to republish, to post on servers or to redistributeto lists, requires prior specific permission and/or a fee.
POPL’10, January 17–23, 2010, Madrid, Spain.
Copyright c 2010 ACM 978-1-60558-479-9/10/01. . . $10.00

let rec mult x y =if x <= 0 || y <= 0 then0else
x + mult x (y - 1)
in assert (100 <= mult 100 100)
Figure 1. The multiplication example.
logic formulas. For instance, suppose we want to check that the assertion never fails in the program shown in Figure 1. (Here, we use
the Ocaml syntax.)
One way to check the assertion is by giving mult the following
dependent type.1
x : int → y : int →{u : int | (x ≥ 0 ∧ y > 0 ⇒ u ≥ x)∧(y ≤ 0 ⇒ u ≥ 0)}
The type says that mult takes integers x and y, and returns an
integer that is at least as large as x if x ≥ 0 and y > 0, and nonnegative if y ≤ 0. (As usual, ⇒ binds weaker than other logicaloperators, and → associates to the right.) Indeed, the type is a valid
type for mult and is sufficient to prove that the assertion does not
fail. Note that the type is neither the strongest (i.e., the most precise)type nor the weakest necessary type that can be assigned to multto prove the assertion. The strongest type for mult would bex : int → y : int →{u : int | (x > 0 ∧ y > 0 ⇒ u = x × y)∧(x ≤ 0 ∨ y ≤ 0 ⇒ u = 0)}
which contains non-linear arithmetic, as expected.
This paper presents a method for inferring sufficiently strong
dependent types to check the given properties of a program. Our
approach avoids computing the strongest or the weakest necessary
type, and instead returns some type that is sufficient to prove theproperty when terminating with success.
Many existing dependent type systems (e.g., [4, 10, 40]) require
the programmer to annotate recursive functions like mult withthe correct types. Other systems [14, 34] require the domain ofcandidate types to be pre-defined and form a finite-height latticeso that the type checking can be implemented as a fixed-point
algorithm that infers the strongest types in a bottom-up manner.
We propose a different approach to checking and inferring dependent types that does not require a pre-defined set of correct orcandidate dependent types. Our approach is inspired by research incounterexample guided abstraction refinement (CEGAR) for model
checking [3, 9, 16, 28]. The core of our system is a CEGAR loopthat iteratively refines the lattice of candidate dependent types until
either the program is found to be actually untypable or the lattice
1 The type syntax is borrowed from Augustsson [1] (also used in [12, 22,

23, 34, 37]).

d
e

::=
::=
|

→
d ∪ {F −x = e} | ∅x | c | F | let x = e1 in e2 | e x
if x then e1 else e2 | assert e

Figure 2. The syntax of the simple functional language.
becomes refined enough to type check the program. We start witha coarse lattice containing few candidates and gradually add types
that are sufficient to refute the spurious counterexamples encountered during the CEGAR iteration.
A counterexample in our system is an “unwound” slice of the
program that is untypable with the current candidates. The refinement phase decides whether the slice can be typed if the types are
not confined to the candidates, and if so, generates new candidates
from the inferred typing (if not, then the program is really untypable). For this, we employ recent techniques from both type systems and model checking research: linear intersection types [21]and interpolation [27]. We use linear intersection type inference toinfer a type derivation “shape” that is sufficient for typing the counterexample, and we use an interpolating theorem prover to quickly
compute good candidate types from the type derivation (in particular, without explicit quantifier elimination).
The rest of the paper is organized as follows. Section 2 introduces the language and the dependent type system. The main contribution of the paper is the CEGAR-inspired type inference systemdescribed in Sections 3, 4, 5, and 6. While the paper mostly focuseson the assertion checking application for simplicity, it is easy to extend the system to more general program specification checking as
discussed in Section 7. Section 8 describes the prototype implementation for a subset of the Ocaml language, Section 9 discusses
related work, and Section 10 concludes. The proofs of the key results appear in Appendix C.

2. Preliminaries
We focus on a small functional language shown in Figure 2. We
briefly describe the syntax. A program, d, is a finite set of function→
definitions, F −x = e, which defines a function named F with the→→formal parameters −x and the body e. The notation −a denotes apossibly empty sequence. We often use letters u, x, y, z, ui , etc. torange over program variables and first-order logic variables, andletters F , G, H, Fi , etc. to range over function names. Functions
can be mutually recursive in that the body of a function may referto other functions, including itself. We assume that each function
is closed (except for the free function names). We also assume thatevery function name is unique and that there is a function named
main that takes no arguments. Note that nested function definitions
can be supported via lambda lifting [19].
An expression, e, is a variable, a constant c, a function name, alet expression let x = e1 in e2 , a (constant or function) application
e x, a conditional branch if x then e1 else e2 , or an assertion
assert e. Constants include integer and boolean constants such as
0 and true, as well as integer and boolean operations such as +and ≤. For simplicity, we restrict branch condition and function
arguments to just variables.2
We restrict the body of a function to continuation passing style(CPS) so that a function does not return. We also impose the CPS
restriction to the body of a let expression (i.e., e′ in let x = e in e′ )and those of a branch (i.e., e1 and e2 in if x then e1 else e2 )so that they are also non-returning. As usual, non-returning expressions (i.e., non-partial function applications, let expressions, andconditional expressions) are restricted to occur only in a continua2 The implementation lifts this restriction by online A-normalization [13].

E ::= let x = E in e | E e | v E
Figure 3. The non-CPS evaluation contexts.
→→→
F−x = e ∈ d |−x | = |−
v|
APP
→
−
−
→
−
→
F v → e[ v / x ]d→arity (c) = |−
v|
CST
→
−
→
E[c v ] → E[[[c]](−v )]dlet x = v in e →d e[v/x] LET
if true then e1 else e2 →d e1

IF1

if false then e1 else e2 →d e2

IF2

E[assert true] →d E[0]AS1

E[assert false] →d fail AS2
Figure 4. The semantics of the simple functional language.
tion context (i.e., not in a non-CPS evaluation context E shown in
Figure 3). CPS is only enforced on user-defined functions so that
constant operations need not be CPS.
The CPS restriction is imposed only to simplify the exposition.
Non-CPS expressions may be supported indirectly via CPS conversion or directly by extending the type system with conditional types
and union (i.e., disjunctive) types.3
The rest of the syntax is straightforward. As usual, a function
application associates to the left so that e0 e1 e2 = (e0 e1 ) e2 . We→e for the series of applications e0 e1 e2 . . . en where
write e0 −→−e = e1 , e2 , . . . , en . We write e1 ; e2 for let x = e1 in e2 such thatx ∈/ free(e2 ). Without loss of generality, we assume that boundvariables are distinct.
Note that, because of higher-order functions and partial applications, function calls are not syntactically obvious, and one syntactic
occurrence of a function name may end up being called from multiple places.
We define the call-by-value semantics of the language as asmall-step reduction relation from states to states. A state is a runtime expression e that extends the source expressions with values v
and a special failure state, defined as follows.
v ::= c | F | v1 v2
e ::= · · · | v | fail(We overload the symbol e to range over run-time expressions when→
it is clear from the context.) We restrict the application F −v (resp.
→c−v ) to be a value only when it is partial, that is, only when the arity→of F (resp. c) is greater than |−v |. Note that a partial application
denotes a closure value.
Figure 3 defines the non-CPS evaluation contexts. Figure 4
shows the reduction rules. The reduction rules are mostly straightforward. In CST, the notation arity (c) denotes the arity of the constant operation c. Here, [[c]] is the relation denoting the semantics
of c, so that, for example [[+]](i, j) = i + j for all integers i and j.
AS1 returns a dummy value 0, and AS2 aborts the program with anassertion failure. Note that, because of CPS, APP, LET, IF1, andIF2 only occur at the top-level.
3 The latter approach is taken in the implementation discussed in Section 8.

τ
σ

::=
::=

⋆ | {u:B | θ} | x:σ → τ
τ | σ1 ∧ σ2

Figure 5. The syntax of dependent types.

sty (x) is not basesty(x) is base
V
VaF
VaB
Γ; θ ⊢ x : {u:B | u = x}
Γ, x: i τi ; θ ⊢ x : τiΓ, F :

Vi τi ; θ ⊢ F : τi

Γ⊢e:τ
Int1
Γ; θ ⊢∧ e : τFunΓ; θ ⊢ c : ty (c)CstΓ1 ; θ ⊢ ∧ e : σ 1 Γ2 ; θ ⊢ ∧ e : σ 2Int2
Γ1 ∧ Γ2 ; θ ⊢ ∧ e : σ 1 ∧ σ 2

Γ1 ; θ ⊢∧ e1 : σ Γ2 , x:σ; θ ⊢ e2 : ⋆Let
Γ1 ∧ Γ2 ; θ ⊢ let x = e1 in e2 : ⋆Γ1 ; θ ⊢ e : y:σ → τ Γ2 ; θ ⊢∧ x : σ ′ Γ2 ; θ ⊢ σ ′ ≤ σAppΓ1 ∧ Γ2 ; θ ⊢ e x : τ [x/y]Γ1 ; θ ∧ x = true ⊢ e1 : ⋆ Γ2 ; θ ∧ x = false ⊢ e2 : ⋆IfΓ1 ∧ Γ2 ; θ ⊢ if x then e1 else e2 : ⋆Γ; θ ⊢∧ e : σ Γ; θ ⊢ σ ≤ {u:bool | u = true}
AssertΓ; θ ⊢ assert e : {u:int | u = 0}
Figure 6. The type checking rules.
We define a run of a program to be a sequence of reductions
from the initial state emain where main () = emain ∈ d. (Here, ()denotes the empty argument sequence.) We write e →∗d e′ for zeroor more reductions from e to e′ .
We assume that a program is typable with the standard simple
type system4 so that it is guaranteed to not get stuck, for example,
by trying to use an integer as a function. Therefore, a program either
runs forever safely (due to CPS, a program cannot return), or aborts
with an assertion failure. We call a program safe if its run does notcause an assertion failure.
D EFINITION 2.1 (Safety). A program d is said to be safe if
emain 6→∗d fail where main () = emain ∈ d.
Being simply-typable does not imply safety. In the following, we
present a dependent type system that guarantees the safety of typable programs.
2.1 Dependent Type System
Our dependent type system is essentially the previous systems [12,34, 37] extended with intersection types. The reason for adding
intersection types is not just to increase expressibility; it is actuallycrucial to the type inference system described later in the paper.
Recall that a program is simply-typed. For each expression e inthe program, we write sty (e) to denote its simple type. A simple
type, s, is formally defined by the following grammar:
B
s

::=
::=

int | bool
⋆ | B | s → s′

Here, B is called base type, and the dummy type ⋆ represents thetype of a CPS expression.
Figure 5 shows the syntax of dependent types. Here, {u:B | θ}is a refinement base type that refines the base type B by the formula
4 See Appendix A for the definition of the simple type system.

θ which is a formula in some first-order theory. We sometimes
abbreviate {u:B | θ} simply as B when θ is a tautology (e.g.,{u:int | ⊤} = int). Intuitively, {u:B | θ} denotes the type ofsome value u of the base type B satisfying the formula θ. The typex : σ → τ is a dependent function type consisting of the argument
type σ and the return type τ . Intuitively, x:σ → τ denotes the typeof a function (or a constant operation) that returns a value of thetype τ [y/x] when applied to any argument y of the type σ.
The type {x:B | θ} binds x within θ. Likewise, x : σ → τbinds x in τ (but not in σ). We sometimes abbreviate x :σ → τ as
σ → τ when x does not occur free in τ . Types are equivalent up torenaming of bound variables.
We use the symbol σ to distinguish types with possible top-levelintersections from those without (for which we use τ ). Here, theintersection operator ∧ is associative, commutative, and idempotent
V(ACI),
V so that, for example, τ ∧ τ = τ . We sometimes write i τior T for the type τ1 ∧ τ2 ∧ · · · ∧ τn such that {τ1 , . . . , τn } = T
is a non-empty set. Note that, because of ACI, any σ can be written
in such a form.
V
For any intersection of types i τi , we enforce that each τi is of
the same simple-type shape. Formally, the simple-type shape of σis the simple type simple(σ) defined inductively as follows:
simple(x:σ → τ ) = simple(σ) → simple(τ )simple({u:B | θ}) = B
simple(⋆)
V=⋆simple( {τ, . . .}) = simple(τ )V
Then, we enforce that for any type T ,simple(τ ) = simple(τ ′ )′for all τ, τ ∈ T . This does not reduce expressibility because thetype system is a refinement type system [14] of the simple typesystem, and so only the types of the same simple-type shape aremeaningful to intersect. Without loss of generality, we implicitly
assume that any dependent type σ assigned to e in the dependent
type system satisfies simple(σ) = sty (e).
Figure 6 shows the type checking rules of the dependent typesystem. The judgements are of the form Γ; θ ⊢ e : τ where Γ
is a type environment mapping variables and function names totypes possibly containing top-level intersections (i.e., σ’s), and θ
is a formula. The formula θ is used to accumulate the assumptions
from nesting branch conditions.
We discuss each typing rule. VaB types base-type variables.
Note that the rule ignores the environment. Expressibility is not
reduced, however, because the assumption about x in the environment gets discharged at subtyping. The rule is borrowed from previous work [32, 34, 37]. VaF types function-type variables bylooking up the environment and selecting a type from the intersection. Here, as usual, Γ, x : σ denotes the mapping Γ ∪ {x 7→ σ}
if x ∈/ dom(Γ), and is undefined otherwise. Fun is exactly like
VaF except that it is for function names. Cst types constants.
Here, ty (c) is some sound5 dependent type for the constant c (e.g.,ty(+) = x:int → y:int → {u:int | u = x + y}).
Int1 and Int2 introduce intersection types. Here, Γ1 ∧ Γ2 isdefined as follows.
Γ1 ∧ Γ2 = {x 7→ Γ1 (x) ∧ Γ2 (x) | x ∈ dom(Γ1 ) ∩ dom(Γ2 )}∪{x 7→ Γ1 (x) | x ∈ dom(Γ1 ) ∧ x ∈/ dom(Γ2 )}∪{x 7→ Γ2 (x) | x ∈/ dom(Γ1 ) ∧ x ∈ dom(Γ2 )}We could have used a simpler set of rules that shares the environments of the sub-judgements because intersections are non-linear(recall that ∧ is ACI), but this format makes the introduction of
the linearity restriction smoother later in Section 5.2. Note that wewrite ⊢∧ to distinguish judgements that can introduce top-level intersections.
5 See Appendix B for the definition of a sound constant type.

Γ; θ ⊢ ⋆ ≤ ⋆

SubC

u∈
/ free([[Γ]]) ([[Γ]] ∧ θ ∧ θ1 ) ⇒ θ2
Γ; θ ⊢ {u:B | θ1 } ≤ {u:B | θ2 }SubB

Γ; θ ⊢ σ2 ≤ σ1 Γ, x : σ2 ; θ ⊢ τ1 ≤ τ2
SubF
Γ; θ ⊢ x:σ1 → τ1 ≤ x:σ2 → τ2∃i.(Γ; θ ⊢ τi ≤ τ )V
SubI1
Γ; θ ⊢ i τi ≤ τ∀i.(Γ; θ ⊢ σ ≤ τi )V
SubI2
Γ; θ ⊢ σ ≤ i τi

Figure 7. The subtyping rules.

Let is self-explanatory. Note that the typing for e1 may introduce top-level intersections. App types applications. Here, τ [x/y]is the usual capture-avoiding substitution. App checks that the actual argument conforms to the formal argument type via the subtyping Γ2 ; θ ⊢ σ ′ ≤ σ. Figure 7 shows the subtyping rules,
which are a straightforward extension of those of the previous systems [12, 34, 37] with intersection types. In SubB, [[Γ]] is the firstorder logic formula denoting the assumptions about the base-type
variables, and is formally defined as follows.
V V
V[[Γ]] = { i θi [x/u] | Γ(x) = i {u:B | θi }}The If rule types conditional expressions. Note that the assumption about the branch condition (i.e., x) is recorded in the environment. Finally, Assert checks the assertion via subtyping.
We say that a type is closed if it has no free variables. Let∆ be a top-level type environment mapping function names totypes. We say that σ is a well-formed type for F if σ is closed
and simple(σ) = sty (F ). We say that ∆ is a well-formed toplevel type environment if ∆(F ) is well-formed for each F . Unlessmentioned otherwise, we restrict ∆ to range only over well-formed
top-level type environments in the rest of the paper.
−→ → τ to abbreviate the function typeLet us write −x:σ

x1 :σ1 → · · · → xn :σn → τ−−→
where x:σ = x1 : σ1 , . . . , xn : σn . We define the notion of a welltyped program.
D EFINITION 2.2 (Well-typed program). We write ∆ ⊢ d if for→−→ ⊤ ⊢ e : ⋆ for each
x:σ;each function F −x = e ∈ d, we have ∆, −−→ → ⋆ in ∆(F ) = V τ .
τi = −x:σi i
We say that a program d is well-typed (equivalently, typable) if
there exists ∆ such that ∆ ⊢ d.
Assuming that the types of the constants ty(c) are sound, thetype system ensures that a well-typed program does not cause an
assertion failure.
T HEOREM 2.3 (Soundness). If ∆ ⊢ d then d is safe.
The proof is analogous to that of the soundness result for similar
dependent type systems [12, 34, 37] and is omitted.
E XAMPLE 2.4. Let d consist of the following three functions. (Weelide A-normalization for readability.)sum x y k =if x ≤ 0 then k y else sum (x − 1) (x + y) k
check x =assert (100 ≤ x); check x
main () =sum 100 0 check

Note P
that sum is a function that, given integers x and y, computes
y + i∈{0,...,x} i and applies the continuation k to the result.
P
Therefore, d runs safely forever if 100 ≤i∈{0,...,100} i, andaborts with an assertion failure otherwise (i.e., it will run forever).
Assume that we are given the following constant types.
ty(≤) = x:int → y:int → {u:bool | u = x ≤ y}ty(−) = x:int → y:int → {u:int | u = x − y}ty(+) = x:int → y:int → {u:int | u = x + y}ty(i) = {u:int | u = i} where i ∈ {0, 1, 100}
We show that we can prove d to be safe with our type system
assuming that the underlying theory supports booleans and linear
arithmetic.
Let ∆ be the following typing environment.
∆(main) = () → ⋆∆(check) =V {u:int | u ≥ 100} → ⋆∆(sum) = T

where
T =
{ x:{u:int | u ≥ 100} → y:{u:int | u ≥ 0} →({u:int | u ≥ 100} → ⋆) → ⋆,x:int → y:int → ({u:int | u ≥ y} → ⋆) → ⋆ }(Here, () → ⋆ is the special function type for main having an empty
sequence of arguments. See Definition 2.2.)
It is a routine to check that ∆ ⊢ d. Note that the type of sum
does Pnot say that it actually returns (i.e., calls the continuation with)y + i∈{0,...,x} i, but only that it returns some integer at least as
large as 100 when called with x ≥ 100 and y ≥ 0, and some
integer at least as large as y unconditionally, which is sufficient for
typing d.

3. Type Inference Overview
We now present our CEGAR-inspired procedure that checks if thegiven program d is typable, and if so, returns ∆ such that ∆ ⊢ d.
The inference procedure is a semi-algorithm as it is not guaranteed
to terminate, but it is sound and complete in that it is guaranteed
to return some correct typing when terminating with success andreject the program as untypable only if it is actually untypable.
(In practice, we make the procedure give up after some numberof iterations, returning “unknown.”)
The type inference maintains a lattice of candidate top-level
type environments, and repeatedly executes the following two algorithms, one after the other.
• The fixed-point type inference algorithm checks if there exista typing for the program within the current candidates via afixed-point iteration over the lattice of candidate top-level typeenvironments. The algorithm returns a counterexample if the
program is found untypable with the current candidates. The
counterexample records the number of times the fixed-point
iteration was executed to reach the type error. Otherwise, theprogram is found typable and the process exits by returning theinferred typing. (Section 4)• Given a counterexample, the refinement algorithm unwinds therecursive definitions the number of times recorded in the counterexample, generating a non-recursive program slice. Then, thealgorithm decides the slice’s typability completely (i.e., not restricted to any candidates). If the slice is found untypable, thenso is the original, and the process exits. Otherwise, the dependent types that are used to type the slice are added as the new
candidates to refine the lattice. This phase uses linear intersection type inference and interpolation to infer types for the unwound program slice. (Section 5)

The two components are both algorithms in that they are guaranteed
to terminate. The following sections describe the two components
in detail.

4. Fixed-point Type Inference
A candidate set Θ is a mapping from function symbols to a nonempty finite set of dependent types with no top-level intersections
such that for all τ ∈ Θ(FV), τ is closed and simple(τ ) = sty (F ).
Θ induces the lattice Θ defined as follows.6
VVΘ = {∆ | ∀F.∆(F ) = T where T ⊆ Θ(F )}VFor ∆1 , ∆2 ∈Θ, we orderV ∆1  ∆2 if for
V all F , we haveT1 ⊇ T2Vwhere ∆1 (F ) = T1 and ∆2 (F ) = T2 . It is easy
V to
see that Θ with  forms
V a lattice with the mapping λF. ∅ as
the top element and λF. Θ(FV) as the bottom
V element. Note thatexcept for the ones containing ∅, any ∆ ∈ Θ is a well-formed
top-level type environment.
V
We define the algorithm InferNext
that takes ∆ ∈ Θ and reVturns the strongest typing ∆′ ∈ Θ for d that can be typed with ∆(d is an implicit parameter to InferNext ). Moreprecisely, for ∆ aVtype environment (i.e., for all F , ∆(F ) 6= ∅), InferNext (∆) =→∆′ such that for each F −x = e ∈ d,
V
′
−
−
→
−
→ ⊤ ⊢ e : ⋆}∆ (F ) = {x:σ → ⋆ ∈ Θ(F ) | ∆, −x:σ;If ∆ is not a type environment, then we take InferNext (∆) = ∆.
InferNext (∆) can be effectively computed assuming that we
can decide the typing judgements Γ; θ ⊢ e : τ . The main complexity involved here is deciding the subtyping relation SubB (cf.
Figure 7), which can be done by the help from a theorem prover
supporting the underlying first order theory.
It is easy to see that if a fixed point of InferNext is a typeenvironment then it is a valid typing for d. That is,V
T HEOREM 4.1. Suppose ∆ ∈ Θ is a type environment such that
InferNext (∆) = ∆. Then, we have ∆ ⊢ d.

Moreover, it is easy to show that InferNext is monotonic.
V Then, thefollowing theorem is immediate from the fact that Θ is a finite(and therefore, a complete) lattice.

T HEOREM 4.2. The least fixed point ∆ ofVInferNext is a typeenvironment if and only if there exists ∆′ ∈ Θ such that ∆′ ⊢ d.

Therefore, to decide if d is typable with the current candidate set, it suffices V
to compute the least fixed point V∆ =Fi
Θ(F )) and check that ∆(F ) 6= ∅ fori∈ω InferNext (λF.
all F . If such ∆ exists, we stop the CEGAR process and return ∆as the inferred typing for d.
ViOtherwise,
V we have ∆ = InferNext (λF. Θ(F )) such that∆(F ) = ∅ for some F at some iteration i. In this case, we pass
the pair (F, i) as the counterexample to the refinement algorithm
described in Section 5.
E XAMPLE 4.3. Let d consist of the following four functions.
F x y = if x then F y x else G x y
G x y = assert y; F y x
H x = assert x; H xmain () = if true then F true false else H false
Let the current candidate set be Θ shown below.
Θ(main) = {() → ⋆}Θ(F ) = {bool → bool → ⋆,{u:bool | u = true} → {u:bool | u = false} → ⋆}Θ(G) = {{u:bool | u = false} → {u:bool | u = true} → ⋆}Θ(H) = {{u:bool | ⊥} → ⋆}6 Here, ∆’s are allowed to range over non type environments.

VLet ∆0 be the least element of the lattice Θ, that is,VV∆0 = {main V
7→ Θ(main),V
F 7→ Θ(F ),G 7→ Θ(G), H 7→ Θ(H)}Then, InferNext (∆0 ) = ∆1 where∆1 (main) = () → ⋆∆1 (F ) = {u:bool | u = true} → {u:bool | u = false} → ⋆∆1 (G) = {u:bool | u = false} → {u:bool | u = true} → ⋆∆1 (H) = {u:bool | ⊥} → ⋆∆1 is a type environment but ∆1 6= ∆0 . Therefore, iterating one
more time, we get InferNext (∆1 ) = ∆2 where ∆2 (main) =∆1 (main), ∆2 (G) = ∆1 (G), ∆2 (H) = ∆1 (H), but ∆2 (F ) =V∅. Because ∆2 (F ) is not a type, we have reached the fixed pointand can return (F, 2) as the counterexample.

5. Refinement
Recall that the goal of the refinement phase is to check if the counterexample is spurious by constructing a non-recursive programfragment from the counterexample and checking if the fragment istypable, not restricted to any candidate set. And if so, we build new
candidates from the inferred typing, and otherwise, we can reject
the program as untypable.
We separate the refinement phase into the following three subphases, executed in order.
• We take the counterexample (F, i) and unwind the recursive

definitions i times from F to produce a non-recursive programfragment. (Section 5.1)
• We infer the type derivation shape that is sufficient for typing

the unwound fragment via linear intersection type inference.
(Section 5.2)
• Given the linear derivation shape, we generate constraints con-sisting of first-order logic formulas and predicate variables, andcheck if the constraints are satisfiable by using an interpolating theorem prover. If not, then the unwound fragment is untypable, and we stop the CEGAR process declaring the program
untypable. Otherwise, from the typing inferred for the fragment,
we produce new candidate types that are sufficient to refute thecounterexample. (Sections 5.3 and 5.4)
Next, we describe the three sub-phases in detail.
5.1 Unwinding
The unwinding phase is the simplest phase of the refinement process. Given a counterexample (F, i), we inline recursive definitions
i times from F in d, leaving leaf function name occurrences with nodefinitions. The resulting program fragment, d′ , is then guaranteed
to be free of recursive definitions.
We demonstrate the process by unwinding the program d from
Example 4.3. Recall that we are given the counterexample (F, 2).
Then, unwinding produces the following program slice d′ :G1 x y = assert y; F4 y x
F2 x y = if x then F3 y x else G2 x y
F1 x y = if x then F2 y x else G1 x y
Here, F1 , F2 , F3 , F4 , G1 , G2 are inlined function names createdfresh. Note that F3 , F4 , and G2 are leaf functions. We maintainthe mapping Inames that maps the original function names ofd to the set of its inlined copies in d′ . In the above example,
Inames(F ) = {F1 , F2 , F3 , F4 }, Inames(G) = {G1 , G2 }, andInames(H) = Inames(main) = ∅. Note that the unwinding onlycontains functions that are involved in the counterexample, that is,main and H (as well as F and G beyond depth 2) are sliced out.7
We discuss the key properties of unwinding. First, because dis simply typable, d′ is also simply typable, and we assume thatsty (e) is given for each expression e in d′ . Let us extend the typejudgement ⊢ to leaf function name occurrences in the obvious way
by allowing any well-formed type for the function to be assigned.
The following is immediate.
T HEOREM 5.1. Suppose ∆ ⊢ d and d′ is an unwinding of d.
Let ∆′ be a top-level type environment for d′ such that for eachG ∈ Inames(F ), ∆′ (G) = ∆(F ). Then, ∆′ ⊢ d′ .
Therefore, showing that d′ is untypable is sufficient for showingthat d is untypable.
As a contrapositive, we show that the current candidate set isinsufficient for typing d′ , using candidates for the originals for the
inlined functions.
T HEOREM 5.2. Let d′ be the unwinding of d produced from thecounterexample passed from the fixed-point type inference phaseusing the candidate sets Θ. Let Θ′ be a candidate set for d′ such′that for eachV G ∈ Inames(F ), Θ (G) = Θ(F ). Then, there existsno ∆ ∈ Θ′ such that ∆ ⊢ d′ .

The above theorems justify us calling (F, i) a counterexample.
That is, the unwinding d′ produced from (F, i) is a counterexample
to the typability of d under the current candidate set.

isBaseEnv (Γ )sty(x) is baseVaB1Γ; θ ⊢1 x : {u:B | u = x}sty (x) is not baseisBaseEnv (Γ )1

Γ, x:τ ; θ ⊢ x : τ
isBaseEnv (Γ )Cst1Γ; θ ⊢ c : ty(c)VaF1

F is leaf isBaseEnv (Γ )Γ, F :τ ; θ ⊢1 F : τdom(Γ′ ) are all function names isBaseEnv (Γ )→−→ \X; ⊤ ⊢1 e : ⋆F−
x = e ∈ d′Γ′ , −x:σ→−
X = {xi ∈ { x } \ free(e) | sty (xi ) not base}−→ → ⋆; θ ⊢1 F : −−→→⋆Γ, Γ′ , F : −x:σx:σΓ1 ; θ ⊢1∧ e1 : σ Γ2 , x:σ \X; θ ⊢1 e2 : ⋆X = {x | x ∈/ free(e2 ) and sty (x) not base}Γ1 ∧ Γ2 ; θ ⊢1 let x = e1 in e2 : ⋆Γ ⊢1 σ1 ≤ σ1′Γ ⊢1 σ2 ≤ σ2′Γ ⊢1 σ1 ∧ σ2 ≤ σ1′ ∧ σ2′

Fun11

Fun21

Let1

SubI1

Figure 8. The key ⊢1 typing rules.

5.2 Linear Intersection Types
The goal of the rest of the refinement phase is to check if the unwinding d′ is typable, without confining the types of the functions
to any candidate set. An issue here is that the type system allows
unboundedly many intersections, and so we cannot naively derivea type inference algorithm from the type checking rules from Section 2.1. To overcome the issue, we use the observation that only
linear intersections are needed for typing d′ and that the linear intersection “shapes” can be inferred. The crucial properties of d′ thatenable this is that d′ does not contain recursive definitions and issimply typable. Linearity is also important to the constraint solving
phase of the refinement algorithm because it ensures the acyclicityof the generated constraints (cf. Section 5.3).
Informally, in the linear intersection dependent type system ⊢1 ,for a non-base-type binding x : σ, the top-level intersections of σdetermine how the variable x is used. For example, it is possible toderiveΓ2 ; ⊤ ⊢1 if y then x y else x y : ⋆where Γ2 = y : bool, x:(bool → ⋆) ∧ (bool → ⋆), butΓ1 ; ⊤ 6⊢1 if y then x y else x y : ⋆Γ3 ; ⊤ 6⊢1 if y then x y else x y : ⋆where Γ1 = y : bool, x : bool → ⋆ and Γ3 = y : bool, x :(bool → ⋆) ∧ (bool → ⋆) ∧ (bool → ⋆).
Essentially, ⊢1 is equivalent to ⊢ except that it disallows nonlinear use of function-type bindings. The linearity restriction is only
imposed on function types; base types are used non-linearly.
We formally define the type system ⊢1 . The syntax of linear
intersection types is equivalent to that of ⊢ (cf. Figure 5). But
now, ∧ is neither associative, commutative, nor idempotent. We
also modify the typing rules so that the rules in Figure 8 replace
VaB, VaF, Fun, Cst and Let from Figure 6 and SubI1 and
SubI2 from Figure 7. The rest of the rules remain the same, justreplacing ⊢ with ⊢1 , and ⊢∧ with ⊢1∧ . We eliminate any intersectionof base types via the equivalence {u:B | θ1 } ∧ {u:B | θ2 } =7 The implementation performs additional optimizations that can further

reduce the size of the unwinding by slicing out more irrelevant parts.

{u:B | θ1 ∧ θ2 }. As with ⊢, we assume that any type σ assigned
to an expression e satisfies simple(σ) = sty(e).
We discuss the new rules. VaB1 replaces VaB. Here, thecondition isBaseEnv (Γ ) says that all bindings in Γ are base types,that is, dom(Γ) does not contain function names and for all x ∈dom(Γ), Γ(x) is a base type. VaF1 replaces VaF and requires thatthe only function-type binding in the environment is x. Similarly,
Cst1 replaces Cst and requires that Γ contains no function-type
bindings.
Fun11 and Fun21 replace Fun. Fun11 types leaf function
names and is much like VaF1 . Fun21 types non-leaf function
names. (Note that judgements are implicitly parameterized by theunwound fragment d′ .) Unlike Fun, it type checks the body of thefunction in the sub-derivation. Note that this does not lead to an
infinite derivation tree because d′ does not contain recursive defi−→ \ X denotes the bindings −−→ with the bindings
nitions. Here, −x:σx:σfor X removed. We need this because linearity implies that a nonbase-type variable that are not used in e cannot be bound in theenvironment. Let1 similarly takes care of unused non-base variable bindings. Finally, SubI1 replaces SubI1 and SubI2 from
Figure 7. It just structurally applies subtyping inside intersections.
Note that any unwound program fragment has a unique root
function from where the unwinding started and whose name does
not occur free in the unwinding. We define the notion of linearly
typable programs.
D EFINITION 5.3 (Linearly typable programs). Let d′ be an unwound program fragment with F as the root function. Then, we
write ∆ ⊢1 d′ if ∆ ⊢1 F : τ for some τ . (Incidentally, it must be
the case that τ = ∆(F ).)The following theorem states that we can decide if d′ is typableby deciding if d′ is linearly typable.
T HEOREM 5.4. Let d′ be an unwound program fragment. Then,the following are equivalent.
(1) There exists ∆ such that ∆ ⊢1 d′ .
(2) There exists ∆ such that ∆ ⊢ d′ .

We defer the proof to Appendix C.
Unlike ⊢, ⊢1 is completely structural because the shape of a
derivation, including the number of intersections in the types, isdetermined by how variables occur in d′ . To infer the derivation
shape, we adopt the expansion-variable-based inference algorithmof Kfoury and Wells [21], modified so that expansions are not applied to base-type bindings. For space, we refer to their paper [21]for the details of the algorithm. The inferred shape satisfies all thestructural requirements of ⊢1 , that is, everything except for the logical validity premise at SubB.
More precisely, we introduce shape-only types that have holes“−” in place of first-order logic formulas, defined as follows.
τ̂
σ̂

::=
::=

⋆ | {x:B | −} | x: σ̂ → τ̂τ̂ | σ̂1 ∧ σ̂2

Let shape-only type environment Γ̂ be a mapping from variables
and function names to σ̂’s, and top-level shape-only type environˆ be a mapping from functions names to σ̂’s. Then, linear inment ∆tersection type shape inference judgement Γ̂; −⊢ˆ1 e : τ̂ consists of⊢1 rules, but using τ̂ (resp. σ̂) wherever τ (resp. σ) appears, using
the hole − for formulas, and replacing SubB with the followingrule.
Γ̂; −⊢ˆ1 {u:B | −} ≤ {u:B | −}We also replace formulas in constant types ty(c) with holes, prohibit intersection of base types, and use types containing no intersections for the unused bindings X at Fun21 and Let1 . Then, thelinear intersection type shape inference infers a shape-only derivaˆ ⊢ˆ1 d′ . The fact that such a derivation exists is the consetion ∆quence of the fact that d′ is recursion free and is simply typable,8and follows from well-known properties of intersection types (see,e.g., [21]).
The linear intersection type shape inference is non-trivial in thepresence of higher-order functions. In fact, it is known that thecomplexity of the inference is non-elementary time hard [30, 35].
But the expansion-variable-based algorithm appears to work wellin practice, perhaps because functions of high ranks,9 which could
cause the inference to explode, are used sparingly in practice.
5.3 Constraint Generation and Constraint Solving
Having generated the derivation shape for d′ , the next step is tocheck if the shape can be turned into an actual ⊢1 derivation byfilling in the holes with first-order logic formulas. To this end,
we introduce predicate variables that serve as placeholders forfirst-order logic formulas in the derivation. We use large letters
P, Q, etc. to range over predicate variables. We generate constraints
containing predicate variables and formulas from the underlying
theory, and use an interpolating theorem prover to solve for thepredicate variables.
We extend the syntax of dependent types to allow predicate
variables in place of formulas in refinement base types:
ρ
τ

::=
::=

ε | ρ, [x/y]· · · | {u:B | P ρ}

(We overload τ to range over the extended types when it is clear
from the context.) The sequence of substitutions ρ is called pending substitutions [34] (or delayed substitutions [23]). Pending substitutions records the substitutions τ [x/y] made at App so that, forexample, {u:B | P }[x/y] = {u:B | P [x/y]}. (The empty substitution ε is elided.)
8 Actually, typability under any type system that ensures normalization ofrecursion-free terms is sufficient.
9 Roughly, a rank is the number of times a type can be nested in the left
hand side of →.

ˆ ⊢ˆ1 d′ be the inferred derivation shape. ∆ˆ is a mappingLet ∆from non-root functions in d′ to shape-only types. We build a¨ from ∆ˆ such that for each ∆(Fˆ ) = σ̂,function type template ∆¨
we have ∆(F ) = σ where σ is σ̂ with its holes filled with fresh
predicate variables with empty pending substitutions. For example,
from the shapeˆ = {F 7→ x:{u:int | −} → ⋆, G 7→ x:{u:int | −} → ⋆}∆we make the template¨ = {F 7→ x:{u:int | P } → ⋆, G 7→ x:{u:int | Q} → ⋆}∆¨ to emphasize that it may contain
where P 6= Q. (Here, we write ∆predicate variables.)To generate constraints, we convert ⊢1 type checking rules toconstraint generation rules by modifying the base-type subtyping
rule SubB so that instead of checking logical validity, the premise[[Γ]] ∧ θ̈ ∧ θ¨1 ⇒ θ¨2 is recorded as a constraint. Here, we use
the symbol θ̈ to range over formulas possibly containing predicate
variables, (and reserve θ for concrete formulas that do not contain¨ at hand, we
predicate variables). Then, having the template ∆follow the derivation shape and record the constraints that occur ateach SubB instance. Let C be the set of constraints obtained thisway. Note that C is a set of formulas containing predicate variables.
To define a solution for the constraints, we define the scope¨ written scopevars (P ), tovariables of each P in the template ∆,be the set of variables that are allowed to appear free in a solution.
Formally, scopevars is a mapping from predicate variables to thelargest set of variables such that for any mapping S from predicate
variables to concrete formulas with free(S(P )) ⊆ scopevars (P )¨ Here, S(σ) denotes
for all P , S(σ) is closed for all σ ∈ ran(∆).
σ with its predicate variables P replaced by the concrete formula
S(P ). Scope variables can be computed by a linear scan over¨ =the template. For example, scopevars (P ) = {x, u} for ∆{F 7→ x:σ → y:{u:int | P } → ⋆}.
We say that S is a solution for C, written S |= C, if S(P ) ⊆scopevars (P ) for all P and for each θ̈ ∈ C, S(θ̈) is valid. It is¨ ⊢1 d′ where S(∆)¨ iseasy to see that if S is a solution, then S(∆)¨¨
defined {F 7→ S(∆(F )) | F ∈ dom(∆)}.
5.3.1 Least Solution
To solve the constraints, we first compute the least solutions forthe predicate variables. The least solutions are used when computing interpolants in the second phase of the constraint solving (cf.
Section 5.3.2).
Note that each constraint in the generated set of constraints C iseither of the following forms. (Recall that ⇒ binds the weakest.)(1) Ψ ∧ θ ⇒ θ′(2) Ψ ∧ θ ⇒ P ρ
where θ and θ′ do not contain predicate variables and Ψ is aconjunction of predicate variables with pending substitutions:Ψ ::= ⊤ | Ψ ∧ P ρ
Predicate variables appearing in a constraint are guaranteed to be
distinct. Furthermore, C is acyclic in the following sense.
T HEOREM 5.5. The generated set of constraints C does not contain constraints of the form {Pi ρi ∧ θ̈i ⇒ Pi+1 ρ′i | 1 ≤ i ≤ n}for some n ≥ 1 with P1 = Pn+1 .
We defer the proof to Appendix C. The result follows from thefact that the derivation is linear. Indeed, cyclic constraints could be
generated if we had used the simple types to obtain the derivation
shape as seen Example 5.6 below.

Because of acyclicity, we can totally order predicate variables
via topological sort so that if there is a constraint of the formP ρ ∧ θ̈ ⇒ Qρ′ in C, then P < Q.
E XAMPLE 5.6. This example illustrates the importance of linearity
in avoiding cyclic constraints. Let the unwound fragment d′ consistof the following functions.10

sum1 x y k =if x ≤ 0 then k y else sum2 (x − 1) (x + y) k
check1 x =assert (100 ≤ x); check2 x
main1 () =sum1 100 0 check1

H f k = f 0 (G f k)
Gf k x = f x k
F xk=kx
K x = assert x ≤ 0; Kx
main () = H F K

Figure 9. Example 2.4 unwound twice from main.

ˆ ⊢ˆ1 d′ be the inferred linear intersection type shape. Then,
Let ∆
ˆ
∆(H)
= f : τ̂ ∧ τ̂ → k:(x:{u:int | −} → ⋆) → ⋆ˆ
where τ̂ = {u:int | −} → ({u:int | −} → ⋆) → ⋆. From ∆,¨¨
we get the template ∆ such that ∆(H) = f :τ1 ∧ τ2 → . . . whereτ1 = {u:int | P1 } → . . . and τ2 = {u:int | P2 } → . . ., for P1¨ ⊢1 d′ isand P2 fresh. The set of constraints C generated from ∆acyclic, but induces the ordering P1 < P2 . Hence, if we had usedˆ
simple-type shapes so that ∆(H)
= f : τ̂ → . . . instead, then wewould have P1 = P2 , and the constraints become cyclic. 2
Thanks to acyclicity, we can systematically derive the least
solution for C in a bottom up manner, that is, in the ascending orderof <. (Although we call it the least solution, it is an actual solution
only if C is satisfiable.)
We describe the method to obtain the least solution for P having
obtained the least solutions for all Q < P . Let{θ̈1 ⇒ P ρ1 , θ̈2 ⇒ P ρ2 , . . . , θ̈n ⇒ P ρn }be the set of constraints in C of the form θ̈ ⇒ P ρ. We set the least
solution for P to be_
Least (P ) = ∃X. Least (θ̈i )ρ−1
i
i

W

−1
i Least (θ̈i )ρi ) \ scopevars (P ). We explain

where X = free(
the construction. We first concretize each lowerbound θ̈i of P ρi bysubstituting the least solutions for the predicate variables appearing
free in θ̈i . Note that such least solutions are already obtained. Then,
we reverse substitute the pending substitutions ρi to obtain theconcretized lowerbounds for P , that is, Least (θ̈i )ρ−1
for each i.
i
The correctness of the construction requires the targets of ρi to
not occur free in Least (θ̈i ), which can be met by renaming thebound variables in the types. Finally, we take the disjunction of
the concretized lowerbounds, and existentially quantify all freevariables except for the scope variables of P . The latter ensuresthat free(Least (P )) ⊆ scopevars (P ).
The following is immediate from the construction of Least .
T HEOREM 5.7. If C is satisfiable, then Least is the least solution
for C. That is, Least |= C, and for all solutions S such that S |= C,
Least (P ) ⇒ S(P ) for all P .
Thus, to check C’s satisfiability, it suffices to check whether
Least (θ̈) is logically valid for each constraint θ̈ ∈ C. And if so, we¨ ⊢1 d′ , and we can obtain new candidate types fromhave Least (∆)¨¨ is the template obtained from ∆ˆ suchLeast (∆). (Recall that ∆ˆ ⊢ˆ1 d′ .) While this is a sound and complete way to solve C andthat ∆
generate new candidates, it tends to produce suboptimal candidates.
¨ as the new canThere are two problems with using Least (∆)
didates. One problem is that the least solutions may contain existential quantifiers that need to be eliminated before using them ascandidates so that the fixed point type inference phase only needs
to work with quantifier-free formulas.
10 The code is somewhat contrived because of the CPS restriction. The
essence is F being applied to the “return value” of another instance of itself.

The second, more critical, issue is that the least solutions areoften too strong as candidates. We illustrate the problem using thesummation program d from Example 2.4. Suppose we are given
the counterexample (main, 2). Unwinding d twice from main, we
obtain d′ shown in Figure 9. Then, using the least solutions, we¨
obtain the following top-level type environment ∆ = Least (∆).
∆(sum2) =x:{u:int | u = 99} → y:{u:int | u = 100} →({u:int | ⊥} → ⋆) → ⋆∆(sum1) =x:{u:int | u = 100} → y:{u:int | u = 0} →({u:int | ⊥} → ⋆) ∧ ({u:int | ⊥} → ⋆) → ⋆∆(check1) = ({u:int | ⊥} → ⋆) ∧ ({u:int | ⊥} → ⋆)∆(check2) = {u:int | ⊥} → ⋆Note that ∆ says that sum2 (resp. sum1) can only take 99 (resp.
100) as its first argument. Nevertheless, we have ∆ ⊢1 d′ , andso ∆ is sufficient for typing d′ . However, it is too strong to typethe original program. Indeed, if we had used the least solutions tobuild candidates every time, then we would be generating a hundred
candidate types to type the original program.
More generally, the least solutions are too strong when the unwinding is “incomplete,” which is often the case for programs containing recursive functions. We would suffer from the dual problem
had we used the greatest solutions instead, that is, they would be too
weak. To overcome these issues, we use interpolation [11] to find aquantifier-free solution Interp that can be weaker than Least (i.e.,
Least (P ) ⇒ Interp(P )) but is still strong enough to type d′ (i.e.,
Interp |= C).
5.3.2 Interpolants
We compute Interp via interpolation and the least solution Leastobtained by the process in Section 5.3.1. We briefly review the basic
properties of interpolation.
Interpolation Review Given formulas θ1 and θ1 where θ1 ⇒ θ2 ,an interpolant between θ1 and θ2 , written hθ1 , θ2 i, is a formula θsuch that θ1 ⇒ θ, θ ⇒ θ2 , and free(θ) ⊆ free(θ1 ) ∩ free(θ2 ). It is
known that quantifier-free interpolants exist and can be computed
for many useful first-order theories, such as the quantifier-freetheory of linear arithmetic and uninterpreted function symbols [5,20, 27].
Recall the total ordering of predicate variables < from Section 5.3.1. We compute Interp(P ) for each P in the descendingorder of <. We describe how to compute Interp(P ) having computed Interp(Q) for all Q > P . Let{P ρ1 ∧ θ̈1 ⇒ θ̈1′ , P ρ2 ∧ θ̈2 ⇒ θ̈2′ , . . . , P ρn ∧ θ̈n ⇒ θ̈n′ }be the set of constraints in C of the form P ρ ∧ θ̈ ⇒ θ̈′ . We set
Interp(P ) = hLeast (P ), θi if Least (P ) ⇒ θ where^θ=S(θ̈i ⇒ θ̈i′ )ρ−1ii

where S is the substitution such that S(Q) = Interp(Q) if P < Q
and S(Q) = Least (Q) if Q < P . (P is guaranteed to not appearin θ̈i ⇒ θ̈i′ .) Otherwise, Least (P ) 6⇒ θ and we reject d′ , andtherefore also the original program d, as untypable.
We explain the construction of the upperbound θ above. First,
we concretize the upperbound of each P ρi (i.e., θ̈i ⇒ θ̈i′ ) by substituting formulas for the free predicate variables via S. Some free
predicate variables in θ̈i ⇒ θ̈i′ may not have its Interp computed
yet, and so S uses Least for such predicate variables. However,
because of acyclicity, such predicate variables are guaranteed toappear only negatively (i.e., to the left of ⇒). Then, we reverse
substitute ρi to obtain the concretized upperbounds for P , that is,S(θ̈i ⇒ θ̈i′ )ρ−1
for each i. The correctness of the construction rei
quires that the targets of ρi do not occur free in S(θ̈i ⇒ θ̈i′ ), which
can again be ensured by renaming of bound variables. Finally, wetake the conjunction of the concretized upperbounds to obtain θ.
The following theorem states that the above algorithm finds a
correct Interp if and only if C is satisfiable.

It is worth noting that the theorem would hold true even if
Least had been used instead of Interp. Nonetheless, the idea isthat Interp is likely to eliminate other spurious counterexamples
that we would see in future had we used Least instead.

T HEOREM 5.8. The algorithm computes Interp such that Interp |=C if and only if C is satisfiable.

6. Putting Type Inference Components Together

The proof is by induction on the (totally-ordered) predicate variables. See Appendix C for details. Note that because
free(Least (P )) ⊆ scopevars (P ), we have free(Interp(P )) ⊆scopevars (P ) from the property of interpolants.
From the construction, we have Least (P ) ⇒ Interp(P ) for all
P . Although Theorem 5.8 does not imply that Interp 6= Least ,interpolating theorem provers tend to produce small interpolantsthat often work better as candidates than do the least solutions.
Computing without Quantifiers It is possible to compute theinterpolant hLeast (P ), θi by renaming the existentially quantified
variables in the least solutions with fresh variables. This approachis justified by the following lemma and the fact that existential
quantifiers appear only positively in Least (P ) and only negativelyin θ.
L EMMA 5.9. A formula θ is an interpolant between ∃X.θ1 and→(∃Y.θ2 ) ⇒ θ3 if and only if it is an interpolant between θ1 [−
x /X]
→
−
→
−
→
−
and θ2 [ y /Y ] ⇒ θ3 where x and y are fresh variables.
Thus, we can check for the satisfiability of C and obtain a quantifierfree Interp without explicit quantifier elimination by using a theorem prover that can produce quantifier-free interpolants for theformulas in the underlying theory.
5.4 New Candidate Types
Given Interp, we generate the new candidates sufficient for typ¨ ⊢1 d ′ .
ing the counterexample. Recall that we have Interp(∆)′¨ is a mapping from function names in d to their types.
Interp(∆)
Recall that Inames maps the original function names in d to theirinlined copies in d′ .
′We define the
V new candidates Θ as follows: for each F in d,¨Θ′ (F ) = {τi | i τi = Interp(∆)(G)
where G ∈ Inames(F )}.
Then, we pass Θ′ to the fixed-point type inference component
which updates the candidates by Θ := Θ ⊎ Θ′ , where Θ ⊎ Θ′is the point-wise union λF.Θ(F ) ∪ Θ′ (F ). From the property
free(Interp(P )) ⊆ scopevars (P ), the new types are guaranteed
to be closed, and so the updated Θ is a valid candidate set. Fur¨ ⊢ d′ , it follows from Theorem 5.2
thermore, because Interp(∆)
that the updated candidate set is sufficient to eliminate the spurious counterexample from future CEGAR iterations, as stated in thefollowing theorem.
T HEOREM 5.10. Suppose that the lattice of candidates was refinedby refuting the counterexample (F, i). Then, for any counterexample (F, j) reported in future, j > i.

V∃∆∈ Θ.∆⊢dFixed-point
Type Inference

Typable(∆)
Counterexample (F,i)

New Candidates Θ′

Untypable(d′ )¬∃∆.∆⊢d′Refinement

Figure 10. The type inference CEGAR loop.

Figure 10 summarizes our CEGAR-inspired type inference process. The fixed-point type inference algorithm checks if the program d is typable under the current set of candidates Θ′ , and if
so, returns Typable with the inferred typing ∆, and otherwise,passes the counterexample (F, i) to the refinement algorithm. The
refinement algorithm creates the unwinding d′ from the counterexample and decides d′ ’s typability completely. If d′ is found untypable, then the refinement algorithm returns Untypable with thereal counterexample d′ , and otherwise, returns new candidates Θ′that is sufficient for typing d′ . The fixed-point routine refines thecandidates by updating Θ := Θ ⊎ Θ′ , and the CEGAR iteration
repeats.
As remarked before, while the fixed point type inference and refinement algorithms are each guaranteed to terminate, the CEGAR
loop may iterate forever, producing an ever more refined set of candidates. But, the type inference is sound and complete in the sensethat it always returns the correct answer when it terminates.
6.1 Initializing Candidates
The remaining question is about priming the CEGAR loop, that is,
how to pick the initial set of candidates. In principle, any Θ suchthat each Θ(F ) is a finite non-empty set of well-formed types canbe used as the starting set of candidates.
One approach to building a sensible initial Θ is to run the refinement process with artificial counterexamples (F, i) for each F
for some i, and take the point-wise union of Θ′ produced from eachcounterexample as the initial Θ. The implementation discussed in
Section 8 takes this approach with i = 1.
Another possible approach is to heuristically create the initial
candidates by scanning the program text, for example, by using
expressions appearing in branch conditions as the formulas in therefinement base types. This is also the approach taken in Rondon
et al. [34] for building the domain of possible types. Finally, we
may allow the programmer to suggest additional candidates (e.g.,as type annotations).
6.2 Example
Recall the summation program d from Example 2.4. Suppose thatthe current set of candidates is Θ shown below:
Θ(sum) = {int → int → (int → ⋆) → ⋆,{u:int | u ≥ 100} → {u:int | u ≥ 0} →({u:int | u ≥ 100} → ⋆) → ⋆}Θ(main) = {() → ⋆}Θ(check) = {{u:int | u ≥ 100} → ⋆}V
V
Then, InferNext 2 (λF. Θ(F )) = ∆ with ∆(main) = ∅, andso the counterexample (main, 2) is reported. Hence, we unwind
from main twice, and obtain d′ shown earlier in Figure 9.
ˆ such that
Next, linear intersection type shape inference infers ∆ˆ ⊢ˆ1 d′ . From ∆ˆ we obtain the template ∆¨ such that∆¨∆(sum1)=x:{u:int | P1 } → y:{u:int | P2 } →k:(z :{u:int | P3 } → ⋆) ∧ (z :{u:int | P4 } → ⋆) → ⋆¨∆(sum2)=x:{u:int | Q1 } → y:{u:int | Q2 } →k:(z :{u:int | Q3 } → ⋆) → ⋆Programboolflipsum
sum-acm
sum-allmult
mult-cps
mult-allwhere the predicate variables are fresh. (We omit the templates formain1, check1, and check2.) Generating constraints and solving
for the least solutions, we obtain

Programboolflip-esum-esum-acm-e
sum-all-e
mult-emult-cps-e
mult-all-e

Least (P1 ) ⇔ u = 100 Least (Q1 ) ⇔ u = 99
Least (P2 ) ⇔ u = 0
Least (Q2 ) ⇔ u = 100
Least (P3 ) ⇔ Least (P4 ) ⇔ Least (Q3 ) ⇔ ⊥As remarked in Section 5.3.1, these solutions, while correct, arestronger than desired. It is possible, though not guaranteed, for aninterpolating theorem prover to generate Interp such that

Time
0.2
0.1
0.5
0.1
0.6
1.0
0.5

T-TP
95%
97%
98%
93%
99%
98%
98%

T-INT
72%
26%
14%
46%
31%
31%
50%

Candidates
10
6
9
9
6
13
10

Table 1. Experiment results - typable programs.

Time
0.2
2.8
9.9
0.3
13.9
42.1
1.1

T-TP
95%
99%
99%
97%
99%
99%
98%

T-INT
79%
85%
94%
75%
91%
90%
71%

Candidates
8
9
10
9
9
16
10

Table 2. Experiment results - untypable programs.

Interp(Q1 ) ⇔ Interp(Q2 ) ⇔ ⊤Interp(Q3 ) ⇔ u ≥ y¨ we obtain the new candidates Θ′ such that
From Interp(∆),′Θ (sum) = x:int → y:int →({u:int | u ≥ y} → ⋆) → ⋆V
Then, as shown in Example 2.4, there exists ∆ ∈ (Θ ⊎ Θ′ ) suchthat ∆ ⊢ d, and the fixed-point type inference algorithm returns
Typable(∆).

7. Beyond Assertion Checking
We have shown that our system can be used to check the absenceof assertion failures. This section presents an extension that checks
more general program properties specified via user-provided types.
Specifically, we allow the user to provide a mapping Υ from function names to types and ask if there exists a typing ∆ ⊢ d such that∅; ⊤ ⊢ ∆(F ) ≤ Υ(F ) for all F . Such a specification conformancecheck can be handled by a simple extension outlined below. Notethat this can also be used to force the system to infer a typing of adesired precision.
We assume that Υ(F ) is well-formed for each F . We modify the fixed-point type inference algorithm from Section 4 so that
InferNext reports the counterexample (F, i) if it reaches ∆ suchthat ∅; ⊤ 6⊢ ∆(F ) ≤ Υ(F ) at the ith fixed-point iteration. Otherwise, a fixed point ∆ such that for all F , ∅; ⊤ ⊢ ∆(F ) ≤ Υ(F ) isreached and the system declares that d conforms to Υ.
We also extend the refinement algorithm from Section 5 so thatgiven the counterexample (G, i), it unwinds d to get d′ as before,
and then checks if there exists ∆ such that ∆ ⊢ d′ and for all
F , for all F ′ ∈ Inames(F ), ∅; ⊤ ⊢ ∆(F ′ ) ≤ Υ(F ). If so, therefinement algorithm returns new candidates Θ′ constructed fromsuch ∆, and otherwise, declares that d does not conform to Υ.
Note that the additional conditions ∅; ⊤ ⊢ ∆(F ′ ) ≤ Υ(F ) can be
reduced to constraints that can be solved by the constraint solving
algorithm.

8. Implementation and Experiments
We have implemented a prototype of the type inference system,
Depcegar, which takes a subset of Ocaml programs corresponding
to the simple functional language (cf. Figure 2) extended to directstyle syntax. Depcegar handles non-CPS expressions by extending

the type system with conditional types and union types, and handles
non-A-normal forms by online A-normalization [13].
Depcegar is implemented as a modification to the Ocaml 3.10.2
compiler. We use Ocaml’s parser and ML-type inference as thefront-end to parse the program and obtain the simple types.11 We
use CSIsat 1.2 [5] as the interpolating theorem prover. CSIsat supports the quantifier-free first-order theory of uninterpreted function symbols and linear arithmetic (EUF+LA). CSIsat supports realarithmetic but not integer arithmetic, and so integers are approximated as reals in Depcegar (it does not affect the examples inthis paper). For convenience, we use CSIsat both to generate interpolants in the refinement phase and to decide base-type subtyping judgements in the fixed-point type inference phase (i.e., SubB
from Figure 7). The implementation contains about 5000 lines oforiginal code. A web demo of Depcegar and the benchmark programs are available online [36].
We have conducted experiments on small hand-crafted programs, including the ones used as examples in the paper. Table 1
summarizes the results. Here, the first column is the program nameand the second column is the running time in seconds. The column T-TP is the fraction of the running time spent by the interpolating theorem prover CSIsat (both interpolant computation andsubtyping judgements), and the column T-INT is the fraction of therunning time CSIsat spent computing interpolants. The times do
not include the parsing and ML-type inference time. The column
Candidates shows the total number of candidates generated (for all
functions combined). The experiments were conducted on a Intel
Core 2 Extreme 3GHz machine with 2GB of ram, running Linux.
All of the programs in Table 1 are typable. We briefly describe
each program. The program boolflip is the boolean programfrom Example 4.3. The program sum-acm is the summation program from Example 2.4, sum is the same summation program written in direct-style (i.e., without using the accumulation parametery), and sum-all is sum recursively
applied to all non-negative inteP
gers (i.e., it asserts x ≤ i∈{0,...,x} i for all x ≥ 0). The program
mult is the multiplication program from Figure 1, mult-cps is thesame program written in CPS, and mult-all is mult recursively
11 Depcegar does not take advantage of ML’s parametric polymorphism, but

in principle, let polymorphism can be handled by inlining.

applied to all non-negative integers, that is, it replaces the last lineof mult with the following:12
and f y = assert (y <= mult y y); f (y+1)
and main () = f 0
Depcegar was able to successfully infer a typing for each of the
programs. The Candidates column shows that relatively few candidates are generated to type the programs, confirming our hypothesisthat the interpolation-based candidate generation method is quite
effective at generating good candidates.
To test Depcegar on untypable programs, we injected assertions
errors into each of the programs. For example, mult-e replaces thelast line of mult with the following to assert that 600 ≤ 100 × 5:
and main () = assert (600 <= mult 100 5)
and boolflip-e applies F to y y instead of y x inside the body ofF (cf. Example 4.3).
Depcegar successfully detected the type error in all of the programs. Table 2 summarizes the results. Note that the interpolation
fraction T-INT tends to be higher for the untypable programs. Thisis primarily because their run ends during the last refinement phase,whereas for typable programs, the run ends when the last fixedpoint type inference phase has finished. The results also show that
Depcegar quickly detects that boolflip-e (and sum-all-e andmult-all-e) are untypable, but is quite slow on mult-e (andsum-acm-e and mult-cps-e).
More generally, we have observed that while Depcegar can often quickly detect typable programs to be typable by generating
good candidates early in the CEGAR loop, for untypable programs,
it must iterate the CEGAR loop long enough until a real counterexample is encountered. This may result in a large unwinding for a
type error that only occurs “deep” in the program. A similar issue occurs in CEGAR-based model checking when detecting errorsthat take many steps from the initial state to reach [2, 25]. One possible remedy is to multiply the unwinding depth by an increasing
factor as the CEGAR loop progresses. We leave for future work toaddress the issue in a more depth.
We also observe that Depcegar’s running times are almost completely dominated by that of theorem proving, with a non-negligible
fraction dedicated to computing interpolants. As discussed in Section 9.3, interpolating theorem provers are fairly new technology
and are actively being researched. Hence, we expect the runningtimes to improve as interpolating theorem provers mature. A possible optimization is to use a faster, non-interpolating theorem proverfor deciding subtyping judgements and use an interpolating theorem prover only for computing interpolants.
Finally, we note that while the interpolation-based refinement
guarantees the elimination of the given spurious counterexample,
it does not guarantee the convergence of our system on all typable
programs.13 An interesting future research direction is to investigate a more complete approach to candidate generation.

9. Related Work
9.1 Inferring Dependent Types
Inferring complex types via fixed-point type inference iteration isa classic idea. For instance, Freeman and Pfenning [14] infers thestrongest refinement types given a user-provided lattice of refinement types. The recent work by Rondon et al. [34] can be casted
as an instance of this approach to dependent types. Their systemchooses a finite set of candidate formulas by a syntactic scan of

the program text and the user-provided set of formulas, and infers
the strongest types within the lattice of dependent types confined tothese formulas via fixed-point iteration and theorem proving, similar to the fixed-point type inference phase of our system. Lacking
automatic refinement, these approaches require the lattice of candidate types to be pre-defined and be of finite height. In contrast, oursystem automatically infers candidate types within an infinite domain of types (i.e., unbounded intersections and arbitrary formulas)
via counterexample analysis.
One advantage of our approach is that the type inference becomes complete. That is, when the system declares the program
to be untypable, the user is assured that it is actually untypable
rather than wondering if more candidates were needed. A consequence of this is that the inferred types may not be the strongest.
But, this is generally unavoidable as the strongest types may noteven be finitely expressible within the underlying theory, as in, forexample, the mult program from Figure 1. However, as remarked
in Section 7, the system can be made to infer types of the userspecified strength.
Concurrent to our work, Unno and Kobayashi [37] have proposed to infer dependent types via interpolation and iterative unrolling of recursive constraints. Chin et al. [6, 7] have also suggested a constraint unrolling approach with the Omega test [33] as
the backend solver. These approaches use neither candidate types
nor a fixed-point type inference routine, but they resemble the refinement phase of our work in that they also reduce the inference problem to finding a solution to a set of first-order logic constraints. One issue with these purely constraint-based approaches isthe presence of “false constraint cycles” like the one shown in Example 5.6.14 In contrast, our approach divides type inference into
the fixed-point type inference phase and the constraint-solving refinement phase so that the latter is able to leverage unwinding andlinear intersection types to ensure constraint acyclicity.
We note that none of the previous systems listed above supports
unbounded intersection types. To the best of our knowledge, oursystem is the first dependent (or refinement) type inference systemthat can infer unbounded intersection types embedded with arbitrary formulas from a first-order theory.

9.2 Inferring Intersection Types
The success of our system owes much to intersection types. Not
only do intersection types make the underlying dependent typesystem more expressive by being able to type more safe programs,
they are also crucial to the refinement phase of the system that uses
linear intersection type inference [21] to infer a derivation shapethat is sufficient for ensuring both type inference completeness andconstraint acyclicity.
Linear intersection type inference cannot be applied directly
to programs containing recursive definitions as linear intersection
types are not even defined for such programs. Our approach circumvents the issue by iteratively producing non-recursive programfragments as counterexamples, and then checking if the candidate
types inferred for the fragments are also sufficient for typing theoriginal, recursive program.
In our system, intersection types are restricted to only intersect
types of the same simple-type shape, but intersection type inference
algorithms are capable of inferring arbitrary intersection of types,
as well as inferring principal typing [38], which we also do not
utilize in this work. We leave for future work to capitalize on thefull potential of intersection type inference.

12 Depcegar does not handle arithmetic overflows.
13 However, it is trivial to show that the system is guaranteed to converge on
programs with only finitary-data base types (e.g., just booleans).

14 For [6, 7], if extended to higher-order functions.

9.3 Model Checking
Counterexample-guided abstraction refinement has been used withgreat success in hardware and software model checking (see, e.g.,[3, 9, 16]). However, most of the existing software model checkers
only target low-level imperative programs such as device drivers
written in C, and are unsuitable for functional programs because
they cannot accurately model higher-order functions and function
closures.
Recently, researchers have proposed model checking algorithms
for typed higher-order functional programs by leveraging theirequivalence to higher-order pushdown systems [24, 31]. However,these algorithms only handle finite data domains, whereas our system supports infinite data domains such as integers by utilizing aninterpolating theorem prover.
Interpolation has found various applications in model checking,such as predicate abstraction [15, 18] and reachable state approximation [26, 28]. We have shown that interpolation is also quite
effective for inferring dependent types. Algorithms for computinginterpolants for various theories are actively being researched (e.g.,[5, 8, 17, 20]). As future work, we plan to extend our system toother data types, such as lists and arrays, by using interpolating
theorem provers for their theories.

10. Conclusion
We have presented a new approach to inferring dependent types.
The key to the success is the iterative refinement of candidate dependent types via counterexample analysis, utilizing linear intersection type inference and interpolation. We have shown that theapproach enables a sound and complete type inference of an expressive dependent type system that allows unbounded intersection
types embedding arbitrary formulas from a first order theory.

References[1] L. Augustsson. Cayenne - a language with dependent types. In ICFP,
pages 239–250, 1998.

[14] T. Freeman and F. Pfenning. Refinement types for ML. In PLDI, pages
268–277, 1991.
[15] T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, pages 232–244, 2004.
[16] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pages 58–70, 2002.
[17] H. Jain, E. M. Clarke, and O. Grumberg. Efficient Craig interpolation
for linear Diophantine (dis)equations and linear modular equations. In
CAV, pages 254–267, 2008.
[18] R. Jhala and K. L. McMillan. Interpolant-based transition relation
approximation. In CAV, pages 39–51, 2005.
[19] T. Johnsson. Lambda lifting: Transforming programs to recursive
equations. In FPCA, pages 190–203, 1985.
[20] D. Kapur, R. Majumdar, and C. G. Zarba. Interpolation for data
structures. In SIGSOFT FSE, pages 105–116, 2006.
[21] A. J. Kfoury and J. B. Wells. Principality and type inference forintersection types using expansion variables. Theor. Comput. Sci.,
311(1-3):1–70, 2004.
[22] K. Knowles and C. Flanagan. Compositional reasoning and decidable
checking for dependent contract types. In PLPV, pages 27–38, 2009.
[23] K. W. Knowles and C. Flanagan. Type reconstruction for generalrefinement types. In ESOP, pages 505–519, 2007.
[24] N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416–428, 2009.
[25] D. Kroening and G. Weissenbacher. Counterexamples with loops forpredicate abstraction. In CAV, pages 152–165, 2006.
[26] K. L. McMillan. Interpolation and SAT-based model checking. In
CAV, pages 1–13, 2003.
[27] K. L. McMillan. An interpolating theorem prover. Theor. Comput.
Sci., 345(1):101–121, 2005.
[28] K. L. McMillan. Lazy abstraction with interpolants. In CAV, pages
123–136, 2006.
[29] P. M. Neergaard. Theoretical pearls: A bargain for intersection types:
a simple strong normalization proof. J. Funct. Program., 15(5):669–
677, 2005.

[2] T. Ball, O. Kupferman, and M. Sagiv. Leaping loops in the presenceof abstraction. In CAV, pages 491–503, 2007.

[30] P. M. Neergaard and H. G. Mairson. Types, potency, and idempotency:
why nonlinearity and amnesia make a type system work. In ICFP,
pages 138–149, 2004.

[3] T. Ball and S. K. Rajamani. The SLAM project: debugging system
software via static analysis. In POPL, pages 1–3, 2002.

[31] C.-H. L. Ong. On model-checking trees generated by higher-orderrecursion schemes. In LICS, pages 81–90, 2006.

[4] J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis.
Refinement types for secure implementations. In CSF, pages 17–32,
2008.

[32] X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing withdependent types. In IFIP TCS, pages 437–450, 2004.

[5] D. Beyer, D. Zufferey, and R. Majumdar. CSIsat: Interpolation for
LA+EUF. In CAV, pages 304–308, 2008.
[6] W.-N. Chin and S.-C. Khoo. Calculating sized types. Higher-Orderand Symbolic Computation, 14(2-3):261–300, 2001.
[7] W.-N. Chin, S.-C. Khoo, and D. N. Xu. Extending sized type withcollection analysis. In PEPM, pages 75–84, 2003.
[8] A. Cimatti, A. Griggio, and R. Sebastiani. Efficient interpolant generation in satisfiability modulo theories. In TACAS, pages 397–412,
2008.
[9] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith.
Counterexample-guided abstraction refinement. In CAV, pages 154–
169, 2000.
[10] J. Condit, M. Harren, Z. R. Anderson, D. Gay, and G. C. Necula.
Dependent types for low-level programming. In ESOP, pages 520–
535, 2007.

[33] W. Pugh. The Omega test: a fast and practical integer programmingalgorithm for dependence analysis. In SC, pages 4–13, 1991.
[34] P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI,
pages 159–169, 2008.
[35] R. Statman. The typed lambda-calculus is not elementary recursive.
Theor. Comput. Sci., 9:73–81, 1979.
[36] T. Terauchi. Dependent types from counterexamples, 2009.
http://www.kb.ecei.tohoku.ac.jp/∼terauchi/.
[37] H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP, pages 277–288, 2009.
[38] J. B. Wells. The essence of principal typings. In ICALP, pages 913–
925, 2002.
[39] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38–94, 1994.
[40] H. Xi and F. Pfenning. Dependent types in practical programming. In
POPL, pages 214–227, 1999.

[11] W. Craig. Linear reasoning. a new form of the Herbrand-Gentzen
theorem. J. Symb. Log., 22(3):250–268, 1957.
[12] C. Flanagan. Hybrid type checking. In POPL, pages 245–256, 2006.

A. Simple Type System[13] C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence ofcompiling with continuations. In PLDI, pages 237–247, 1993.

We formally present the simple type system. The syntax of simple
types is defined by the following grammar: (Also shown in Sec-Γ ⊢s F : Γ(F ) Γ ⊢s c : simple(ty (c))Γ ⊢s e : boolΓ ⊢s x : Γ(x) Γ ⊢s assert e : ints′sΓ ⊢s e1 : s Γ, x:s ⊢s e2 : ⋆ Γ ⊢ e : s → s Γ ⊢ y : sΓ ⊢s let x = e1 in e2 : ⋆Γ ⊢s e y : s ′Γ ⊢s x : bool Γ ⊢s e1 : ⋆ Γ ⊢s e2 : ⋆Γ ⊢s if x then e1 else e2 : ⋆Figure 11. The simple type system type checking rules.

C[(st ℓ in λp.e) q] →β
C[st ℓ :: (b = q) in e[b/p]]
C1 [let a = e in C2 [(st ℓ in λp.e′ ) a]] →βC1 [let a = e in C2 [st ℓ :: (b = e) in e′ [b/p]]]
C1 [st ℓ1 :: a = e :: ℓ2 in C2 [(st ℓ in λp.e′ ) a]] →βC1 [st ℓ1 :: a = e :: ℓ2 in C2 [st ℓ :: (b = e) in e′ [b/p]]]C1 [let a = e in C2 [a x]] →β C1 [let a = e in C2 [e x]]
C1 [st ℓ1 :: a = e :: ℓ2 in C2 [a x]]→β C1 [st ℓ1 :: a = e :: ℓ2 in C2 [e x]]
Figure 12. The →β reduction rules.

tion 2.1.)
B
s

::=
::=

int | bool
⋆ | B | s → s′Figure 11 shows the type checking rules. Here, we overload thesymbols Γ and ∆ to range over mappings to simple types.
D EFINITION A.1 (Simply-typed program). Let ∆ be a top-level
simple type environment. We write ∆ ⊢s d if for each function→→ ⊢s e : ⋆ where ∆(F ) = −→ → ⋆.
F−x = e ∈ d, we have ∆, −x:sx:s
We say that a program d is simply-typed if there exists ∆ suchthat ∆ ⊢s d.
The simple type of a sub-expression e of d, sty(e), is defined
to be the type assigned to the (unique) occurrence of e in thederivation ∆ ⊢s d.
The following theorem is the standard type safety result thatsays that a simply-typed program does not get stuck, which can beproven via the standard method [39]. (Recall that due to CPS, aprogram does not return.)
T HEOREM A.2 (Simple Type Safety). Let d be simply-typed andmain () = emain ∈ d. Then, for any e such that emain →∗d e, either
e →d fail or there exists e′ such that e →d e′ .

B. Sound Constant Types
For a constant operation c over booleans and/or integers, we say−−→that the dependent type τ = x:B → {u:B | φ} is sound if thefollowing properties all hold:• τ is closed.
• simple(τ ) = sty (c).

→→→→• For any −v in the input domain of c, φ[−v /−x ][[[c]](−v )/u] islogically valid.
Sound types for boolean and integer constants are defined analogously. For example, a sound type for the constant c of the basetype B is {u:B | u = c}.
While a constant operator in our language accepts all inputs in
its domain, behaviors such as the divide-by-0 error can be modeledby inserting appropriate assert statements.

C. Proofs of Key Results
We prove Theorem 5.4, Theorem 5.5, and Theorem 5.8. To facilitate the proofs of Theorem 5.4 and Theorem 5.5, we define a β
reduction like semantics for unwound program fragments.

First, we update the syntax of the language so that λ abstractions
are used to denote functions and function closures:
e
x
ℓ

::=
|
::=
::=

x | c | F | λp.e | e x | let a = e1 in e2
if x then e1 else e2 | assert e | st ℓ in e2
p|a
−
−→e
a−=

(For convenience, we overload the meta variable e to range overthe expressions in the updated syntax.) We separate variables to
two kinds: stack variables, ranged over by symbols a, b, etc., andparameter variables, ranged over by symbols p, q, etc. Symbols x,
y, etc. range over both kinds. Stack variables are bound at let and−→e in e
the new construct st. Conceptually, the expression st −
a−=
−
−
−
→
represents a function-call stack frame with the stack a = e, and theprogram counter e. We use stacks instead of explicit substitution sothat we can type intermediate states via the App and If rules as
they require a variable for the argument and the branch condition.
Stack frames are also used to mark function bodies to avoid basetype variables in the parent context from affecting their typing.
We translate an unwound fragment d′ to its representation in
the updated syntax lam(d′ ) by replacing all non-leaf functions
with the equivalent λ representation enclosed in an empty stack
frame, and replacing all let-bound variables with a fresh stack→variable. More formally, for F −x = e ∈ d′ , we define lam(F ) =→→→→st ε in λ−p .lam(e[−p /−x ]) where −p are fresh, and lam(e) isdefined inductively as e with all its non-leaf free function nameG replaced by lam(G) and all let bindings let x = e1 in e2
replaced by let a = e1 in e2 [a/x] for a fresh stack variable a.
→(Here, ε denotes the empty sequence, and λ−x .e is a short hand for→
λx1 .λx2 . . . . λxn .e where −x = x1 , x2 , . . . , xn .) Then, we definelam(d′ ) = lam(F ) where F is the root function of d′ . Note that
only the leaf functions of d′ may appear free in lam(d′ ).
We define normal forms, ranged over by nf , by the grammar
below:→→→
nf ::= x | p −x | c−x |F−
x | λp.nf | st nℓ in nf

nℓ

|
|
::=

let a = nf 1 in nf 2 | assert nf
if x then nf 1 else nf 2−−−−→
a = nf

Let C range over any expression context. Figure 12 defines
the “β reduction” semantics for expressions in the updated syntax.
Intuitively, these rules implement the usual β reduction, but using
stacks instead of explicit substitutions. In the first three rules, thestack variable b appearing to the right of →β is fresh (i.e., it does
not appear free to the left). The first three rules, differing only on
whether the variable a (or q) is a parameter variable, let-bound or
st-bound, applies the function st ℓ in λp.e to the argument a (orL EMMA C.5. Let d′ be an unwound program fragment. Then,∃∆.∆ ⊢ d′ if and only if ∃∆.∆; ⊤ ⊢ lam(d′ ), and ∃∆.∆ ⊢1 d′ if
and only if ∃∆.∆; ⊤ ⊢ lam(d′ ).

Γ, p:σ; θ ⊢ e : τLamΓ; θ ⊢ λp.e : p:σ → τFor each i.Γ; θ ⊢∧ ei : σia1 :σ1 , . . . , an :σn ; ⊤ ⊢ e′ : ⋆Γ; θ ⊢ st a1 = e1 , . . . , an = en in e′ : ⋆Γ, p:σ \X; θ ⊢1 e : τ
X = {p | p ∈/ free(e) and sty(p) not base}1

Γ; θ ⊢ λp.e : p:σ → τ

Proof: By induction on the structure of d′ . 2
It is easy to show the preservation result for the dependent typesystem ⊢, again via the standard method [39].

St

L EMMA C.6. If Γ ⊢ e : ⋆ and e →β e′ , then Γ ⊢ e′ : ⋆.
Lam1

For each i.Γ; θ ⊢1∧ ei : σia1 :σ1 , . . . , an :σn \X; ⊤ ⊢1 e′ : ⋆X = {ai | ai ∈/ free(e) and sty (ai ) not base}
Γ; θ ⊢1 st a1 = e1 , . . . , an = en in e′ : ⋆St1

Figure 13. Dependent type checking rules for the extended expressions.

Now, let us cast the extended ⊢1 type rules as constraint generation rules by modifying the SubB rule just as we have done
for the original set of rules in Section 5.3. We show that the generate set of constraints coincides for d′ and lam(d′ ). For convenience, we assume that the derivation is modified so that the constraint generated by each subderivation is written explicitly as in
Γ; φ ⊢1 e : τ ; C where C is the set of constraints generated by thederivation Γ; φ ⊢1 e : τ . To generate constraints from lam(d′ ), it
suffices to just make fresh predicate variables appear everywhere in
the argument type σ at Lam1 .
The following theorem states that constraints generated from d′
is equivalent to those generated from lam(d′ ).

q). The last two rules, differing only on whether the variable a is
let-bound or st-bound, substitutes a with e.
Note that the semantics do not reduce conditionals, asserts,
constant applications, nor leaf function applications, but reducesuser-defined function applications everywhere. It is easy to see thata normal form cannot be reduced, i.e.,

L EMMA C.7. Let C be the set of constraints generated from ∆ ⊢1d′ . Then, we have ∆ \ {F | F is not leaf}; ⊤ ⊢1 lam(d′ ) : ⋆; C.

L EMMA C.1. For any normal form nf , there exists no e such thatnf →β e.

T HEOREM 5.4. Let d′ be an unwound program fragment. Then,the following are equivalent.

We update the simple type system ⊢s in a straightforward way
to the extended syntax by adding the rules below.

(1) There exists ∆ such that ∆ ⊢1 d′ .
(2) There exists ∆ such that ∆ ⊢ d′ .

Proof: By induction on the structure of d′ . 2
C.1 Theorem 5.4

L EMMA C.2. Let d′ be an unwound program fragment. Then,∃∆.∆ ⊢s d′ if and only if ∃∆.∆ ⊢s lam(d′ )By Lemma C.5, it suffices to show that the typability of lam(d′ )coincides for ⊢1 and ⊢. (1) ⇒ (2) is trivial because any ⊢1 typing
derivation is a valid ⊢ derivation that just does not use function typebindings non-linearly.
We prove (2) ⇒ (1) by showing that any strongly-normalizing⊢ typable terms are ⊢1 typable. Then, because any lam(d′ ) isstrongly normalizing by Lemma C.4 anyway, it follows that any⊢ typable term is ⊢1 typable.
For a free non-base type stack variable a in nf , we write
I(a, nf ) for the set of types σ such that simple(σ) = sty (a)and the top level linear intersections of σ matches the occurrencesof a in nf . For example,

Proof: By induction on the structure of d′ . 2

I(a, λp.p a a) = {τ ∧ τ ′ | simple(τ ) = simple(τ ′ ) = sty (a)}It can be shown that ⊢s typing is preserved across →β using thestandard method [39].

For a type environment Γ, let I(Γ, nf ) be the set of type environments Γ′ that maps all base-type variables and (non-basetype) stack variables in dom(Γ) (i.e., it does not map non-basetype parameter variables and function names) such that Γ′ (a) ∈I(a, nf ) for a ∈ dom(Γ) a non-base-type stack variable and′ΓV(x) = h|Γ(x)|i for x ∈ V
dom(Γ) a base type variable, whereh| i {u:B | θi }|i = {u:B | i θi }. Essentially, Γ′ ∈ I(Γ, nf ) isa type environment that is equivalent to Γ for base-type variables
and has arbitrary well-shaped types for non-base-type stack variables.
We now show that any ⊢ typable normal form is ⊢1 typable
under such an environment.

Γ, p:s ⊢s e : s′Γ ⊢s λp.e : s → s′
For each i.Γ ⊢s ei : si
a1 :s1 , . . . , an :sn ⊢s e′ : ⋆Γ ⊢ st a1 = e1 , . . . , an = en in e′ : ⋆St

The next lemma states the expected, that is, simple typability ofd′ and lam(d′ ) coincides.

L EMMA C.3. If Γ ⊢s e : ⋆ and e →β e′ , then Γ ⊢s e′ : ⋆.
Also, by the standard strong normalization result for the simply
typed λ calculus, we have that →β is strongly normalizing forsimply typable terms. (See, e.g., [29].)
L EMMA C.4. Suppose Γ ⊢s e : ⋆. Then, e strongly normalizes tosome normal form.
Henceforth, we assume that any expression is simply typed, andthat its simple type, sty (e), is available.
We also update the dependent type system ⊢ and ⊢1 to theextended expressions so that the typability of d′ and lam(d′ ) also
coincides there. Formally, we add the rules shown in Figure 13.
Note that the typing rules for a stack frame (St and St1 ) ignoresthe parent’s environment assumption.
We restate the expected property as a lemma.

L EMMA C.8. Suppose Γ; ⊤ ⊢∧ nf : σ. Let Γ′ ∈ I(Γ, nf ).
Then, there exists Γ′′ ⊇ Γ′ and σ ′ such that Γ′′ ; ⊤ ⊢1∧ nf : σ ′ ,simple(σ ′ ) = simple(σ), and if σ is a base type, σ ′ = h|σ|i.
Proof: By induction on the structure of nf . The case nf is a variable→→
is trivial. For the case nf is p −x (resp. F −x ), we set Γ′′ (p) (resp.

Γ′′ (F )) appropriately so that it is a function taking the arguments of→the type Γ′ (−x ) (if an argument is also a function-type parametervariable or a function name, then it too can be set to be of any
appropriate type).
→
The case nf is c −x follows from the sound constant type assumption (cf. Section B) that all arguments to a constant operator
are of base types. The case nf is a lambda abstraction follows trivially from the induction hypothesis.
For the case nf is a let expression let a = nf 1 in nf 2 , we split
on whether sty (a) is a function type or not, and apply induction
hypothesis. The case nf is a stack frame stnℓinnf ′ is similar. The
case nf is an assert expression or a conditional expression follows
from induction hypothesis and the fact that asserted expressions
and branch conditions are always of base types. 2
Next, we show the “subject-expansion” property.
L EMMA C.9. Suppose e1 →β e2 , Γ0 ; φ ⊢ e1 : ⋆, and Γ; φ ⊢1 e2 :⋆. Then, there exists Γ′ such that Γ′ ; φ ⊢1 e1 : ⋆.
Proof: We prove by case analysis on the reduction kinds. For thecase the reduction is one of the first three rules in Figure 12, we
type e1 by setting the type of the parameter variable p to be thetype of b in the typing for e2 .
The case the reduction is one of the last two rules in Figure 12
follows trivially from the inspection of the rules St1 and Let1 . 2
By Lemmas C.4,C.6,C.8, and C.9, it follows that if ∆; ⊤ ⊢ e : ⋆then there exists ∆′ such that ∆′ ; ⊤ ⊢1 e : ⋆. This proves (2) ⇒(1).
C.2 Theorem 5.5
T HEOREM 5.5. The generated set of constraints C does not contain constraints of the form {Pi ρi ∧ θ̈i ⇒ Pi+1 ρ′i | 1 ≤ i ≤ n}for some n ≥ 1 with P1 = Pn+1 .
By Lemma C.7, it suffices to show that lam(d′ ) generates
acyclic constraints. Because we are only concerned with constraintgeneration in this section, we assume that ⊢1 judgements andderivations are that of constraint generation and not type checking. Recall that constraint generation judgements have the form
Γ; φ ⊢1 e : τ ; C where C is the set of constraints generated by
the derivation (cf. Section C). Also, for readability, we elide the¨ etc., which was used in the main body
decorated notation θ̈, τ̈ , ∆,of the paper to emphasize the fact that the object may contain predicate variables, and simply use the non-decorated version θ, τ , ∆,etc.
We prove the theorem semantically, like (2) ⇒ (1) of Theorem 5.4. This time, we show that any strongly normalizing(w.r.t. →β ) expression generates acyclic constraints. Then, the result follows from Lemma C.4 which says that any unwound program fragment is actually strongly normalizing.
In a spirit similar to the construction of I(Γ, nf ) from Section C.1, for a normal form nf , let I(nf ) be the set of type environments Γ mapping base-type variables (both parameter and stack)and non-base-type stack variables free in nf to arbitrary types of
the correct linear shape. For example,
I(λp.p a a)
= {{a 7→ τ ∧ τ ′ } | simple(τ ) = simple(τ ′ ) = sty(a)}We now show that the set of constraints generated from a normal
form expression under such an environment is acyclic.
L EMMA C.10. Let Γ ∈ I(nf ) and C be any acyclic set of constraints. Then, there exists Γ′ ⊇ Γ and τ ′ such that Γ′ ; φ ⊢1 nf :
τ ′ ; C ′ and C ∪ C ′ is acyclic.
Proof: By induction on the structure of nf . The case nf is a variable→→
is trivial. The cases nf is an application p −x (resp. F −x ) holds byletting the type of p (resp. F ) in Γ′ to be of a type containing fresh
predicate variables everywhere (i.e., distinct, and not in Γ or C).
Note that p ∈/ dom(Γ) because p is a function-type variable. The→
constant application case c −x is trivial.
The case nf is a lambda abstraction follows trivially from induction hypothesis. The case nf is a stack frame or a let expressionis also straightforward from induction hypothesis, instantiating C to
be the constraints from the other subterms. The case nf is an assert
expression or a conditional expression is similar. 2
Note that the lemma implies that constraints C generated froma program-level environment (i.e., ∆; ⊤ ⊢1 nf : ⋆; C for ∆ withfresh predicate variables everywhere.) is acyclic.
Given constraints C we say that there is an edge from P to Q
if there exists a constraint of the form P ρ ∧ θ ⇒ Qρ′ ∈ C. We
say that there is a path from P to Q if there exists a non-empty
sequence of edges connecting P to Q. Note that C is acyclic if andonly if there exists no path connecting a predicate variable to itself.
We now show the “subject-expansion” property.
L EMMA C.11. Suppose e1 →β e2 , and Γ; φ ⊢1 e2 : ⋆; C with C
acyclic. Then, there exists Γ′ such that Γ′ ; φ ⊢1 e1 : ⋆; C ′ with C ′acyclic.
Proof: We prove by case analysis on the reduction kinds. For the
first three rules in Figure 12, we use fresh predicate variables forthe type of the argument p.
Then, it can be shown that C ′ comprises of the predicate variables in C and the fresh predicate variables from the type of p. The
new constraints from the function application in e1 do not induce
new paths in C ′ between variables that are in C, and that there are
no edges directly connecting the new predicate variables appearing
in the type of p. Thus, C ′ is acyclic.
The case the reduction is one of the last two rules follows
trivially from the inspection of the rules St1 and Let1 . 2
Lemma C.10 and Lemma C.11 imply that constraints generated from any strongly normalizing e is acyclic. Therefore, byLemma C.7 and Lemma C.4, we have proven Theorem 5.5.
C.3 Theorem 5.8
T HEOREM 5.8. The algorithm computes Interp such that Interp |=C if and only if C is satisfiable.
The only if direction is trivial. We prove the if direction. We
enumerate the predicate variables as P1 , . . . , Pn where Pi < Pi+1
for 1 ≤ i < n. (Recall that predicate variables are totally ordered.)
Let S be a mapping from predicate variables to formulas. Forj, k ≤ n, we define Sjk to be the following mapping:(
Least (Pi ) if i < jkSj (Pi ) =S(Pi )
if k < i(Sjk (Pi ) is undefined for j ≤ i ≤ k.) Recall that a predicate
variable can occur at most once in any constraint θ̈ ⇒ θ̈′ ∈ C.
For each Pi , let Φi ⊆ C be the set of constraints of the form
Pi ρ ∧ θ̈ ⇒ θ̈′ .
Let us write Ok i (S) if for all j ≥ i, we have Least (Pj ) ⇒S(Pj ) and S(Pj ) ⇒ (Sjj (θ̈) ⇒ S(θ̈′ ))ρ−1 for all Pj ρ ∧ θ̈ ⇒ θ̈′ ∈Φj . Note that S such that Ok 1 (S) is exactly Interp.
The following lemma shows that if C is satisfiable, then thealgorithm is able to compute some Interp.
L EMMA C.12. Suppose Least |= C. Then, there exists S such thatOk 1 (S).
Proof: We prove Ok i (S) for all i by induction in descending order.

Base case
We show that there exists S such that Ok n (S). Pick Pn ρ ∧ θ̈ ⇒
θ̈′ ∈ Φn . By the property of the ordering <, it must be the case thatθ̈′ is concrete. Then, because Least |= C, we have Least (Pn )ρ ⇒(Least (θ̈) ⇒ θ̈′ )ρ−1 . So, there exists an interpolant S(Pn ) =hLeast (Pn ), (Least (θ̈) ⇒ θ̈′ )ρ−1 i and we have Ok n (S).
Inductive case
Let S be such that Ok j (S) for all j > i (by definition the same S
can be used for all such j). We show that there exists S ′ such that
Ok i (S ′ ).
Pick Pi ρ ∧ θ̈ ⇒ θ̈′ ∈ Φi . Let k > i be the smallest k such that
Pk appears in θ̈. The following is a tautology.
kLeast (Pi )ρ ⇒ (Sik (θ̈) ∧ (Si+1(Pi ρ ∧ θ̈) ⇒ S(θ̈′ )) ⇒ S(θ̈′ ))Let Pk ρk ∧ θ̈k = θ̈. By induction hypothesis, we have S(Pk )ρk ⇒k(Si+1(Pi ρ ∧ θ̈k ) ⇒ S(θ̈′ )). Therefore, we have
Least (Pi )ρ ⇒ (Sik (θ̈) ⇒ S(θ̈′ ))Let S ′ (Pi ) = hLeast (Pi ), (Sik (θ̈) ⇒ S(θ̈′ )ρ−1 i and S ′ (Pj ) =S(Pj ) for all j > i. Then, Ok i (S ′ ).
Now suppose no such k > i exists. Because Least |= C,
we have Least (Pi )ρ ⇒ (Least (θ̈) ⇒ Least (θ̈′ )). By induction
hypothesis, we have Least (θ̈′ ) ⇒ S(θ̈′ ). Therefore,
Least (Pi )ρ ⇒ (Least (θ̈) ⇒ S(θ̈′ ))And we can set S ′ (Pi ) = hLeast (Pi ), (Least (θ̈) ⇒ S(θ̈′ ))ρ−1 i
and S ′ (Pj ) = S(Pj ) for all j > i, and get Ok i (S ′ ). 2
To complete the proof of the theorem, we show that Interp
obtained this way (i.e., Ok 1 (Interp)) is actually a solution for C.
L EMMA C.13. Suppose Ok 1 (S). Then, for all i, S |= Ψi .
Proof: We prove by induction on i in ascending order.
Base case
For i = 1, the result follows trivially from the definition of
Ok 1 (S).
Inductive case
Pick Pi ρ ∧ θ̈ ⇒ θ̈′ ∈ Φi . It suffices to show that S(Pi ) ⇒ S(θ̈ ⇒θ̈′ )ρ−1 .
Let k < i be the largest k such that Pk appears in θ̈. Let
Pk ρk ∧ θ̈k = θ̈. The following is a tautology.
S(Pi )ρ ⇒ ((S(θ̈) ∧ (S(Pi ρ ∧ θ̈k ) ⇒ S(θ̈′ )) ⇒ S(θ̈′ ))By induction hypothesis, we also have S(Pk )ρk ⇒ (S(Pi ρ ∧θ̈k ) ⇒ S(θ̈′ )). Therefore, S(Pi ) ⇒ S(θ̈ ⇒ θ̈′ )ρ−1 .
Now, suppose no such k < i exists. Then, we have S(Pi ) ⇒S(θ̈ ⇒ θ̈′ )ρ−1 by the definition of Ok 1 (S).
2Finally, Theorem 5.8 follows from Lemma C.12 and Lemma C.13.