Automating Relatively Complete Verificationof Higher-Order Functional Programs
Hiroshi Unno

Tachio Terauchi

Naoki Kobayashi

University of Tsukuba
uhiro@cs.tsukuba.ac.jp

Nagoya University
terauchi@is.nagoya-u.ac.jp

University of Tokyokoba@is.s.u-tokyo.ac.jp

Abstract
We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional
programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on theclassical work on relatively complete “Hoare logic like” programlogic for higher-order procedural languages. Then, by adopting therecently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automatedrelatively complete verification of higher-order programs.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meaningof Programs]: Specifying and Verifying and Reasoning about Programs
Keywords Relative Completeness, Higher-Order Programs, Software Model Checking, Type Inference

1. Introduction
Recently, motivated by the success of software model checkers [12]for the automated verification of first-order programs, researchers
have proposed “model checkers” for the automated verification ofhigher-order programs [13, 18, 23, 26, 27]. Interestingly, they haveall been formulated as a form of refinement type inference.1
The refinement type systems employed in the automated higherorder program verification have some important differences fromthe ones from the original, non-automated approaches like DML[30], making them more amenable to automation (such as the lackof implicit Π types). But, they follow the non-automated onesin that the types embed first-order logic (FOL) formulas, calledrefinement predicates, over program values (as in dependent types)that are used to express and enforce detailed properties of the
program.
For example, consider the OCaml program shown in Figure 1. Here, * denotes a non-deterministic choice. Given an in-c ACM, 2013. This is the author’s version of the work. It is posted here by permissionof ACM for your personal use. Not for redistribution. The definitive version was
published in the Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages (POPL 2013)let rec app x f = if * then app (x+1) f
else f x inlet check x y = if x <= y then ()else assert false in
let main i = app i (check i)
Figure 1. A simple higher-order program.
teger argument i to main, the program recursively calls app nondeterministically to apply the closure check i to i + j where j is
the number of times the then branch is taken in app. The program issafe in that assert false is unreachable for any argument i. The
program is difficult to verify via first-order program verification
methods because of the higher-order recursive function app.
Recent advances in higher-order program verification have enabled automated verification of such programs via refinement type
inference. For the program above, the following refinement types
may be automatically inferred to verify its safety.2
app : x:int → f :({u:int | u ≥ x} → unit) → unit
check : x:int → y :{u:int | u ≥ x} → unit
main : i:int → unit
The type of app expresses the fact that the function takes aninteger argument x, and a function-type argument f which takes aninteger at least as large as x. The type of check says that it takes
integers x and y such that x ≤ y. And, the type of main says thatit takes any integer argument.
The refinement type systems underlying the verifiers are sound,that is, they only type safe programs. However, they are incompletein that there are safe programs that they cannot type. Indeed, theonly known positive result is for the class of the finite domainbase-type data programs, which can be verified completely by arefinement type system augmented with intersection types [16, 17].
The situation is in stark contrast to that of automated first-orderprogram verification [12] where the underlying program logic, suchas the Hoare logic, is relatively complete.
For example, none of the refinement type systems proposed forautomated higher-order program verification can type and verify
the program shown in Figure 2, even though the program is onlya small modification of the one from Figure 1: it simply switches
the order of app’s arguments. Nor, are they able to type and verify
the program shown in Figure 3, which uses the function succ to
successively build closures to pass integers larger than i to checki. The program is untypable even if we were allowed to change theorder of the function arguments.
We note that this is an incompleteness at the level of the program logic (i.e., refinement type system) and not the verification
algorithm (i.e., type inference algorithm). That is, there exist notypes within the refinement type system that can type the program,

1 In fact, the equivalence of model checking and refinement type inference

has been shown for the finite domain base-type data case [16, 17].

2 The type syntax is borrowed from Augustsson [1].

let rec app f x = if * then app f (x+1)
else f x inlet check x y = if x <= y then ()else assert false in
let main i = app (check i) i
Figure 2. A variant of Figure 1.
let rec app3 f g = if * then app3 (succ f) g
else g f inlet app x f = f x inlet succ f x = f (x + 1) in
let check x y = if x <= y then ()else assert false in
let main i = app3 (check i) (app i)be called with any integer i. (For a base type B, we often abbreviate
the refinement type {u:B | ⊤} as B. E.g., int = {u:int | ⊤}.)
Therefore, we try to type the body of main under the assumptionthat the type of i is {u:int | ⊤}. The most precise type for thepartial application check i is y : {u:int | u ≥ i} → unit (i.e.,functions that can take any integer at least as large as i), and themost precise type for i is {u:int | u = i} (i.e., integers equal
to i). (Intuitively, {u:B | θ} expresses values of the base type B
satisfying the refinement predicate θ, and x : τ → σ expresses
functions that return a value of the type σ[e/x] when given theargument e of the type τ .)We show that the type systems fail to give the higher-orderfunction app a sufficiently precise type to verify the program’ssafety. The type of app must be of the form

Figure 3. Another variant of Figure 1.

f :({u:int | θ} → unit) → x:{u:int | φ} → unit

let alone inferable ones. While higher-order program verification isin general undecidable, like the first-order program verification is,
it would be desirable to have a relatively complete reasoning framework that would serve as the basis of verification algorithms, as the
Hoare logic does for first-order programs.
To this end, this paper presents an automated approach to a
relatively complete verification of higher-order programs. First,
we present an extension to the refinement type system such thatthe resulting refinement type system is relatively complete. The
extension is inspired by the classical work on relatively complete
program logic for higher-order procedural languages by German
et al. [6, 7] (also, [8]) who showed that relative completeness isachievable while avoiding the explicit use of functions as data so as
to maintain a “Hoare logic like” control-data separation.
However, their proof of relative completeness does use encoding of functions as base-type data, and we rely on the same technique for our relative completeness proof. Moreover, to hide the useof functions as data from the program logic, they introduce quantifiers that the client verifier must appropriately instantiate. (To thebest of our knowledge, no actual verifier was built based on theirprogram logic.) Therefore, as our second contribution, we show atype inference method that extends the first-order logic constraint
solving of the previous automated refinement type inference systems to quantified reasoning by leveraging recent advances on arelated problem [4, 9, 24].
In summary, the paper’s contributions are as follows.

where the refinement predicates θ and φ are FOL formulas in
the theory of base-type data.3 In addition, as discussed below,
to prevent degenerate types, the refinement type systems enforce
an important well-formedness condition that restricts the variables
that can appear free in a refinement predicate. (Here, θ and φ are
restricted so that fv(θ) ⊆ {u} and fv(φ) ⊆ {f, u}, where fv(θ)
denotes the free variables of θ.)
From the application f x in the body of app, the type systemasserts that φ ⇒ θ, that is, f must be safe to be given the argument x. In the body of main, app is applied to check i and i,and the type system asserts that the type of check i is a subtype of {u:int | θ} → unit and the type of i is a subtypeof {u:int | φ}. This leads to the constraints u = i ⇒ φ andθ ⇒ u ≥ i, accurately expressing the fact that i is passed as thesecond argument to app and that the first argument to app (i.e.,
check i) expects a value at least as large as i.
A solution to the set of constraints is θ ≡ u ≥ i and φ ≡ u = i,but this is degenerate because main’s variable i would appear inapp’s type. (Recall that θ, φ are refinement predicates of app’s
type.) Intuitively, it means that the function app could “see” values
from a specific context of its use (i.e., main). Indeed, as remarked
above, the refinement type systems disallow such degenerate types
via the well-formedness condition, and only allow θ, φ such thatfv(θ) ⊆ {u} and fv(φ) ⊆ {f, u}. That is, the refinement predicates are allowed to only mention the variables in their respective
scopes. Consequently, the program is (conservatively) rejected as
untypable. It is worth noting that the program of Figure 1 does nothave this issue as app’s arguments are conveniently ordered so thatapp’s function-type argument could depend on the base-type argument to allow the following sufficiently precise type:• A refinement type system that is relatively complete for safety

verification of higher-order functional programs.
• A type inference algorithm for the refinement type system.

In the next section, we give an informal overview of the main ideas.
On incompleteness of the inference: The type inference algorithm that we propose is, of course, incomplete in that it is not able
to decide the typability of all programs. This is expected because
safety verification is undecidable in general. Instead, our contribution is a type system that is complete relative to a hypotheticaltheorem prover complete for first-order arithmetic, and a novel inference algorithm that is able to automatically verify a non-trivial
subset of the programs that were not possible to verify with theprevious automated approaches.

2. Informal Overview
We informally describe the incompleteness issue by showing how
the existing approaches [13, 18, 23, 26, 27] fail to type the programs
shown in Figures 2 and 3.
First, let us try to type Figure 2. Here, the goal is to show thatmain can be given the type i : int → unit, that is, main is safe tox:int → f :({u:int | u ≥ x} → unit) → unit
Unfortunately, as exemplified by Figure 3, the incompletenessissue is not just a matter of choosing the right order of function
arguments. Here, the program is untypable even if we were allowed
to change the order of the arguments, and the untypability comesfrom not being able to give a precise enough type to app3. Ideally,
we would like to express via app3’s type the fact that g is safe whenapplied to f (and also when applied to succj f for any j > 0). But,
this requires a type that is parametric in f and g’s behavior, andthat cannot be given because the only parameters of app3 are f andg, and they are both function-type arguments. Note that refinement
predicates of the form “g is safe to be called with f” are prohibitedas they are required to be FOL formulas over the base-type data.
3 We could also give non-⊤ refinement predicates to unit, but it does notaffect the example.

2.1

Our Approach

Our approach to solving the incompleteness issue is inspired by
the research on relatively complete program logic for higher-orderprocedural languages [6–8]. The main idea is to add extra dummybase-type parameters that are instantiated appropriately so thatthe refinement type of a higher-order function can depend on theparameters.
For example, for the program of Figure 2, we add an extra basetype parameter a to app and obtain the following program.
let rec app a f x = if * then app[a] f (x+1)
else f x inlet check x y = if x <= y then ()else assert false in
let main i = app[i] (check i) i
Here, for clarity, the parameter passings for the extra parameters
are written as quantifier instantiations, but they may be understoodas ordinary function applications (e.g., app[a] is app a). With theaddition of the extra parameter, it becomes possible for the existingrefinement type systems designed for automated verification totype and verify the program. For example, the following types are
sufficient for typing the program.
app : a:int → f :(τ → unit) → x:τ → unit
check : x:int → y :{u:int | u ≥ x} → unit
main : i:int → unit
where τ = {u:int | u ≥ a}. Note that the extra parameter a isused to parametrize f ’s behavior in the type of app.
There is a simple rule to adding extra parameters that can beshown to be sufficient for relative completeness: add one just before
each function-type argument. Following the rule, for example, theprogram of Figure 3 is translated as follows.
let rec app3 a f b g =if * then (app3[a] (succ[a] f))[a] gelse g[a] f inlet succ b f x = f (x + 1) in
let check x y = if x <= y then ()else assert false in
let app x a f = f x inlet main i = (app3[i] (check i))[i] (app i)And, it can be shown that the resulting program is typable, forexample, by the following types.
app3 : a:int → f :τ1 → b:int → g :τ2 → unit
app :
x:int → a:int → f :({u:int | u ≥ x} → unit) → unit
succ : b:int → f :(σ → unit) → x:σ → unit
check : x:int → y :{u:int | u ≥ x} → unit
main : i:int → unit
where σ = {u:int | u ≥ b}, τ1 = {u:int | u ≥ a} → unit,and τ2 = c:int → τ1 → unit.
However, the rule does not answer how the extra parameters
should be instantiated. (In the above, we seem to have magicallyconjured the appropriate instantiations i and a!) Indeed, an analogous rule was first discovered by German, Clarke, and Halpern[6, 7] in their work on a relatively complete program logic forhigher-order procedural languages, and their proof of relative completeness relies on the fact that, with an expressive theory of thebase-type data domain (such as Peano arithmetic), one can encode
each function closure as a base-type data expression so that the extra parameters can be instantiated by the base-type data representation of the corresponding function-type argument. However, explicitly instantiating the extra parameters by such encoded expressions
and forcing the client verifier to reason about them is impractical.

d
e

::=
::=
|

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

Figure 4. The syntax of the simple functional language.
Therefore, they proposed to leave the instantiations unspecified in
the program logic so that the task of finding sufficient instantiations
is left to (the FOL theorem prover of) the client verifier.
Following the idea, for example, the program of Figure 2 istranslated as follows by introducing fresh variables v1 and v2.
let rec app a f x = if * then app[v1] f (x+1)
else f x inlet check x y = if x <= y then ()else assert false in
let main i = app[v2] (check i) i
Then, the refinement type inference problem is reduced to the problem of finding appropriate instantiations for v1 and v2 along withthe types for the program. For this, we extend the FOL constraint
solving used in the previous work on refinement type inferencewith quantified reasoning over template expressions [4, 9, 24]. Concretely, in Section 4, we show how the counterexample-guided refinement type inference [18, 26] can be extended in this way toinfer appropriate instantiations as well as types.
2.2 Paper Organization
The rest of the paper is organized as follows. Section 3 presents
the refinement type system along with the target functional language, and proves its relative completeness under the extra parameter addition strategy. Section 4 presents the type inference algorithm. Section 5 presents the preliminary experience with the type
inference algorithm, implemented as an extension to the higherorder software model checker (i.e., refinement type inference system) MoCHi [18]. Section 6 discusses related work, and Section 7
concludes. The extended report [28] contains the omitted materials.

3. Language and Type System
We formalize the target programming language. Figure 4 shows thesyntax. The language is essentially the simply-typed lambda calculus with recursion and primitives for integer arithmetic operations.
For simplicity the only base-type data in this language is integers,
but other base types and their operations can be encoded in thestandard way: for example, true = 1 and false = 0.
→
A program, d, is a finite set of function definitions, F −x = e,−→
defining a function named F with the formal parameters x and the→
body e. The notation −a denotes a possibly empty sequence. The
functions are mutually recursive in that the body of a function may
refer to other functions, including itself. Each function is closed
except for the free function names (i.e., functions are lambda lifted[15]). We also assume that d contains a function named main that
only takes base-type (i.e., integer) arguments.
Expressions, e, comprise non-deterministic branches, let expressions, constants c, function names F , variables x, and (constantor user-defined function) applications e x. Constants include integer constants such as −1, 0, 1, 2, and integer operations such as +and ≤ (recall that we model booleans via integers). We assume that
there are unary constant operators named assert and assume.
We restrict expressions to be in continuation passing style (CPS)
so that they are non-returning, except when they occur let-bound(i.e., occurs as e1 in let x = e1 in e2 ). By contrast, let-bound expressions are restricted to be non-CPS (i.e., value returning) expressions, which are total applications of constant operators including
the assume and assertion expressions assume x and assert x, andlet x = e1 in e2 →d e2 [e3 /x] where e1 ⇓ e3
let x = assert 1 in e →d e[1/x]
let x = assert i in e →d fail where i 6= 1
let x = assume 1 in e →d e[1/x]
let x = assume i in e →d safe where i 6= 1
if ∗ then e1 else e2 →d e1
if ∗ then e1 else e2 →d e2
→
→
→
→
F−
e → d e ′ [−e /−x]where F −x = e′ ∈ dFigure 5. The reduction rules.
partial applications (of user-defined functions). We restrict constantoperator applications to be total. CPS/A-normal-form-style is used
for simplicity. Direct-style syntax can be supported by CPS conversion.
The rest of the syntax is straightforward. As usual, applications
associate to the left so that e0 e1 e2 = (e0 e1 ) e2 . We write→→
e for the series of applications e0 e1 e2 . . . en where −e =e0 −e1 , e2 , . . . , en . We write e1 ; e2 for let x = e1 in e2 such thatx ∈/ fv(e2 ), where fv(e) denotes the free variables of e. Without
loss of generality, we assume that bound variables are distinct.
Note that, while the language only has non-deterministic branches,a conditional branch if x then e1 else e2 can be encoded asif ∗ then assume x; e1 else let y = ¬x in assume y; e2which is equivalent for assertion safety.
We define the operational semantics of the language as a smallstep reduction relation from states to states. A state is a run-time
expression e that extends the source expressions with non-variable
arguments at function applications, a special failure state fail, anda special safe state safe. (We overload the symbol e to range overrun-time expressions when it is clear from the context.)
The reduction relation →d is defined by the rules shown in
Figure 5. Here, e ⇓ e′ denotes the evaluation of the value returning→→
expression e to the value e′ , and is defined as F −e ⇓ F −
e and
→
→
c−
e ⇓ [[c]](−e ) where [[c]] is the relation denoting the semantics ofa non-assume/assert constant c, so that, for example [[+]](i, j) =i + j for integers i and j. (An integer constant is represented by→a 0-ary constant.) We let partial applications (i.e., F −e ) represent
function closures. Formally, a value is either an integer constant ora function closure.
The semantics of a program d is defined as a series of reductions−→ →→starting from an initial state emain [ i /−x ] where main −x =emain ∈ d
−
→
−
→
→
and i are integer arguments for main (i.e., | i | = |−x |). Note
that, because of CPS, reductions only occur at the top level. We
write e →∗d e′ for zero or more reductions from e to e′ . We saythat a program is (assertion) safe if its evaluation does not cause an−→ →assertion failure, that is, if emain [ i /−x ] 6→∗d fail for any arguments−→
i of main.
We assume that a program is typed under the standard simple
type system whose type grammar is shown below.
s ::= ⋆ | int | s → s′
Here, the type ⋆ represents the type of a CPS expression. For each
expression e in the program, we write sty(e) to denote its simple
type.
The typability in the simple type system assures that the program does not “get stuck”, for example, by trying to use an integer as a function, but it does not guarantee its safety. Therefore, aprogram either runs forever safely (due to CPS, a program cannot
return), stops safely in the state safe by reaching a false assume, oraborts with an assertion failure. The typing rules for the simple typesystem are standard and are deferred to the extended report [28].

τ, σ

::=

⋆ | {u | θ} | x:σ → τ

Figure 6. The syntax of refinement types.
sty(x) = int
VbΓ ⊢ x : {u | u = x}Γ ⊢ c : ty(c)Cststy(κ) ∈→VfΓ ⊢ κ : Γ(κ)Γ ⊢ e1 : σ Γ, x:σ ⊢ e2 : ⋆LetΓ ⊢ let x = e1 in e2 : ⋆Γ ⊢ e : y :σ → τ Γ ⊢ x : σAppΓ ⊢ e x : τ [x/y]Γ ⊢ e1 : ⋆ Γ ⊢ e2 : ⋆IfΓ ⊢ if ∗ then e1 else e2 : ⋆Γ⊢e:σ

Γ ⊢ σ ≤ τ fv(τ ) ⊆ dom(Γ)
Sub
Γ⊢e:τ
Figure 7. The typing rules.

3.1 Refinement Type System
We present a refinement type system for the language. First, we
present a sound but incomplete refinement type system without theextra parameter addition, and then introduce the extra parameter addition as an extension in Section 3.2. The (incomplete) refinement
type system is not significantly different from the ones proposed
previously for automated verification [13, 18, 23, 26, 27] (e.g., it
can be obtained by removing intersection types from [18, 26]4 ).
Figure 6 shows the syntax of refinement types. Here, {u | θ}is a refinement base (i.e., integer) type that refines an integer by
the refinement predicate θ which is a FOL arithmetic formula overthe base (i.e., integer) type variables.5 We sometimes abbreviate{u | θ} as int when θ is a tautology (e.g., {u | ⊤} = int).
Intuitively, {u | θ} denotes the type of integers u satisfying theformula θ.
The type x : σ → τ is a dependent function type, consisting of
the argument type σ and the return type τ . Intuitively, x : σ → τdenotes the type of a function (or a constant operation) that returns
a value of the type τ [y/x] when applied to an argument y of thetype σ. As usual, → associates to the right.
The type {x | θ} binds x in θ. Likewise, x:σ → τ binds x in τ
(but not in σ). That is,fv({x | θ}) = fv(θ) \ {x}fv(x:σ → τ ) = fv(σ) ∪ (fv(τ ) \ {x})We sometimes abbreviate x : σ → τ as σ → τ when x does notoccur free in τ . (It actually suffices to limit x to occur free in τ
only if x is a base type argument because refinement predicates are
restricted to be over the base-type variables.) Types are equivalent
up to renaming of bound variables.
The simple-type shape of σ, tshape(σ), is defined as follows:
tshape({u | θ}) = int
tshape(⋆) = ⋆tshape(x:σ → τ ) = tshape(σ) → tshape(τ )4 While intersection types are not needed for relative completeness, they

compromise neither soundness nor completeness, and sometimes aid theverification in practice. The implementation shown in Section 5 supports
intersection types.
5 The full theory of Peano arithmetic is needed for relative completeness,but any subset (e.g., the quantifier-free theory of linear arithmetic) is sufficient for soundness.

Γ ⊢ σ2 ≤ σ1 Γ, x : σ2 ⊢ τ1 ≤ τ2Sf
Γ ⊢ x:σ1 → τ1 ≤ x:σ2 → τ2

Γ⊢⋆≤⋆

Sc

u∈
/ fv([[Γ]]) ([[Γ]] ∧ θ1 ) ⇒ θ2Sb
Γ ⊢ {u | θ1 } ≤ {u | θ2 }Figure 8. The subtyping rules.
Figure 7 shows the typing rules. The judgements for the expressions are of the form Γ ⊢ e : τ where Γ is a type environment
mapping variables and function names to types.
We discuss each typing rule. Vb 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. Vf types function-type variables and function names by looking up the environment. Here, →denotes the set of simple function types. (We use the meta variableκ to range over both variables and function names.) Cst types constants. Here, ty(c) denotes the pre-assigned type of the constant csuch thatty(assume) = x:int → {u | x = 1 ∧ u = 1}ty(assert) = x:{u | u = 1} → {u | u = 1}
and ty(c) is the precise type for a non-assume/assert constant c(e.g., ty(+) = x : int → y :int → {u | u = x + y}).6 Let isself-explanatory. App types applications. Here, τ [x/y] is the usual
capture-avoiding substitution. If types branch expressions.
Sub is the subsumption rule. The subtyping relation is definedin Figure 8. In Sb, [[Γ]] is the FOL formula denoting the assumptions about the base-type variables in Γ, and is defined as follows.
^θ[x/u][[Γ]] =
x:{u|θ}∈Γ

Like the rule of consequence of the Hoare logic [10], Sb asks theclient verifier (i.e., the type inference system) to decide the validityof arbitrary FOL arithmetic formulas. As expected, our completeness result is relative to the hypothetical completeness of deciding
this. In verification practice, one may settle for incomplete theorem proving or a decidable theory subset to make type checking
decidable.7
Sub enforces well-formedness of the introduced type by asserting that its free variables appear bound in the environment. As
shown below, the top-level types (i.e., the types of the recursivefunctions) are required not to contain free variables.
D EFINITION 3.1 (Well-formed type). We say that a type is closed
if it has no free variables. Let ∆ be a top-level type environment
mapping function names to types. We say that σ is a well-formed
type for F if σ is closed and tshape(σ) = sty(F ). We say that ∆ isa well-formed top-level type environment if ∆(F ) is well-formed
for each F .
−→ → τ to abbreviate the function type x :σ →Let us write −x:σ11−→ = x : σ , . . . , x : σ . We define· · · → x :σ → τ where −
x:σ
n

n

1

1

n

n

the notion of a well-typed program.
D EFINITION 3.2 (Well-typed program). We write ∆ ⊢ d if thefollowing conditions hold.
(1) ∆ is a well-formed top-level type environment.
6 See the extended report [28] for the definition of a precise constant type.

Also, non-precise but sound constant types, that over-approximate the actual semantics, are sufficient for soundness.
7 Also, type checking being decidable is different from type inference (i.e.,
typability) being decidable. The previous research has proposed various
incomplete inference approaches [13, 18, 23, 26, 27].

→−−→ ⊢ e : ⋆ where(2) For each function F −x = e ∈ d, we have ∆, x:σ−→ → ⋆.
∆(F ) = −x:σ−−−→(3) ∆(main) is of the form x:int → ⋆. (I.e., the refinement
predicates for the arguments of main are all ⊤.)A program d is said to be well-typed (equivalently, typable) if there
exists ∆ such that ∆ ⊢ d.
The condition (2) says that ∆ contains fixed-point types for therecursive functions comprising d, and (3) says that main is safe to
be called with any arguments (recall that main is a function overinteger arguments).
The type system is sound in that it ensures that a well-typed
program does not cause an assertion failure.
T HEOREM 3.3 (Soundness). If ∆ ⊢ d then d is safe.
The theorem follows from the soundness of the refinement typesystem extended with extra parameter additions (Theorem 3.6).
E XAMPLE 3.4. Let the program d1 consist of the following functions.
app x f = if ∗ then app (x + 1) f else f x
check x y = if ∗ then assume (x ≤ y); check x yelse assume ¬(x ≤ y); assert 0; check x ymain i = app i (check i)
The program is the one from Figure 1 translated into the target
language. (We elide A-normalization for readability.) Let ∆ be thefollowing type environment.
∆(app) = x:int → f :({u | u ≥ x} → ⋆) → ⋆∆(check) = x:int → y :{u | u ≥ x} → ⋆∆(main) = i:int → ⋆It is routine to check that ∆ ⊢ d1 . Therefore, d1 is typable and is
safe.
Next, consider d2 shown below.
app f x = if ∗ then app f (x + 1) else f x
check x y = if ∗ then assume (x ≤ y); check x yelse assume ¬(x ≤ y); assert 0; check x ymain i = app (check i) i
The program is a translation of the program from Figure 2. The
program is safe but untypable (as remarked in Section 2, also under
the previous refinement type systems [13, 18, 23, 26, 27]). Notethat we cannot simply assign app the type ∆(app) from the above
but with the order of x and f reversed so thatf :({u | u ≥ x} → ⋆) → x:int → ⋆The type is not closed and therefore is not a well-formed top-level
type (cf. Definition 3.1). The well-formedness condition forces therefinement predicates to only refer to the values passed earlier.
Well-formedness is not a superficial restriction: In the presence of
higher-order functions and function closures (i.e., partial applications), we cannot generally determine “up front” in the programlogic what will be passed later to a closure.
The issue is apparent in the following program d3 , which is atranslation of Figure 3.
app3 f g = if ∗ then app3 (succf ) g else g f
app x f = f x
succ f x = f (x + 1)
check x y = if ∗ then assume (x ≤ y); check x yelse assume ¬(x ≤ y); assert 0; check x ymain i = app3 (check i) (app i)
As remarked in Section 2, the program is safe but untypable, evenif we were allowed to change the order of the function arguments.
Here, it is not possible to determine what will be passed to the−−→ → τ abbreviation introduced(Note that this subsumes the x:σ→→
earlier.) Let h−γ i be the sequence −γ with each universal quantifierbinding ∀x : σ replaced with the variable binding x : σ. That is,→→→hεi = ε, and hx:σ, −γ i = h∀x:σ, −γ i = x:σ, h−γ i.
We extend the notion of well-typed program to accommodate
universal quantifier bindings.

Γ ⊢∀ e : ∀x:σ.τ Γ ⊢∀ o : σ o ∈ pureExps
InstΓ ⊢∀ e : τ [o/x]Γ ⊢∀ σ2 ≤ σ1 Γ, x:σ2 ⊢∀ τ1 ≤ τ2S∀
Γ ⊢∀ ∀x:σ1 .τ1 ≤ ∀x:σ2 .τ2
Figure 9. Additional typing rules.

D EFINITION 3.5 (Well-typed program – Extended). We write ∆ ⊢∀d if the following conditions hold.

closures succj f without some non-trivial program reasoning (i.e.,
i captured in g added the number of times app3’s then branch istaken before the else branch is reached). In effect, the idea of theextra parameter addition for relative completeness is to delegate
such tasks to the client verifier.

(1) ∆ is a well-formed top-level type environment.
→→(2) For each function F −x = e ∈ d, we have ∆, h−γ i ⊢∀ e : ⋆−→where ∆(F ) = γ → ⋆.
−−−→(3) ∆(main) is of the form x:int → ⋆.

3.2

Extra Parameters for Relative CompletenessAs shown in Example 3.4 (also Section 2), the refinement type system is incomplete by itself. While a complete checking of safety isclearly undecidable as the language allows arbitrary integer operations, we would like to make the refinement type system be complete relative to an oracle that could decide the FOL implications
discharged at the subtyping rule Sb.
Rather than formulating the extra parameter addition as a program translation as done in Section 2, here, we present it as a typesystem extension in the form of universally quantified types. Thisis expositionally convenient, because extra parameters can be represented as universally bound variables so that they can be easily
distinguished from ordinary parameters.
We extend the grammar of refinement types with universallyquantified types as follows.
τ, σ ::= ... | ∀x:σ.τ
In ∀x:σ.τ , x is a binding occurrence and may occur free in τ (i.e.,fv(∀x:σ.τ ) = fv(σ) ∪ (fv(τ ) \ {x})). Intuitively, it expresses thefunction type x:σ → τ such that x is an extra parameter. We define
tshape(∀x:σ.τ ) = tshape(τ ).
We extend the type system with the quantifier instantiation andthe subtyping rules shown in Figure 9. Here, pureExps is the set ofside-effect-free integer-type expressions defined by the grammar→o ::= x | c −o→where x is an integer-type variable and c −o is a total application of
8
a non-assume/assert constant. Therefore, Inst allows instantiation
with any in-scope side-effect-free integer-type expression having
the requested type. S∀ is analogous to the subtyping rule for function types (i.e., Sf). To distinguish, we write ⊢∀ for the type judgements of the extended type system. All the rules from Figure 7 andFigure 8 are assumed to be included in ⊢∀ (with ⊢ replaced by ⊢∀ ).
The well-formedness definition is also retained from the preextension (cf. Definition 3.1). Therefore, for example, both
x:int → ({u | u = 0} → ⋆) → ⋆x:int → ∀y :int.({u | u = y} → ⋆) → ⋆are well-formed refinement types for F such that sty(F ) = int →(int → ⋆) → ⋆.
Let γ be a disjoint union of variable bindings x : σ or universal→
quantifier bindings ∀x:σ. The type abbreviation −γ → τ is defined
as follows.

→

if −
γ =ε
τ
−
→
−
→
→
→
γ → τ = ∀x:σ.τ1
if γ = ∀x:σ, −γ1 and −γ 1 → τ = τ1

→
−
→
−
→
x:σ → τ if −γ = x:σ, γ and γ → τ = τ
1

8 We

1

1

1

extend the typing rules to (non-A-normal-form) side-effect-free
integer-type expressions in the obvious way. See the extended report [28].

A program d is said to be well-typed if ∃∆.∆ ⊢∀ d.
→Note that the only differences from Definition 3.2 are −γ → ⋆ and−→h γ i in (2) which allow universal quantifiers in the type of the functions. Also, note that the well-formedness condition now allows therefinement predicates to refer to the universally quantified variablesin their scope.
We state the soundness of the extended refinement type system.
T HEOREM 3.6 (Soundness – Extended). If ∆ ⊢∀ d then d is safe.
The proof is standard [23, 27, 29] and is deferred to the extended
report [28].
As remarked in Section 2, for relative completeness, it suffices
to limit the position of extra parameters (i.e., universal quantifiers)
to one before each function-type parameter. To this end, we define
ushape(σ) to be a simple type such that, for a function of thesimple type ushape(σ), σ has just the sufficient extra parameters.
Formally, ushape(σ) is defined by the rules below.
ushape({u | θ}) = int

ushape(⋆) = ⋆tshape(σ) = int
ushape(x:σ → τ ) = ushape(σ) → ushape(τ )tshape(σ ′ ) = int tshape(σ) ∈→ushape(∀y :σ ′ .x:σ → τ ) = ushape(σ) → ushape(τ )Note that ushape(σ) is defined only for σ that has one extra
parameter just before a function-type parameter. Also, for σ suchthat ushape(σ) is defined, we have ushape(σ) = tshape(σ). We are
now ready to state the relative completeness theorem, which saysthat if a program is safe then it can be typed with extra parameter
additions (even when their positions are restricted to the pattern
above).
T HEOREM 3.7 (Relative Completeness). If d is safe, then there
exists ∆ such that ∆ ⊢∀ d and ushape(∆(F )) = sty(F ) for each→F−x = e ∈ d.
We defer the proof to the extended report [28]. The proof adopts
the ideas from the work on relatively complete program logics forhigher-order procedural languages [6–8] that instantiate the extra
parameters by the base-type encoding of the function closures. It is
worth noting that, as a corollary of Theorem 3.7, it follows thatthe refinement type system is relatively complete for first-orderprograms (i.e., programs without function-type parameters) even
without the extra parameter extension.
E XAMPLE 3.8. We show how ⊢∀ types d2 and d3 from Example 3.4. First, we have ∆2 ⊢∀ d2 where∆2 (app) =∀a:int.f :({u | u ≥ a} → ⋆) → x:{u | u ≥ a} → ⋆∆2 (check) = x:int → y :{u | u ≥ x} → ⋆∆2 (main) = i:int → ⋆Note that the types correspond to the ones used to type Figure 2
in Section 2.1. Also, note that ushape(∆2 (app)) = sty(app),ushape(∆2 (check)) = sty(check), and ushape(∆2 (main)) =sty(main). It is easy to see that check can be given the type
∆2 (check). We show that app can be given the type ∆2 (app). We
type the body of app under the type environment ∆2 , a : int, f :{u | u ≥ a} → ⋆, x : {u | u ≥ a}. Therefore, the applicationf x type-checks to give the type ⋆. To type the other branch,
app f (x + 1), we instantiate ∆2 (app) with a at app to give thetype
f :({u | u ≥ a} → ⋆) → x:{u | u ≥ a} → ⋆The type is then used to give the application app f the type x :{u | u ≥ a} → ⋆, which in turn gives the branch the type ⋆.
Finally, main can be given the type ∆2 (main) by instantiating∆2 (app) with i.
Likewise, let ∆3 be the following type environment.
∆3 (app3) = ∀a:int.f :τ1 → ∀b:int.g :τ2 → ⋆∆3 (app) = x:int → ∀a:int.f :({u | u ≥ x} → ⋆) → ⋆∆3 (succ) = ∀b:int.f :(σ → ⋆) → x:σ → ⋆∆3 (check) = x:int → y :{u | u ≥ x} → ⋆∆3 (main) = i:int → ⋆such that τ1 = {u | u ≥ a} → ⋆, τ2 = ∀c : int.τ1 → ⋆, andσ = {u | u ≥ b}. Note that ushape(F ) = sty(∆3 (F )) for each F= app3, app, succ, check, and main. We show that ∆3 ⊢∀ d3 byfollowing the same instantiation scheme used to type Figure 3 inSection 2.1. We type the then branch of app3 by instantiating app3
and succ with a, and instantiating the resulting app3 (succ f )with a (or with an arbitrary side-effect-free integer-type expression,
because b does not appear free in its scope in ∆3 (app3)). The elsebranch can be typed by instantiating g with an arbitrary side-effectfree integer-type expression (because c does not appear free in its
scope in ∆3 (app3)). Then, to type main, we instantiate app3 withi, and instantiate app3 (check i) with an arbitrary side-effect-free
integer-type expression.
The examples show that instantiating via simple expressions areoften sufficient for verifying safety, and not all quantifiers may evenbe needed. (Contrast this with the instantiation via Gödel numbering used in the proof of Theorem 3.7.9 ) We take advantage of theobservation in the type inference method described in Section 4.

4. Type Inference
The type inference framework is based on, and extends the recent
work on the counterexample-guided approach to refinement type
inference [18, 26] (but, the idea may be adopted to extend the backend of other refinement type inference systems like [13, 27]). To allow smooth adoption and use the existing type inference algorithms
mostly as a blackbox, we implement the extra parameter addition
as a program translation as in Section 2, instead of modifying theunderlying type system to model it by universally quantified types
as in Section 3.2.
Figure 10 shows the overview of the type inference process. In
Step 1, we translate the given program by adding extra parameters
as done in Section 2. Here, we maintain and use a parameter
substitution for instantiating the extra parameters. We initialize theinstantiation expressions to arbitrary constants (e.g., 0), and thenperform a counterexample-guided refinement type inference over
the translated program.
Following the counterexample-guided abstraction refinement(CEGAR) scheme popularized in model checking [3, 12], in the
counterexample-guided refinement type inference, we maintain a
9 This can be seen as a difference between just checking safety and express-

ing the precise semantics as weakest preconditions.

Input Program

Safe
TypableStep 1: Parameter
Addition(Section 4.1)
New Parameter
Substitutions

Translated Program

Step 2: Fixed-point
Type Inference[18, 26]

Counterexample

New Candidate Types

Step 4: Refinement(Section 4.2),[18, 26]

Infeasible

Step 3:
Feasibility Check[18]
Feasible

UnsafeFigure 10. The type inference overview.
set of candidate refinement types (or the refinement predicatesthat comprise them). Then, we try to find a type assignment forthe program within the candidates via the standard fixed-pointtype inference process (Step 2 in Figure 10). The fixed-point type
inference uses an automated FOL theorem prover, such as a SMT
solver, to decide the FOL implications discharged at the subtyping
rule Sb. We refer interested readers to the previous work [18, 26]
for details.
A counterexample is generated when the candidates are foundinsufficient, and we analyze the reason for the failure to either validate the counterexample (Step 3), or update the candidate types
or the parameter substitution to eliminate the spurious counterexample (Step 4). In the refinement step, the previous work [18, 26]
only generated new candidate types (i.e., the arrow from Step 4 toStep 2). But, because of the incompleteness of the underlying typesystem, some spurious counterexamples are impossible to refuteby just adding new candidate types. The key component of our new
type inference method is generating new parameter substitutions insuch a situation (i.e., the arrow from Step 4 to Step 1).
Then, the CEGAR process is repeated with the updated candidate types or the updated parameter substitutions. The former caseis identical to the previous work, and in the latter case, we repeat
from Step 1 to re-translate the program with the updated parameter
instantiations.
4.1 Adding Extra Parameters
We add an extra parameter just before each function-type parameter. Also, we assign a unique label to each sub-expression of the
program where a parameter instantiation occurs. (Note that suchplaces are syntactically determined.) Let L be the set of the labels
and bvs(ℓ) denote the base-type variables that can occur free in thescope of the sub-expression with the label ℓ ∈ L.
The type inference process maintains the parameter substitution
P that maps each ℓ to a side-effect-free integer-type expression
o such that fv(o) ⊆ bvs(ℓ). We use P (ℓ) as the instantiation
expression at ℓ. We restrict the range of P , and therefore, theinstantiation expressions, to linear arithmetic expressions. That is,
P (ℓ) is restricted to be of the form
c 0 + c 1 x1 + · · · + c n xn
where bvs(ℓ) = {x1 , . . . , xn } and c0 , . . . , cn are integer constants.
This is an important design choice motivated both by the desire tominimize the complexity of the type inference, and also by the ob-servation that sufficient instantiations tend to be simple expressionsin practice (cf. Example 3.8).
The parameter substitution P may be initialized arbitrarily, forexample, P (ℓ) = 0 for all ℓ. We translate the input programby adding the extra parameters to the function definitions andreplacing each instantiation site e with the application eP (ℓ) whereℓ is the label of e.
E XAMPLE 4.1. Recall the program d2 in Example 3.4. We add
an extra parameter a just before the function-type parameter fof app. Let ℓ1 and ℓ2 be the labels of the occurrences of app in
the body of app and main respectively. We have L = {ℓ1 , ℓ2 },bvs(ℓ1 ) = {a, x}, and bvs(ℓ2 ) = {i}. Suppose that the parameter
substitution is P = {ℓ1 7→ a, ℓ2 7→ i}. Then, d2 is translated to theprogram dP shown below.
app a f x = if ∗ then app a f (x + 1) else f x
check x y = if ∗ then assume (x ≤ y); check x yelse assume ¬(x ≤ y); assert 0; check x ymain i = app i (check i) i
4.2Counterexample-Guided Refinement

In MoCHi [18], a counterexample is a straightline higher-orderprogram (SHP) that is untypable with the current candidate types.
SHP is defined to be a recursion-free slice of the target program obtained by copying functions and removing branches so that it contains no branches and every function occurrence is “linear” (i.e.,each function is called only once).10 Intuitively, a counterexample
corresponds to the (abstract) program path taken to reach the assertion failure.
We check if the counterexample SHP is feasible. This part is
identical to the previous work [18] and is done by symbolicallyevaluating the SHP. If it is feasible, then the program is determinedunsafe and we are done. Otherwise, we attempt to infer refinement
types for the SHP. If the SHP is found typable, then the inferredrefinement types (or the refinement predicates embedded therein)
are added to the candidates and the CEGAR iteration returns to the
fixed-point type inference phase (i.e., Step 2 of Figure 10).
We infer types for counterexamples by using the techniquesfrom the previous work [18, 26, 27] that reduce the inference
problem to solving constraints over FOL formulas and predicate
variables such that the predicate variables serve as placeholders of
the refinement predicates to be inferred. We refer to the previous
work for details.
E XAMPLE 4.2. Given dP from Example 4.1, MoCHi may generate the SHP dS shown below.
app1 a f x = app2 a f (x + 1)
app2 a f x = f x
check x y = assume ¬(x ≤ y); assert 0
main i = app1 i (check i) i
Note that dS is recursion-free and linear. The SHP is typable and
MoCHi may infer refinement types ∆ such that∆(app1) = ∆(app2) =a:int → f :({u | u ≥ a} → ⋆) → x:{u | u ≥ a} → ⋆∆(check) = x:int → y :{u | u ≥ x} → ⋆∆(main) = i:int → ⋆Note that ∆ ⊢ dS .
As remarked above, because of the incompleteness of the underlying type system (i.e., ⊢), sometimes, a counterexample that is
detected to be infeasible is also found untypable. (The feasibility
10 [26]

defines a counterexample to be simply a currently-untypable
recursion-free program slice (i.e., possibly containing branches and nonlinearity), but uses linear intersection types to obtain a similar effect.

check is actually relatively complete.) In such a situation, we infer a new parameter substitution PR for the SHP so that the SHP
with each of its instantiation site ℓ instantiated with PR (ℓ) is typable. Then, we update the parameter substitution with PR , that is,
we set P := PR ∪ P |L\LSHP where LSHP is the labels of the SHP.
And, the CEGAR process returns to the parameter addition phaseto re-translate the program (i.e., Step 1 of Figure 10).
The parameter substitution inference proceeds as follows. First,
we assign labels to the SHP such that every copy of a subexpression gets the same label as the one in the original. (Note that
because of function copying, the same expression in the original
program can have multiple copies in the SHP.) Next, we introduce
a parameter substitution template, PT , that maps each ℓ ∈ LSHP toa linear arithmetic expression template p0 + p1 x1 + · · · + pn xn ,where bvs(ℓ) = {x1 , . . . , xn } and p0 , . . . , pn are fresh integer
variables. This, in turn, induces a SHP template that has PT (ℓ) as
the instantiation expression at each ℓ ∈ LSHP .
Now, the problem of inferring PR is reduced to that of inferring an appropriate integer substitution for the integer variables−→
p in the template. We reduce the problem to constraint solving→→
by generating a FOL constraint over −p of the form ∀−x .θ (for−→→some non-linear FOL formula θ over the variables p and −x ). Thatis, the SHP is typable with the instantiation expression PT (ℓ)ρ→
at each ℓ iff (∀−x .θ)ρ holds where ρ is a substitution that maps−→
p to integer constants. Although the problem of solving quantified integer non-linear FOL constraints is undecidable in general, the recently proposed constraint solving techniques based on
Farkas’ lemma [4, 9, 24] have shown effective for our applicationin many cases. We describe the constraint generation process in
Section 4.2.1 and the constraint solving process in Section 4.2.2.
4.2.1

Constraint Generation

The constraint generation algorithm is essentially the same as theones from the previous work [18, 26, 27] used for candidate type
inference. We give a brief review of the algorithm. For each function in the program, we prepare type templates containing predicate
variables that serve as placeholders of the refinement predicates tobe inferred. Then, we generate constraints over the predicate variables in the standard way. That is, we apply the typing rules to the
SHP but restricting the application of the subsumption rule Sub tojust the argument position of function applications (cf. Section 3.1).
This generates constraints over the type templates, which, in turn,
reduce to Horn-clause-like constraints over the predicate variables.
(See the extended report [28] for the formal definition of the constraint generation rules.) Because SHP is recursion-free and linear,
the generated Horn clauses are non-recursive, and we can obtain an
equivalent FOL formula.
E XAMPLE 4.3. Consider the SHP d′S shown below, which isequivalent to dS from Example 4.2 except that the extra parameter of app1 is instantiated by 0 instead of i.
app1 a f x = app2 a f (x + 1)
app2 a f x = f x
check x y = assume ¬(x ≤ y); assert 0
main i = app1 0 (check i) i
It is easy to see that the counterexample d′S is infeasible (i.e., issafe), and MoCHi is also able to detect the infeasibility. However,d′S is untypable with the underlying type system ⊢ because of theinappropriate instantiation expression.
To infer a new instantiation expression, we prepare the parameter substitution template PT for the instantiation sites of d′S , andfrom it, obtain the SHP template dT shown below.
app1 a f x = app2 (p0 + p1 a + p2 x) f (x + 1)
app2 a f x = f x
check x y = assume ¬(x ≤ y); assert 0
main i = app1 (p3 + p4 i) (check i) i
where p0 , . . . , p4 are free integer variables. Next, we generate theconstraints by preparing the type template ∆ such that∆(app1) =a:{u | P1 (u)} → ({u | P2 (a, u)} → ⋆) → {u | P3 (a, u)} → ⋆∆(app2) =a:{u | P4 (u)} → ({u | P5 (a, u)} → ⋆) → {u | P6 (a, u)} → ⋆∆(check) = x:{u | P7 (u)} → y :{u | P8 (x, u)} → ⋆∆(main) = i:int → ⋆This generates the following non-recursive set of Horn-clause-likeconstraints on the predicate variables P1 , . . . , P8 .
∀a, x.P1 (a) ∧ P3 (a, x) ⇒ P4 (p0 + p1 a + p2 x)∀a, x, u.P1 (a) ∧ P3 (a, x) ∧ P5 (p0 + p1 a + p2 x, u) ⇒ P2 (a, u)∀a, x.P1 (a) ∧ P3 (a, x) ⇒ P6 (p0 + p1 a + p2 x, x + 1)
∀a, x, u.P4 (a) ∧ P6 (a, x) ⇒ P5 (a, x)∀x, y.P7 (x) ∧ P8 (x, y) ⇒ x ≤ y∀i.⊤ ⇒ P1 (p3 + p4 i)∀i.⊤ ⇒ P7 (i)∀i, u.P2 (p3 + p4 i, u) ⇒ P8 (i, u)∀i.⊤ ⇒ P3 (p3 + p4 i, i)
Systematically simplifying the constraints by computing the least
solutions for the predicate variables in a bottom-up manner, we
obtain an equisatisfiable FOL formula on the variables p0 , . . . , p4
shown below.
∀x, y, z.
p4 x = p4 z ∧ p1 p4 x + p2 z = (p1 p4 + p2 )(y − 1) ⇒ x ≤ y
4.2.2

Constraint Solving

The constraint generation process above returns a constraint of the→form ∀−x .θ, where θ is a quantifier-free non-linear FOL formula→→over the variables −p and −x . (More precisely, θ is linear over−→−→x with coefficients over p .)11 The goal of the constraint solving→→
phase is to find an assignment ρ for −p satisfying ∀−x .θ.
We solve the constraints by adopting Gulwani et al.’s approach [9]. We give a brief overview of the idea. First, we use
Farkas’ lemma to remove the universal quantifications in the con→→straint ∀−x .θ, and obtain a constraint of the form ∃−r .φ, where φ→is a quantifier-free non-linear FOL formula on the variables −
p and
−
→
r . Then, we translate the constraint to a SAT formula by modeling integer variables as bit-vectors and integer operations suchas addition, multiplication, and comparison as boolean operations.
Finally, we use a state-of-the-art SAT solver to find a substitution ρ
→
→
for −
p and −
r that satisfies φ.
We describe the approach in a more detail. Given a univer→sally quantified constraint V∀−
x .θ, we convert θ to an equivalentV formula of the form i θi , where each θi is of the form¬( j=1,...,mi ei,j ≥ 0) such that each ei,j ≥ 0 is a linear in→→equality on −x with polynomials on −p as coefficients. We translateeach θi by applying Farkas’ lemma.
T HEOREM 4.4 (Farkas’ lemma). Consider the following system ofinequalities over real-valued variables x1 , . . . , xn .

c1,0 + c1,1 x1 + . . . + c1,n xn ≥ 0

 .
..
..

 ..
.
.
cm,0 + cm,1 x1 + . . . + cm,n xn ≥ 0
11 We assume that constant types only embed quantifier-free linear arithmetic refinement predicates.

The system is unsatisfiable iff there exist non-negative reals r0 , r1 ,. . . , rm such that
• r0 + r1 c1,0 + · · · + rm cm0 = −1, and• r1 c1,j + · · · + rm cmj = 0 for each j = 1, . . . , n.

Farkas’ lemma is incomplete for integers because the “onlyif” direction does not always hold. (Trivially, the “if” direction
holds even for integers.) The incompleteness, however, has notaffected the experiments in Section 5. (See Section 4.3 for the listof limitations with our approach.)
E XAMPLE 4.5. Recall the constraints generated from the SHP
template dT in Example 4.3. We translate the constraints to theequivalent form below.
∀x,y, z.

p4 x−p4 z ≥ 0 ∧
−p4 x+p4 z ≥ 0 ∧ ¬  p1 p4 + p2 +p1 p4 x −(p1 p4 + p2 )y +p2 z ≥ 0 ∧  −p p − p −p p x +(p p + p )y −p z ≥ 0 ∧ 
1 4
2
1 4
1 4
2
2
−1
+x
−y
≥ 0
Applying Farkas’ lemma, the constraint is further translated to thefollowing form.
∃r0 , r1 , r2 , r3 , r4 ≥ 0.
r0 + (p1 p4 + p2 )(r3 − r4 ) − r5 = −1 ∧p4 (r1 − r2 ) + p1 p4 (r3 − r4 ) + r5 = 0 ∧−(p1 p4 + p2 )(r3 − r4 ) − r5 = 0 ∧−p4 (r1 − r2 ) + p2 (r3 − r4 ) = 0
We reduce the constraints to SAT by modeling integers as bitvectors, and apply SAT solving to find a satisfying assignment. A
possible solution is
p0 = 0, p1 = 1, p2 = 0, p3 = 0, p4 = 1
r0 = 1, r1 = 0, r2 = 0, r3 = 0, r4 = 1, r5 = 1
And from the solution, we obtain the substitutionρ = {p0 7→ 0, p1 7→ 1, p2 7→ 0, p3 7→ 0, p4 7→ 1}
Note that applying the inferred parameter substitution ρ to dT
results in the program equivalent to dS from Example 4.2. Finally,
we update the parameter substitution P via PT ρ to translate theinput program, which results in the program dP from Example 4.1,
and is typable by the underlying type system. While the example
only require a variable as the instantiation expression, this is not
the case in general (even when the instantiations are restricted tolinear arithmetic expressions). Section 5 shows examples needing
non-variable instantiation expressions.
We use the iterative approach of Gulwani et al. [9] to model integers as bit-vectors: we start with a low number of bits, and gradually increase the number of bits until a solution is found. Becauseof the incompleteness limitation, it is possible that a solution is notfound even though the process is given an infeasible SHP. (cf. Section 4.3.) Section 5 shows heuristics for coping with the issue.
New candidate types with new parameter substitutions It is often
desirable to infer new candidate types along with the new parameter
substitutions. For instance, in Example 4.5, rather than returning to
Step 1 of Figure 10 after the updated parameter substitution PT ρ isinferred, it is better to infer candidate types for the translated counterexample SHP dT ρ so that the counterexample is immediately
eliminated from the future CEGAR iterations.
Inferring parameter substitution for prior counterexamples For
simplicity, we have shown how to infer a parameter substitution
for one counterexample SHP. In practice, it is better to record thecounterexamples that have been encountered (or, the constraints

generated from them), so that the inferred parameter substitution
is able to also refute the past counterexamples. This can be done
by a minor modification to the algorithm because constraints frommultiple counterexamples simply add up as conjunctions. We takethis approach in the implementation described in Section 5.
4.3

Limitations

Our type inference algorithm is incomplete as it is not able todecide the typability of all programs. This is expected because theunderlying problem (i.e., safety verification) is undecidable. Here,
we list the source of incompleteness.
(1) Like the predicate abstraction in first-order software model
checking [12], we restrict the refinement predicates to an efficiently
decidable first-order theory, such as the quantifier-free theory of
linear arithmetic. Consequently, there are programs, even ones thatare first-order, that we cannot verify. Also, predicate discovery
uses various heuristics such as interpolation, and is in generalincomplete even for the theory subset (but, there are approaches
to make this part complete [14]).
(2) As remarked in Section 4.1, we restrict instantiation expressions to linear arithmetic expressions. While this has been sufficientfor many cases, as we show in Section 5, there are programs that wecannot verify because of the restriction.12 (But, as we show there,
simple heuristics can often be used to handle such cases.)(3) The parameter substitution inference is invoked only when
the counterexample is untypable with the current substitutions, because otherwise it may simply infer the same substitutions. For
some programs, the parameter substitution inference becomes forever blocked because the program generates infinitely many counterexamples each of which can be refuted by just updating the candidate types.13 (See Section 5 for an example.)(4) As remarked in Section 4.2.2, Farkas’ lemma is incomplete
for integers.

5. Implementation and Experiments
We have implemented a prototype of the type inference algorithm
as an extension to the higher-order model checker MoCHi [18]. It
takes (direct-style and CPS) OCaml programs. We use CVC3 [2]for the SAT-based non-linear constraint solving described in Section 4.2.2. A web interface of the implementation and the benchmark programs from the experiments are available online [28].
We ran experiments on small but representative higher-orderprograms. Table 1 summarizes the results. The column S is thesize measured in the number of words in the program. O is thelargest order of the functions in the program. (Base-type values areorder-0, and order-n functions only take arguments of order less→→than n.) The column |−p | is the total number of the variables −pthat occur in the range of the parameter substitution template PT(cf. Section 4.2). #E is the number of extra parameters added before
each function-type parameter. (#E > 1 is used in the heuristics
described below.) #I is the number of CEGAR iterations. The
column T is the running time in seconds, and P/T is the fractionof the running time spent on the parameter substitution inference.
NV marks the programs that required non-variable instantiation
expressions. The experiments were conducted on a machine withIntel Xeon E5620 2.4GHz CPU and 4GB RAM.
Note that the programs are higher-order (i.e., O > 1). The programs are safe, but none of them can be verified by the previous
12 The limitation is also linked with (1) above, because allowing more
complex instantiations has no benefit when the underlying theorem provercannot decide formulas embedding them.
13 This is an instance of a more general issue with the parameter substitution
inference not inferring sufficiently general substitutions.

→program
S O |−
p | #E
d2
40 2
3
1
d3
56 3
10
1
fhnhn
26 2
2
1
repeat-add
51 2
51
app-leq
29 2
21
app-lin-ord2 37 2
2
1
app-lin-ord3 45 3
61
app-succ
50 2
51
app-succ0
50 2
5–
a-test-upd
80 2
92
a-checksum
76 2
6
2
a-max
78 2
8
1
l-forall-leq 69 2
81
l-len-append 126 2
22
1
l-isort
170 2
39
–

#I
T
2 0.43s
3 1.76s
1 0.15s
3 1.05s
1 0.26s
1 0.22s
1 0.96s
2 0.36s–—–
7 2.06s
8 3.38s
4 7.32s
2 2.68s
2 0.73s–—–

P/T NV
40%
68%
12%
7%
41% X
38% X
84% X
37%
—%
32%
29%
26%
51%
35% X
—%

Table 1. Experiment results.
refinement type systems proposed for automated higher-order program verification [13, 18, 23, 26, 27]. We describe each program.
• d2 and d3 are from Example 3.4.
• fhnhn compares the return value of two function arguments:

let f x y = assert (x () = y ()) in
let h x () = x in let main n = f (h n) (h n)• repeat-add makes the closure add n for some n ≥ 0, applies

it to 0 for k-times for some k > 0, and asserts that the result is
not less than n:
let add x1 x2 = x1 + x2 in
let rec repeat f k x = if k <= 0 then x
else f (repeat f (k - 1) x) in
let main n k =if n >= 0 && k > 0 thenassert (repeat (add n) k 0 >= n)• app-leq (resp. app-lin-ord2) is the program below with e≡ (a<=b) (resp. e ≡ (4*a+2*b)).
let app f x = f x inlet check x y = assert (x = y) in
let main a b = app (check e) e
• app-lin-ord3 is app-lin-ord2 “lifted” one order higher.
• app-succ calls check i i for some non-deterministically-

chosen i ≥ n:
let succ f x = f (x + 1) in
let rec app f x =if * then app (succ f) (x - 1) else f x inlet check x y = assert (x = y) in
let main n = app (check n) n
• app-succ0 is app-succ with n in the body of main fixed to 0.
• In a-xxx, we model and check array manipulating programs.

We model an array as the pair consisting of its size and thefunction that maps indices to the array elements:
let make array n =(n, fun i -> assert (0 <= i && i < n); 0)
let upd (n, ar) i x =assert (0 <= i && i < n);(n, fun j -> if j = i then x else ar j)

The array benchmarks extend the ones from the previous work[18] that demonstrate the application of higher-order program
verification to the verification of data structure properties.
a-test-upd tests array updates. It creates an array of size n
and updates the i-th element to x for some i ∈ {0, . . . , n − 1}.
The program then reads the element and checks that the result
is equal to x as expected:
let test (n, ar) i x = assert (ar i = x) in
let main n i x =if 0 <= i && i < n thentest (upd (make array n) i x) i x
Note that the program also checks for array bounds violation.
a-checksum creates an array of size 2, updates the first andthe second elements to a and b respectively, and asserts that thesum of the two array elements equals a + b:
let checksum (n, ar) x =assert ((ar 0) + (ar 1) = x) in
let main a b =checksum(upd (upd (make array 2) 0 a) 1 b) (a + b)
a-max creates an array of size n whose elements are from theset {0, . . . , x} where x > 0, computes the maximum element mof the array, and asserts that m ≤ x.
• The programs l-xxx model and check list operations. We

model a list by a pair of its length and a function from a nonnegative integer i to the i-th element. We model the core list
operations as follows:
let nil = (0, fun i -> assert false)
let cons a (len, l) =(len + 1, fun i -> if i=0 then a else l (i-1))
let hd (len, l) = l 0
let tl (len, l) = (len - 1, fun i -> l (i + 1))
let is_nil (len, l) = len=0
l-forall-leq creates a list of the length n whose i-th element is n − i, and asserts that x ≤ n holds for all element x of
the list.
l-len-append appends two lists of the length len1 andlen2, computes the length of the resulting list, and asserts that
it is not greater than len1 + len2.
l-isort creates a list, sorts the list via an insertion sort, andthen checks that the result is actually sorted.
The implementation was able to successfully verify the programs by automatically inferring appropriate extra parameter substitutions, except for app-succ0 and l-isort. Before we discuss
the reason for failure on these two, we describe the heuristic thatwas needed for verifying a-test-upd and a-checksum.
Recall that we limit instantiation expressions to linear arithmetic expressions. With this restriction, it can be shown thata-test-upd and a-checksum (and also l-isort) are actuallyuntypable when we are allowed to add only one extra parameter before a function-type parameter.14 However, a-test-upd anda-checksum can be typed if we are allowed to add two extra parameters before a function-type parameter, even with the linearinstantiation-expression restriction. (Note that #E is 2 for these
programs in Table 1.)
For instance, in a-checksum, to show the safety of the call tochecksum, we need to infer the property that the second argument
14 Note that the relative completeness theorem (Theorem 3.7) assumes that

arbitrary side-effect-free integer-type expressions can be used for instantiation.

equals the sum of the first and the second elements of the functionencoded array passed as the first argument. Because the two elements of the array are independent (i.e., the arguments a and b ofmain), it is not possible to express such a fact via a refinement typewith just one (linearly instantiatable) extra parameter. Nonetheless,the property can be expressed even under the linear-instantiationexpression restriction by using two extra parameters. For example,
the following type is sufficient:∀a:int.∀b:int.
(int × (x:int → {u | θ})) → {u | u = a + b} → ⋆where θ ≡ (x = 0 ⇒ u = a) ∧ (x = 1 ⇒ u = b), and × isthe pair type constructor. We use a simple heuristic to progressively
increase the number of extra parameters that are added before eachfunction-type parameter: we increment the number by one when
the parameter substitution inference fails to find a solution to theconstraints, with some pre-defined threshold on the number ofbits used in the bit-vector modeling (cf. Section 4.2.2). With theheuristic, the implementation was able to verify a-test-upd anda-checksum. Note that the increased extra parameter heuristic issound because the soundness theorem (Theorem 3.6) holds for any
pattern of extra parameter additions.
The program l-isort remains untypable even with the heuristic. In fact, it can be shown that no finite number of extra parameter
additions can type the program when the instantiation expressions
are restricted to be linear.
The implementation fails to verify app-succ0 for a different
reason. To verify the program, we need to infer the following typefor app with the extra parameter i.
∀i:int.f :({u | u = i} → ⋆) → x:{u | u = i} → ⋆However, each counterexample SHP generated from app-succ0 is
actually typable by assigning (the copies of) app the types of thefollowing form whose refinement predicates do not mention theextra parameter:∀i:int.f :({u | u = c} → ⋆) → x:{u | u = c} → ⋆where c is some integer constant. Therefore, the type inference
system generates infinitely many counterexample SHPs that are
refuted by the types of the above form each time, and the parameter
substitution inference is never invoked to infer the necessary typethat uses the extra parameter. We leave the issue for future work.

6. Related Work
6.1 Refinement Type Systems
The relatively complete refinement type system of this paper can beseen as DML [30] but with quantifiers (i.e., introduction of Π types)
restricted to one before each function-type parameter. Hence, ourresult shows that DML is actually relatively complete (even whenthe quantification pattern is restricted). In relation to DML, thispaper’s contribution is in actually proving relative completeness,and in proposing an automated type inference method.
The previous refinement type systems proposed for automatedhigher-order program verification [13, 18, 23, 26, 27] lack relativecompleteness, except for the case when the base-type data domain
is finite [16, 17]. We have shown how the type inference systems
underlying the verifiers may be extended to attain relative completeness.
6.2 Hoare Logic for Higher-order Languages
There is a long line of research on relatively complete Hoare logic
like proof systems for higher-order functional (or procedural) languages. One way to achieve relative completeness is to have ahigher-order logic as the interpretation logic (i.e., the logic for thedata part) so that the formulas can directly refer to higher-orderfunctions as data (see, e.g., [5, 11, 21, 22]). However, such an approach is difficult to automate as the client verifier must rely on ahigher-order logic theorem prover. The dilemma is similar to that
arising from explicitly encoding functions as base-type data in the
program logic.
The approach of using base-type encoding of functions toachieve relative completeness was first proposed by German etal. [6, 7]. (A similar approach is taken in [8].) Crucial to theirapproach is the idea of avoiding the explicit encoding in the program logic via quantification, allowing the client verifier to choose
appropriate quantifier instantiations. To our knowledge, no actual
verifier was built based on their program logic.
The encoding approach is also used in a recent work on relatively complete dependent (refinement) type system [19] where a
DML-like type system is extended with linear intersection types,
and is shown sound and relatively complete (for terminating programs). Their type system is designed for a type-based complexity
analysis, and the paper does not discuss automated verification.
6.3

Quantified First-order Logic Constraint Solving

Our type inference method utilizes an algorithm for deciding→→
the validity a FOL formula of the form ∃−x .∀−y .θ where θ is a→→quantifier-free arithmetic formula over the variables −x and −
y , and−→if valid, finding appropriate instantiations for x so that the formula→→→can be reduced to ∀−y .θ[−e /−x ].
The problem is studied in the context of constraint-based (or,template-based) program verification [4, 9, 24] where the existentially quantified variables are used to represent the unknowns in theinvariant template. The technique has found wide applicability, including hybrid system verification [20] and program synthesis [25].
Our work adds higher-order program verification to the list.

7. Conclusion
We have presented an automated approach to a relatively complete verification of higher-order functional programs. Our work
extends the recent research on refinement type inference for automated program verification. We have extended the underlying refinement type system by adopting the classical result on relatively
complete Hoare logic like proof systems for higher-order procedural languages, which shows that certain extra base-type parameter
additions are sufficient for relative completeness. Then, we have extended the type inference system by utilizing the techniques fromthe recent work on quantified FOL constraint solving over template
expressions to infer appropriate instantiations for the extra basetype parameters.
Acknowledgments We thank the anonymous reviewers for usefulcomments. This work is partially supported by Kakenhi 23220001
and 23700026.

References[1] L. Augustsson. Cayenne - a language with dependent types. In ICFP,
pages 239–250, 1998.
[2] C. Barrett and C. Tinelli. CVC3. In CAV, pages 298–302, 2007.
[3] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith.
Counterexample-guided abstraction refinement. In CAV, pages 154–
169, 2000.
[4] M. Colón, S. Sankaranarayanan, and H. Sipma. Linear invariant
generation using non-linear constraint solving. In CAV, pages 420–
432, 2003.
[5] W. Damm and B. Josko. A sound and relatively∗ complete Hoarelogic for a language with higher type procedures. Acta Inf., 20:59–101,
1983.

[6] S. M. German, E. M. Clarke, and J. Y. Halpern. Reasoning aboutprocedures as parameters. In Logic of Programs, pages 206–220,
1983.
[7] S. M. German, E. M. Clarke, and J. Y. Halpern. Reasoning aboutprocedures as parameters in the language L4. Inf. Comput., 83(3):265–
359, 1989.
[8] A. Goerdt. A Hoare calculus for functions defined by recursion onhigher types. In Logic of Programs, pages 106–117, 1985.
[9] S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis asconstraint solving. In PLDI, pages 281–292, 2008.
[10] C. A. R. Hoare. An axiomatic basis for computer programming.
Commun. ACM, 12(10):576–580, 1969.
[11] K. Honda, M. Berger, and N. Yoshida. Descriptive and relative completeness of logics for higher-order functions. In ICALP (2), pages
360–371, 2006.
[12] R. Jhala and R. Majumdar. Software model checking. ACM Comput.
Surv., 41(4), 2009.
[13] R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: Verifying functional programs using abstract interpreters. In CAV, pages 470–485,
2011.
[14] R. Jhala and K. L. McMillan. A practical and complete approach topredicate refinement. In TACAS, pages 459–473, 2006.
[15] T. Johnsson. Lambda lifting: Transforming programs to recursive
equations. In FPCA, pages 190–203, 1985.
[16] N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416–428, 2009.
[17] N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal
mu-calculus model checking of higher-order recursion schemes. In
LICS, pages 179–188, 2009.
[18] N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In PLDI, pages 222–233,
2011.
[19] U. D. Lago and M. Gaboardi. Linear dependent types and relativecompleteness. In LICS, pages 133–142, 2011.
[20] J. Liu, N. Zhan, and H. Zhao. Computing semi-algebraic invariants
for polynomial dynamical systems. In EMSOFT, pages 97–106, 2011.
[21] E.-R. Olderog. Correctness of programs with Pascal-like procedures
without global variables. Theor. Comput. Sci., 30:49–90, 1984.
[22] B. Reus and T. Streicher. Relative completeness for logics of functional programs. In CSL, pages 470–480, 2011.
[23] P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI,
pages 159–169, 2008.
[24] S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Constraint-based
linear-relations analysis. In SAS, pages 53–68, 2004.
[25] S. Srivastava, S. Gulwani, and J. S. Foster. From program verification
to program synthesis. In POPL, pages 313–326, 2010.
[26] T. Terauchi. Dependent types from counterexamples. In POPL, pages
119–130, 2010.
[27] H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP, pages 277–288, 2009.
[28] H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs, 2012. http://www.kb.is.s.u-tokyo.ac.jp/~uhiro/relcomp.
[29] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38–94, 1994.
[30] H. Xi and F. Pfenning. Dependent types in practical programming. In
POPL, pages 214–227, 1999.