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 in1 In fact, the equivalence of model checking and refinement type inference
has been shown for the finite domain base-type data case [16, 17].

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’13, January 23–25, 2013, Rome, Italy.
Copyright c 2013 ACM 978-1-4503-1832-7/13/01. . . $10.00

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,
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. Appendix contains the materials omitted from the main
body of the paper.

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

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.
the assume and assertion expressions assume x and assert x, andpartial 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→→e0 −e for the series of applications e0 e1 e2 . . . en where −e =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,or aborts with an assertion failure. The typing rules for the simple
type system are standard and are deferred to Appendix A.

τ, σ

::=

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

Figure 6. The syntax of refinement types.
sty(κ) ∈→sty(x) = intVbVfΓ ⊢ x : {u | u = x}Γ ⊢ κ : Γ(κ)Γ ⊢ c : ty(c)CstΓ ⊢ 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 Appendix B 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:σ−→ → ⋆.
x:σ∆(F ) = −−−−→(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 → ⋆.
A program d is said to be well-typed if ∃∆.∆ ⊢∀ d.

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

1

1

1

8 We extend the typing rules to (non-A-normal-form) side-effect-free
integer-type expressions in the obvious way. See Appendix C.

→
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 Appendix D.
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 Appendix E. The proof adopts the ideas fromthe work on relatively complete program logics for higher-orderprocedural 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 that the refinement
type system is relatively complete for first-order programs (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 expressing 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
c0 + c1 x1 + · · · + cn 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.2 Counterexample-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 Appendix F 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 ∧  −p1 p4 − p2 −p1 p4 x +(p1 p4 + p2 )y −p2 z ≥ 0 ∧ 
−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.

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

T
0.43s
1.76s
0.15s
1.05s
0.26s
0.22s
0.96s
0.36s
—–
2.06s
3.38s
7.32s
2.68s
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[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.

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.

[18] N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In PLDI, pages 222–233,
2011.

7. Conclusion[19] U. D. Lago and M. Gaboardi. Linear dependent types and relativecompleteness. In LICS, pages 133–142, 2011.

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.

[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.

[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.

A. Simple Type System
The syntax of simple types is defined by the following grammar:(Also shown in Section 3.)
s ::= ⋆ | int | s → s′The proof is by the usual syntactic approach [29] and is similar to
those of the previous work on refinement type systems [23, 27].

Γ ⊢s κ : Γ(κ) Γ ⊢s c : cty (c)s′sΓ ⊢s e1 : s Γ, x:s ⊢s e2 : ⋆ Γ ⊢ e : s → s Γ ⊢ y : sss′Γ ⊢ let x = e1 in e2 : ⋆Γ⊢ ey : sΓ ⊢s x : int Γ ⊢s e1 : ⋆ Γ ⊢s e2 : ⋆Γ ⊢s if x then e1 else e2 : ⋆ℓ(e1 ) ⇓ v b freshst ℓ in let x = e1 in e2 →d st ℓ, (b = v) in e2 [b/x](a = 1) ∈ ℓ b freshst ℓ in let x = assert a in e →d st ℓ, (b = 1) in e[b/x]Figure 11. The simple type system typing rules.
Figure 11 shows the typing rules of the simple type system. Here,cty (c) is the simple type of the constant c. We overload the symbols
Γ 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 [29]. (Recall that due to CPS, aprogram cannot return normally.)
T HEOREM A.2 (Simple Type Safety). Let d be simply-typed and→−→main −
x = emain ∈ d. Then, for any arguments i of main and any→ −−e such that emain [ i /→x ] →∗d e, either e = fail, e = safe, or there
exists e′ such that e →d e′ .

B. Sound and Precise Constant Types
For a constant operation c over integers, we say that the type−−−→
τ = x:int → {u | φ} is sound if the following properties allhold:(a = i) ∈ ℓ i 6= 1
st ℓ in let x = assert a in e →d fail(a = 1) ∈ ℓ b freshst ℓ in let x = assume a in e →d st ℓ, (b = 1) in e[b/x](a = i) ∈ ℓ i 6= 1
st ℓ in let x = assume a in e →d safe
st ℓ in if ∗ then e1 else e2 →d st ℓ in e1
st ℓ in if ∗ then e1 else e2 →d st ℓ in e2→
F−
x = e′ ∈ d−→→→st ℓ in F a →d st ℓ in e′ [−
a /−
x]
→
→
(b = F −a2 ) ∈ ℓ F −x = e′ ∈ d
→
→
→/−
→
st ℓ in b −a → st ℓ in e′ [−
a ,−
a
x]
1

d

2

1

Figure 12. The stack augmented reduction rules.
We augment the dynamic semantics with stacks so that the
run-time expressions are in A-normal forms. Figure 12 shows theaugmented reduction rules. Here, ℓ is a sequence of stack bindingsa = v such that v is a stack value defined by the following grammar→
v ::= i | F −aAlternatively, we may A-normalize the expressions and use thetyping rules from Section 3.1.

where i is an integer constant. (Here, we overload v to range overstack values.) We often use letters a, b for stack variables, andlet x, y, z, etc. range over arbitrary (i.e., stack, program, first-orderlogic) variables. Here ℓ(e) is defined to be e[v1 , . . . , vn /a1 , . . . , an ]where a1 , . . . , an are the free stack variables of e and ℓ(ai ) = vi
if e is an non-assume/assert integer operation (i.e., is of the form→c−a where c is a non-assume/assert constant), and otherwise, e is a→→→→a if κ ispartial application κ −a and ℓ(κ −a ) is defined to be F −
a1 −
−
→
−
→
a stack variable and ℓ(κ) = F a1 , or F a if κ is a function nameF . (I.e., we only dereference the function-type variable at the head
position so that the result of ⇓ is a stack value.) As with parameterand let-bound variables, we assume that bound stack variables are
distinct.
We redefine the semantics of a program d to be a series of−−−→→→
reductions starting from an initial state st a = i in emain [−
a /−
x]
−
→
→
−
where main x = emain ∈ d and i are integer arguments for main.
−−−→(Here, a = i are the series of stack bindings a1 = i1 , . . . , an = in→−where i1 , . . . , in = i .) As before, a program is said to be safe if
it cannot be evaluated to fail.
The following is immediate.

D. Proof of Theorem 3.6

L EMMA D.1. A program is safe with the original semantics iff it issafe with the stack semantics.

Theorem 3.6: If ∆ ⊢∀ d then d is safe.

Therefore, it suffices to prove Theorem 3.6 for the stack semantics.

• τ is closed.
• tshape(τ ) = cty(c). (cf. Appendix A.)

→
−

→
−

→
−

→
• For any i in the input domain of c, φ[ i /−x ][[[c]]( i )/u] = ⊤.
→ →−We say that τ is precise if in addition to the above, φ[ i /−x ][j/u] =→−⊥ for j 6= [[c]]( i ). For example, for a 0-ary operators (i.e., constant integer) c, the precise types are of the form {u | u = c}.
While a non-assert constant operator in our language accepts all
inputs in its domain, behaviors such as the divide-by-zero error canbe modeled by inserting appropriate assert statements.

C. Typing pureExps
We add the rule below to type (non-A-normal-form) side-effectfree integer-type expressions.
Γ ⊢∀ c : y :σ → τ Γ ⊢∀ o : σΓ ⊢∀ c o : τ [o/y]We extend the typing rules to type the stack augmented intermediate expressions. (We equate st ε in e with e.)Γ ⊢∀ v : σ Γ, a : σ ⊢∀ st ℓ in e : ⋆StΓ ⊢∀ st (a = v), ℓ in e : ⋆We also add the following so that safe is always typable.
Γ ⊢∀ safe : ⋆Safe

The following is immediate from the property of sound constanttypes (Appendix B).
L EMMA D.2. Suppose o ∈ pureExps and Γ ⊢ o : {u | θ}. Then,[[Γ]] ⇒ ∃u.θ.
The following lemma states that to we can derive Γ ⊢∀ e : ⋆by binding a fresh variable bound to the type of a side-effect-free
integer-type expression in scope.
L EMMA D.3. Suppose Γ ⊢∀ o : τ and Γ, x : τ ⊢∀ e : ⋆ such thato ∈ pureExps and x ∈/ fv(e). Then, Γ ⊢∀ e : ⋆. (Note that weassume x ∈/ dom(Γ).)
Proof: By inspection of the ⊢∀ typing rules, the binding of the
non-occurring variable x can affect the type derivation of e in only
two ways: (1) by using x as a sub-expression of the instantiating
expression at Inst, or (2) by having x : τ in the left hand side of ⇒within the FOL formula denoting the assumptions about the basetype variables in the environment at the subtyping judgement Sb.
In the case (1), any such use of x can be substituted by o toattain the same effect. In the case (2), suppose τ = {u | θ}. Then,in Sb, θ may only occur as φ1 ∧ θ[x/u] ⇒ φ2 such that x does
not occur free in φ1 , φ2 , or θ. Therefore, the formula is logically isequivalent to φ1 ∧ ∃u.θ ⇒ φ2 . By inspection of the typing rules,
φ1 must be such that φ1 ⇒ [[Γ]]. Also because Γ ⊢∀ o : {u | θ}and o ∈ pureExps , it follows that [[Γ]] ⇒ ∃u.θ by Lemma D.2.
And, we can derive the instance of Sb without the binding. 2
We state a couple of substitution lemmas.
L EMMA D.4 (Substitution I). Suppose Γ ⊢∀ y : σ and Γ, x :σ ⊢∀e : ⋆. Then, Γ ⊢∀ e[y/x] : ⋆.
Proof: By induction on the derivation. 2
L EMMA D.5 (Substitution II). • Suppose Γ ⊢∀ y : σ1 , andΓ, x:σ1 ⊢∀ σ2 ≤ σ3 . Then, Γ ⊢∀ σ2 [y/x] ≤ σ3 .
• Suppose Γ ⊢∀ o : σ1 , o ∈ pureExps , and Γ, x : σ1 ⊢∀ σ2 ≤σ3 . Then, Γ ⊢∀ σ2 [o/x] ≤ σ3 .
Proof: By induction on the derivation. 2
Given type environments Γ1 and Γ2 , let Γ1 , Γ2 denote the typeenvironment formed by appending the two in sequence in thatorder. It suffices show the following preservation lemma to prove
the theorem.
L EMMA D.6 (Preservation). Suppose ∆ ⊢∀ e : ⋆ and e →d e′ .
Then, ∆ ⊢∀ e : ⋆.
Proof: We prove by case analysis on the reduction relation.
Suppose e is of the form st ℓ in let x = e1 in e2 and e1 isneither an assume nor assertion expression. Then, ∆ ⊢∀ e : ⋆and e →d e′ imply that we must have ∆, Γ ⊢∀ v : σ and∆, Γ, x : σ ⊢∀ e2 : ⋆ where ℓ(e1 ) ⇓ v and Γ is the bindings
from the stack ℓ formed by St. Therefore, by Lemma D.4 and St,
we have ∆ ⊢∀ st ℓ, (b = v) in e2 [b/x] : ⋆.
Suppose e is of the form st ℓ in let x = assert a in e1 .
Then, ∆ ⊢∀ e : ⋆ and e →d e′ imply that we must have∆, Γ ⊢∀ a : {u | u = 1} and ∆, Γ, x : {u | u = 1} ⊢∀ e1 : ⋆where Γ is the bindings from the stack ℓ formed by St. Therefore, it must be the case that (a = 1) ∈ ℓ, and we havee →d st ℓ, (b = 1) in e1 [b/x]. Hence, by Lemma D.4 and St,
we have ∆ ⊢∀ st ℓ, (b = 1) in e1 [b/x] : ⋆.
Suppose e is of the form st ℓ in let x = assume a in e1 . Then,∆ ⊢∀ e : ⋆ and e →d e′ imply that we must have ∆, Γ, x :{u | a = 1 ∧ u = 1} ⊢∀ e1 : ⋆ where Γ is the bindings fromthe stack ℓ formed by St. Therefore, if (a = 1) ∈ ℓ, then e →dst ℓ, (b = 1) in e1 [b/x]. Therefore, by Lemma D.4 and St, wehave ∆ ⊢∀ st ℓ, (b = 1) in e1 [b/x] : ⋆. Otherwise, (a = i) ∈ ℓsuch that i 6= 1. Then, e →d safe and we have ∆ ⊢∀ safe : ⋆.
Suppose e is of the form st ℓ in if ∗ then e1 else e2 andst ℓ in if ∗ then e1 else e2 →d st ℓ in e1 . Then, ∆ ⊢∀ e : ⋆imply that we must have ∆, Γ ⊢∀ e1 : ⋆ where Γ is the bindings
from the stack ℓ formed by St. Therefore, by St, we have ∆ ⊢∀st ℓ in e1 . The case st ℓ in if ∗ then e1 else e2 →d st ℓ in e2
is analogous.
→→
Suppose e is of the form st ℓ in F −a . Let −a = a1 , . . . , an .
→Then, ∆ ⊢∀ e : ⋆ and e →d e′ imply that we must have −
γ →⋆
−
→
−
and sequences of pure integer-type expressions o0 , . . . , o→n such
that
→
−
−→
−−−→
−−−→
γ = ∀−
y−0 :τ0 , x1 :σ1 , ∀y1 :τ1 , x2 :σ2 , . . . , xn :σn , ∀yn :τn→∆, Γ ⊢∀ F : −γ →⋆and for 0 ≤ i ≤ n and 1 ≤ j ≤ ni ,∆, Γ ⊢∀ ai : σi ρi∆, Γ ⊢∀ oij : τij ρij
ρ−1 = ερi = ρini [oini /yini ]ρij = ρi−1 [oi0 /yi0 ] . . . [oij−1 /yij−1 ]→where Γ is the bindings from the stack ℓ formed by St, and |−oi | =−→−→′
ni for 0 ≤ i ≤ n. Let F xi = ebod ∈ d. Then, we must have γ → ⋆such that
−−−→
−−−→
−−−→
→
−
γ = ∀y0 :τ0′ , x1 :σ1′ , ∀y1 :τ1′ , x2 :σ2′ , . . . , xn :σn′ , ∀yn :τn′→−∆, h γ ′ i ⊢∀ ebod : ⋆′From the rule of subtyping, we have ∆, Γ, hγ ′ |ij i ⊢∀ τij ≤ τij
foreach i, j where γ ′ |ij is the prefix of γ ′ up the binding just before
yij : τij , and ∆, Γ, hγ ′ |i i ⊢∀ σi ≤ σi′ for each i where γ ′ |i is theprefix of γ ′ up the binding just before xi : σi . Therefore, by Sub′
and Lemma D.5, we have ∆, Γ ⊢∀ oij : τijand ∆, Γ ⊢∀ ai : σi′for each i, j. Then, by Lemma D.4, Lemma D.3, and St, we have→→∆ ⊢∀ st ℓ in ebod [−a /−x ] : ⋆.
→
The case e is of the form st ℓ in b −a1 is analogous. 2
Finally, Theorem 3.6 follows from Lemma D.6 because, given∆ such that ∆ ⊢∀ d, we have ∆ ⊢∀ einit : ⋆ for any initial state−−−→→→
einit = st a = i in emain [−a /−x ], and ∆ 6⊢∀ fail : ⋆.

E. Proof of Theorem 3.7
Theorem 3.7: If d is safe, then there exists ∆ such that ∆ ⊢∀ d and→ushape(∆(F )) = sty(F ) for each F −x = e ∈ d.
Following [6–8], we encode functions as integers via Gödelnumbering. We define concrete value (simply value, henceforth),v, to be a simply-typed expression defined by the following grammar.15
v ::= F | i | v1 v2Here, i is an integer constant. We define applicable term (simply
term, henceforth), t, to be a simply-typed expression defined by thefollowing grammar.
−→
t ::= x | F | t1 t2 | c t
15 Note that this is different from the notion of “value” used in the dynamic

semantics (cf. Section 3 and Appendix D).

wpre(e, ψ) ≡ θ
wpre(let x = t in e, ψ) ≡ θ[⌈t⌉/x]wpre(e, ψ) ≡ θ
wpre(let x = assert y in e, ψ) ≡ y = 1 ∧ θ[1/x]wpre(e, ψ) ≡ θ
wpre(let x = assume y in e, ψ) ≡ y = 1 ⇒ θ[1/x]wpre(e1 , ψ) ≡ θ1 wpre(e2 , ψ) ≡ θ2
wpre(if ∗ then e1 else e2 , ψ) ≡ θ1 ∧ θ2
→
−
→
−
→
wpre(t t , ψ) ≡ (∀−α .ψ)[⌈t t ⌉/xhd ]Figure 13. Weakest preconditions.

transformer.
step(ψ) ≡
→
→
→
→
−
→ −
→
−
∀F, −
v . ⌈F −v ⌉ = xhd ⇒ wpre(eF , ψ)[⌈−
v ⌉/−
α ||→
v | ][ x / y ]
→
→
−
→
−
→ maxargs .
−where F = eF ∈ d, −x = −α |maxargs−|→−v | , and y = α ||→
v |+1
−
→
Note that fv(step(ψ)) ⊆ {x , α }.
hd′′
We write e →n
d e if e can be reduced to e by making at most nfunction calls. We show the correctness of the weakest precondition
predicate transformer.

L EMMA E.1. Suppose ψ = step n (⊤).
→→
(1) Let e be a CPS sub-expression of d, fv(e) = {−x }, and −
v be
→
−
−
→
values such that e[ v / x ] is simply typed. Then,
→
→
e[−
v /−
x ] 6→n faild→→iff θ[⌈−v ⌉/−x ] is valid where θ = wpre(e, ψ).
→−→−(2) Let F v1 v2 be a simply-typed total application. Then,→→v 6→n fail
F−
v −
1

→
−
where c t is a total application of a non-assume/assert constant.
→
Note that any value is a term. Given a term t with free variables −x,→→
we define the evaluation relation t[−v /−x ] ⇓val v in the obvious→→
way: v is t[−v /−x ] with all constant operator applications in thesubexpression reduced to integer constants.
For a value v, we write ⌈v⌉ to denote the Gödel number that
encodes v. We let ⌈i⌉ = i for an integer constant i. (Collisions between function-type and integer-type values can always be avoided
in our setting because the program is assumed to be simply typed.)
For each variable x, we introduce a distinct base-type (i.e., integer→
x for the sequence x1 , . . . , xn wheretype) variable x. We write −→→−x}
x = x1 , . . . , xn . We write fv(t) for the set of variables {−→where fv(t) = {−x }.
For a term t, we define ⌈t⌉ to be the integer-type term of over
fv(t) that encodes t. More formally, ⌈t⌉ is the integer term thatsatisfies
→
→
→
→
→
∀v, −
v .(t[−v /−x ] ⇓ v) ⇔ (⌈t⌉[⌈−v ⌉/−x ] = ⌈v⌉)val−→
where →
x = fv(t), and ⌈−v ⌉ is the sequence ⌈v1 ⌉, . . . , ⌈vn ⌉ where→−16v = v1 , . . . , vn .
Let maxargs be the maximum number of function arguments of→→d, that is, maxargs = max{|−x|| F −
x = ∈ d}. Without loss ofgenerality, we assume that each function of d has the same function→−→−
argument names, that is, there exists β such that | β | = maxargs→−→→
and for each F −x = ∈ d, −x is a prefix of β . (Note that thevariables of the same name in different functions need not have the→−same simple type.) In the rest of the proof, we fix the variables β
to be the sequence of function arguments of the program d. Let→−→−α = β . We also introduce a special base-type variable xhd that is→
distinct from −α.
→Let ψ be a formula such that fv(ψ) ⊆ {xhd , −α }. We intend→
to use ψ(xhd , −α ) to express the condition for which it is safe to→call the function encoded by xhd via the arguments encoded by −α.
We say that an expression is a CPS expression if it is given thesimple type ⋆ (e.g., a function body). Figure 13 shows the rules forderiving wpre(e, ψ) for a CPS expression e. Intuitively, wpre(e, ψ)is the condition safe to evaluate e assuming that ψ is the condition→
safe to call the functions. Note that fv(wpre(e, ψ)) ⊆ {−
α }.
→
−
→
Let x |m denote the first m elements of the sequence −x , and→−x |ndenotethesequenceofelements
from
the
mth
element
tom→the nth element of −x . We define the weakest precondition of
the program by taking the fixed point of the following predicate

2

d

→
→
→
→| ] is valid.
iff ψ[⌈F −v1 ⌉/xhd ][⌈−
v2 ⌉/−
α ||−v
2Proof: We prove by induction on n and e. First, we show (1) byinduction on e, assuming that (2) holds.
→→
Suppose e is let y = t in e1 . Then, e[−v /−x ] 6→nd fail iff
n
−
→
−
→
e [v/y][ v / x ] 6→ fail
1

d

→
→
where t[−v /−x ] ⇓val v. By induction hypothesis, the latter holds iff→−→′
x ] is valid where θ′ = wpre(e1 , ψ). Therefore,θ [⌈v⌉/y][⌈ v ⌉/−
→
→
→
→
e[−
v /−
x ] 6→nfailiff θ′ [⌈v⌉/y][⌈−v ⌉/−x ] is valid.
d→→Suppose e is let y = assert z in e1 . Then, e[−v /−x ] 6→nd fail→−→−iff z[ v / x ] = 1 and→→e [1/y][−v /−x ] 6→n fail
1

d

→
→
v ⌉/−
x]
By induction hypothesis, the latter holds iff θ′ [1/y][⌈−
′
−
→
−
→
n
where θ = wpre(e1 , ψ). Therefore, e[ v / x ] 6→d fail iff→→(z = 1 ∧ θ′ [1/y])[⌈−v ⌉/−x](Recall that we let ⌈i⌉ = i for an integer constant i.) The case e islet y = assume z in e1 is similar.
→→
Suppose e is if ∗ then e1 else e2 . Then, e[−v /−x ] 6→nd fail
→
→
−
→
−
→
n
iff e1 [−v /−x ] 6→n
fail
and
e
[
v
/
x
]
→
6
fail.
By
induction
2
d
d
→
→
→
→
v ⌉/−
x ] where
hypothesis, the latter holds iff θ1 [⌈−v ⌉/−x ] and θ2 [⌈−→→θ1 = wpre(e1 , ψ) and θ2 = wpre(e2 , ψ). Therefore, e[−v /−x ] 6→nd→−→−
fail iff (θ1 ∧ θ2 )[⌈ v ⌉/ x ] is valid.
−
→
→
→
→
Suppose e is a total application t t . Let e[−v /−x] = F −
v1 .
→
−
→
−
→
−
→
Then, by (2), F −v1 6→n
fail
iff
ψ[⌈F
v
⌉/x
]
(i.e.,
θ[⌈
v
⌉/
x
])
is
1
hd
d
valid.
Next, we show (2) by induction on n. The case n = 0 is trivial.
→
Suppose that (1) and (2) hold for n − 1. Let F −z = eF ∈ d. Then,
→
−
→ −
→ −
→
→
v2 6→nby (1), F −v1 −d fail iff θ[⌈ v1 , v2 ⌉/ z ] is valid where θ =wpre(eF , ψ ′ ) and ψ ′ = step n−1 (⊤). Therefore, by the definition
→
−
→
−
→ −
→ → ] is valid.
→
v2 6→nof step, F −v1 −d fail iff ψ[⌈F v1 ⌉/xhd ][⌈ v2 ⌉/ α ||−v2 |2The least fixed point of step is the following formula. (Least in
the order of logical implication.)Ψwp ≡ ∀n.step n (⊤)
Note that Ψwp can be expressed as a FOL formula by using Gödelnumbering to encode the sequence of step applications. (This requires encoding the FOL formulas in the sequence.)
The following is immediate from the definition of Ψwp .
→L EMMA E.2. Let t1 t2 be a simply-typed application, and −α =→x :: −
x . Then,1

16 Note that the notation is consistent over values as ⌈v⌉ = ⌈v⌉.

→→
Ψwp [⌈t1 t2 ⌉/xhd ][−x /−α |maxargs−1 ] ⇔ Ψwp [⌈t1 ⌉/xhd ][⌈t2 ⌉/x1 ]u freshwpty(z, x, Y, int → ⋆) ≡ x:{u | (∀Y.Ψwp )[z/xhd ][u/x]} → ⋆s 6= ⋆→→
wpty(z, x :: −x , Y, int → s) ≡ x:int → wpty(z, −x , Y, s)s ∈→u, x′ fresh′

wpty (z, x, Y, s → ⋆) ≡ ∀x :{u | (∀Y.Ψwp )[z/xhd ][u/x]}.x:wpty (x′ , args(s), args − (s), s) → ⋆s ∈→ s′ 6= ⋆ x′ fresh→→wpty(z, x :: −x , Y, s → s′ ) ≡ ∀x′ :int.x:wpty (x′ , args (s), args − (s), s) → wpty (z, −x , Y, s′ )[x′ /x]]
Figure 14. Weakest precondition types.
From Lemma E.1, it follows that Ψwp expresses the weakest
precondition of the program. That is,→→
C OROLLARY E.3. Let F −v1 −v2 be a simply-typed total application.
→
→
→
→
→
→ ] is valid.
Then, F −v −v 6→ fail iff Ψ [⌈F −v ⌉/x ][⌈−
v ⌉/−
α| −
1

2

d

wp

1

hd

2

We prove a few auxiliary lemmas.
L EMMA E.8. Let t1 t2 be a simply-typed partial application. Let
τ1 = wpty(t1 ).

|v2 |In particular, the weakest precondition of main of a safe program must be a tautology, that is, it is safe to execute for all of its
inputs.
C OROLLARY E.4. Ψwp [⌈main⌉/xhd ] = ⊤ iff d is safe.
In the rest of the proof, we assume that d is safe. We use Ψwp
to build refinement types for d’s functions. Specifically, for eachfunction-type term, we define its weakest precondition refinement
type by the rules shown in Figure 14.
→→→
Here, args(−s → ⋆) is the prefix of −α such that |args(−
s →
→
−
→
−
⋆)| = | s |. We define args (s) to be the set of variables {−α} \{args (s)}. Then, given a function-type term t, we definewpty(t) ≡ wpty (⌈t⌉, args(sty(t)), args − (sty(t)), sty(t))
The following is immediate from the rules of constructing wpty.
L EMMA E.5. Let τ = wpty (t). Then, we have fv(τ ) ⊆ fv(t) andushape(τ ) = sty(t).
Proof: By induction on sty(t). 2(1) If sty(t2 ) = int, then τ1 = x:int → σ such that σ[⌈t2 ⌉/x] =wpty(t1 t2 ).
(2) Otherwise, sty(t2 ) ∈→, and wpty (t1 ) = ∀x : int.y :τ → σsuch that τ [⌈t2 ⌉/x] = wpty (t2 ) and σ[⌈t2 ⌉/x] = wpty (t1 t2 ).
Proof: We show (1). By the construction of wpty and the factthat t1 t2 is a partial application, it follows that τ1 is of the form
x1 : int → σ (i.e., because the wpty construction sets the refinement predicate of a non-last base-type argument to ⊤). Let
τ = wpty(t1 t2 ).
Suppose the last argument of τ and σ[⌈t2 ⌉/x1 ] is a base type.
From the construction, it is easy to see that τ and σ[⌈t2 ⌉/x] arealpha-equivalent, except for the refinement predicate in the last−→base-type argument. Let σ have n arguments so that σ = −x−i :σi →−→−→
⋆ with i = 2, . . . , n + 1, and x1 :: xi is a prefix of α . Let→−→x = x1 , . . . , xn+1 . Let −x |n also be the arguments of τ (i.e.,
via alpha-renaming). Let θτ and θσ [⌈t2 ⌉/x1 ] be the refinement
predicates in the last argument of τ and σ[⌈t2 ⌉/x1 ], respectively(i.e., θσ is the refinement predicate in the last argument of σ). Then,
we haveC OROLLARY E.6. Let τ = wpty (F ). Then, τ is a well-formed
type of F such that ushape(τ ) = sty(F ).

θτ = (∀Yτ .Ψwp )[⌈t1 t2 ⌉/xhd ][u/xn ]θσ [⌈t2 ⌉/x1 ] = (∀Yσ .Ψwp )[⌈t1 ⌉/xhd ][u/xn+1 ][⌈t2 ⌉/x1 ]Therefore, to prove Theorem 3.7, it suffices to show ∆ ⊢∀ d for∆ such that ∆(F ) = wpty(F ) for each F .

where Yτ = args − (sty(t1 t2 )), and Yσ = args − (sty(t1 )). Therefore, by Lemma E.2, it follows thatE XAMPLE E.7. For example, the program d2 from Example 3.4−→
has the following weakest precondition. (Here, we set β = x, y.)

→
−
→
θτ [−
x |n
2 / x |n−1 ] ⇔ θσ [⌈t2 ⌉/x]

Ψwp [⌈main⌉/xhd ] = ⊤∀i.Ψwp [⌈main i⌉/xhd ] = ⊤Ψwp [⌈check⌉/xhd ] = x ≤ y∀i.Ψwp [⌈check i⌉/xhd ] = i ≤ x∀i, j.Ψwp [⌈check i j⌉/xhd ] = i ≤ jΨwp [⌈app⌉/xhd ] = ∀i.x = ⌈check i⌉ ⇒ i ≤ y∀i.Ψwp [⌈app (check i)⌉/xhd ] = i ≤ x∀i, j.Ψwp [⌈app (check i) j⌉/xhd ] = i ≤ j

Therefore, σ[⌈t2 ⌉/x] = wpty(t1 t2 ) (via alpha-renaming).
Otherwise, the last argument of τ and σ[⌈t2 ⌉/x1 ] is a function
type (of the same simple type), and an analogous argument holds
for the refinement predicate in the type of the universally boundvariable just before the argument.
We show (2). By the construction of wpty and the fact thatt1 t2 is a partial application, it follows that τ1 is of the form
∀x : int.y :τ → σ (i.e., because the wpty construction sets therefinement predicate of a universally bound variable just before a
non-last function-type argument to ⊤). From the construction, it
follows that τ [⌈t2 ⌉/x] = wpty(t2 ). And, σ[⌈t2 ⌉/x] = wpty(t1 t2 )follows from the argument similar to (1).
2And, the corresponding weakest precondition types are shown below.
wpty(main) = x:int → ⋆wpty(check) = x:int → y :{u | x ≤ u} → ⋆wpty(app)= ∀x′ :int.fx :σ → y :{u | ∀i.x′ = ⌈check i⌉ ⇒ i ≤ u} → ⋆where σ = x:{u | ∀i.x′ = ⌈check i⌉ ⇒ i ≤ u} → ⋆.

L EMMA E.9. Suppose Γ ⊢∀ e : τ and [[Γ]] ⇒ x = t. Then,Γ ⊢∀ e : τ [t/x].

Proof: By Sub and the fact that if θ ⇒ ψ and θ ⇒ x = t thenθ ⇒ ψ[t/x]. 2
Note that for any term t, ⌈t⌉ ∈ pureExps . We are now ready tostate the main lemma.
L EMMA E.10. Let e be a CPS-sub-expression. Let ρ be the substitution such that ρ(x) = x if x is a base-type variable in e andρ(x) = x if x is a function-type variable in e. Let Γ be a typeenvironment for e such that [[Γ]] ⇒ wpre(e, Ψwp )ρ, and for eachfunction-type variable or function name κ ∈ dom(Γ), there exists
a term t such that fv(t) ⊆ dom(Γ), and Γ(κ) = wpty (t). Then,(A) For each integer-type sub-term t of e, Γ ⊢∀ t : {u | ⌈t⌉ρ = u}.
(B) For each function-type sub-term t of e, Γ ⊢∀ t : wpty (t).
(C) Γ ⊢∀ e : ⋆.
Proof: (A) follows from the definition of precise constant types(cf. Appendix B).
We show (B) by induction on t. The base case (i.e., t = x ort = F ) is immediate from the assumption. So, let t = t1 t2 . By
induction hypothesis, we have Γ ⊢∀ t1 : wpty(t1 ). If t2 is an
integer-type term, then the result follows from (A), Lemma E.8(1), and Lemma E.9. Otherwise, t2 is a function-type term, andthe result follows from Lemma E.8 (2), applying Inst with the
instantiating expression ⌈t2 ⌉ to instantiate t1 ’s type to wpty(t2 ) →wpty (t1 t2 ).
We show (C) by induction on e. Suppose e is let x = t in e1 . If
e1 is a base type, then by (A), we have→→
• For each function type variable x ∈ dom(h−γ i), h−γ i(x) =→γ i). (Namely, wewpty(x) with fv(wpty (x)) = {x} ⊆ dom(h−select x to be the one bound universally just before x.)

Let ∆ be such that ∆(F ) = wpty (F ) for each F . By→
Lemma E.10 (C) and Lemma E.11, we have ∆, h−γ i ⊢∀ e F : ⋆→→where ∆(F ) = −γ → ⋆, for each F −x = eF ∈ d. Because ∆−→is well-formed (cf. Corollary E.6) and ∆(main) = int → ⋆(cf. Corollary E.4), we have ∆ ⊢∀ d.

F. Constraint Generation Processsty(x) = int
cgen (Γ ⊢ x) = ({u | u = x}, ⊤)sty(κ) ∈→cgen (Γ ⊢ κ) = (Γ(κ), ⊤)cgen (Γ ⊢ c) = (ty(c), ⊤)(σ, θ1 ) = cgen (Γ ⊢ e1 ) (⋆, θ2 ) = cgen (Γ, x:σ ⊢ e2 )cgen (Γ ⊢ let x = e1 in e2 ) = (⋆, θ1 ∧ θ2 )(y :σ → τ, θ1 ) = cgen (Γ ⊢ e) (σ ′ , θ2 ) = cgen (Γ ⊢ x)cgen (Γ ⊢ e x) = (τ [x/y], θ1 ∧ θ2 ∧ cgen (Γ ⊢ σ ′ ≤ σ))[[Γ, x:τ ]] ⇒ wpre(e1 , Ψwp )ρ
where Γ ⊢∀ t : τ . Therefore, Γ, x : τ ⊢∀ e : ⋆ by induction
hypothesis, and by Let, we have Γ ⊢∀ e : ⋆. Otherwise, e1 isa function type (i.e., a partial application), and we have [[Γ, x :σ, x : τ ]] ⇒ wpre(e1 , Ψwp )ρ where σ = wpty (e1 ) and τ ={u | ⌈t⌉ρ = u}. Then, by induction hypothesis, we have Γ, x:σ, x:τ ⊢∀ e1 : ⋆. Therefore, by (B), Lemma D.3, and Let, we haveΓ ⊢∀ e : ⋆.
Suppose e is let x = assert y in e1 . We have[[Γ, x:{u | u = 1}]] ⇒ wpre(e1 , Ψwp )ρ
Therefore, by induction hypothesis, Γ, x : {u | u = 1} ⊢ e1 : ⋆.
Also, [[Γ]] ⇒ wpre(e, Ψwp )ρ ⇒ y = 1. Therefore, by Let andthe type of assert (i.e., x :{u | u = 1} → {u | u = 1}), we haveΓ ⊢∀ e : ⋆. The case e is let x = assume y in e1 is similar.
Suppose e is if ∗ then e1 else e2 . We have[[Γ]] ⇒ wpre(e1 , Ψwp )ρ
[[Γ]] ⇒ wpre(e2 , Ψwp )ρ
Therefore, by induction hypothesis, we have Γ ⊢∀ e1 : ⋆ andΓ ⊢∀ e2 : ⋆. Then, by If, Γ ⊢∀ e : ⋆.
→−→−Suppose e is a total application t t . Let t = t1 , . . . , tn ,→−and t′ = t t |n−1 . By (B), we have Γ ⊢∀ t′ : wpty(t′ ). Suppose sty(tn ) = int. Then, by (A), we have that Γ ⊢∀ tn :{u | ⌈tn ⌉ρ = u}. By the construction of wpty(t′ ), we have
θ = (∀Y.Ψwp )[⌈t′ ⌉/xhd ][u/x]→
where wpty (t′ ) = x :{u | θ} → ⋆, Y = args − (sty(t′ )) = {−α}\→−{x}, and x is the first element of of α (i.e., by alpha-renaming).
Therefore, by Lemma E.2, wpre(e, Ψwp )ρ ⇔ (⌈tn ⌉ρ = u ⇒ θ),and so [[Γ]] ∧ ⌈tn ⌉ρ = u ⇒ θ. Hence, it follows that Γ ⊢∀ e : ⋆.
The case sty(tn ) ∈→ is similar.
2
Also, the following is clear from the construction of wpty(F ).
→→L EMMA E.11. Let F −x = e ∈ d and wpty(F ) = −γ → ⋆. Then,F→• [[h−
γ i]] ⇒ wpre(eF , Ψwp )ρ, and(⋆, θ1 ) = cgen (Γ ⊢ e1 ) (⋆, θ2 ) = cgen (Γ ⊢ e2 )cgen (Γ ⊢ if ∗ then e1 else e2 ) = (⋆, θ1 ∧ θ2 )cgen (Γ ⊢ ⋆ ≤ ⋆) = ⊤θ1 = cgen (Γ ⊢ σ2 ≤ σ1 ) θ2 = cgen (Γ, x : σ2 ⊢ τ1 ≤ τ2 )cgen (Γ ⊢ x:σ1 → τ1 ≤ x:σ2 → τ2 ) = θ1 ∧ θ2u∈
/ fv([[Γ]])cgen (Γ ⊢ {u | θ1 } ≤ {u | θ2 }) = ∀u.([[Γ]] ∧ θ1 ) ⇒ θ2
Figure 15. The constraint generation rules.
Figure 15 shows the constraint generation rules. Here, cgen (Γ ⊢ e)returns a pair of a refinement type τ and a constraint θ suchthat Γ ⊢ e : τ is derivable if and only if θ is valid. Similarly,cgen (Γ ⊢ τ1 ≤ τ2 ) returns a constraint θ such that Γ ⊢ τ1 ≤ τ2 isderivable if and only if θ is valid.