Relatively Complete Refinement Type System for
Verification of Higher-Order Non-deterministic Programs
HIROSHI UNNO, University of Tsukuba, Japan
YUKI SATAKE, University of Tsukuba, JapanTACHIO TERAUCHI, Waseda University, Japan
This paper considers verification of non-deterministic higher-order functional programs. Our contribution
is a novel type system in which the types are used to express and verify (conditional) safety, termination,
non-safety, and non-termination properties in the presence of ∀-∃ branching behavior due to non-determinism.
For instance, the judgement ⊢ e : u :int ϕ(u) ∀∀ says that every evaluation of e either diverges or reducesto some integer u satisfying ϕ(u), whereas ⊢ e : u :int ψ (u) ∃∀ says that there exists an evaluation of ethat either diverges or reduces to some integer u satisfying ψ (u). Note that the former is a safety property
whereas the latter is a counterexample to a (conditional) termination property. Following the recent work on
type-based verification methods for deterministic higher-order functional programs, we formalize the idea on
the foundation of dependent refinement types, thereby allowing the type system to express and verify richproperties involving program values, branching behaviors, and the combination thereof.
Our type system is able to seamlessly combine deductions of both universal and existential facts withina unified framework, paving the way for an exciting opportunity for new type-based verification methods
that combine both universal and existential reasoning. For example, our system can prove the existence of apath violating some safety property from a proof of termination that uses a well-foundedness terminationargument. We prove that our type system is sound and relatively complete, and further, thanks to having bothmodes of non-determinism, we show that our types are closed under complement.
CCS Concepts: • Theory of computation → Programming logic; Program verification; • Software andits engineering → Formal software verification;
Additional Key Words and Phrases: Program Verification, Relative Completeness, Refinement Types, HigherOrder Programs, Non-Deterministic Programs
ACM Reference Format:
Hiroshi Unno, Yuki Satake, and Tachio Terauchi. 2018. Relatively Complete Refinement Type System for
Verification of Higher-Order Non-deterministic Programs. Proc. ACM Program. Lang. 2, POPL, Article 12(January 2018), 29 pages. https://doi.org/10.1145/3158100

1

INTRODUCTION

Recent years have seen remarkable advances in automated (and semi-automated) methods forverifying higher-order functional programs. Powerful verification methods have emerged for various
important classes of properties, including safety properties [Jhala et al. 2011; Kobayashi et al. 2011;
Ong and Ramsay 2011; Rondon et al. 2008; Terauchi 2010; Unno and Kobayashi 2009; Unno et al.
Authors’ addresses: Hiroshi Unno, Computer Science, University of Tsukuba, Japan, uhiro@cs.tsukuba.ac.jp; Yuki Satake,
Computer Science, University of Tsukuba, Japan, satake@logic.cs.tsukuba.ac.jp; Tachio Terauchi, Computer Science andEngineering, Waseda University, Japan, terauchi@waseda.jp.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires
prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2018 Association for Computing Machinery.
2475-1421/2018/1-ART12
https://doi.org/10.1145/3158100

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12

12:2

Hiroshi Unno, Yuki Satake, and Tachio Terauchi

2013; Zhu and Jagannathan 2013; Zhu et al. 2015], termination [Kuwahara et al. 2014; Vazou et al.
2014], non-termination [Hashimoto and Unno 2015; Kuwahara et al. 2015], and properties expressedin temporal logics such as LTL and linear modal µ-calculus [Koskinen and Terauchi 2014; Murase
et al. 2016].
However, the existing proposals are quite disparate in that they employ rather different techniques
to verify the different classes of properties. For instance, the termination verification proposed in[Kuwahara et al. 2014] and the linear modal µ-calculus verification proposed in [Murase et al. 2016]use program transformation to iteratively convert the verification problem to a (binary) reachability
problem [Cook et al. 2007, 2006] which is checked by a dependent-refinement-type-based safety
property verifier such as [Unno et al. 2013], whereas the non-termination verification of [Kuwahara
et al. 2015] uses predicate abstraction to iteratively build over and under approximations to reduce
the problem to that of higher-order model checking [Kobayashi 2009; Ong 2006]. (Recall that thetermination property asks that every evaluation of the given program terminates, whereas the
non-termination property is its converse and checks that the given program has a non-terminating
evaluation.)
It is our belief that the disparity partly comes from the fact that each class of properties concerns
only one side of non-determinism. That is, while properties such as safety and termination (and,more generally, any linear properties) only ask that a certain fact holds for every run of the program,properties such as non-termination only ask whether there exists a run that satisfies a certain fact.
Likewise, the disparity between safety and termination can be understood as the difference due tothe former asking that every value that can be obtained as the final result satisfies a certain fact
whereas the latter asking that there exists a value that can be obtained as the final result (for every
run, in both cases).
In the present paper, we take a step toward a more unified reasoning framework. Our contribution
is a novel type system that can express and verify both universal and existential behavior of the
program. Following the recent trend [Kobayashi et al. 2011; Koskinen and Terauchi 2014; Rondon
et al. 2008; Terauchi 2010; Unno and Kobayashi 2009; Unno et al. 2013; Vazou et al. 2014; Zhu
and Jagannathan 2013; Zhu et al. 2015], we formalize our approach as a dependent refinement typesystem. A dependent refinement type system allows types to embed predicates on program values,
thereby allowing precise type-based value-and-path-sensitive reasoning.
To support both modes of non-determinism, we qualify the types with “∀” and “∃” at appropriate
places. Specifically, each type is qualified with one of the four modes Q 1Q 2 where Q i is either ∀or ∃ (for i ∈ {1, 2}). Roughly, Q 1 specifies whether the fact expressed by the type holds for every
evaluation of the expression being typed (Q 1 = ∀) or there exists an evaluation for which the factholds (Q 1 = ∃), and Q 2 says whether the fact holds for every value obtained as the result of theevaluation (Q 2 = ∀) or there exists a final value for which the fact holds (Q 2 = ∃). For example,{u :int | u > 0} ∀∀ is the type of expressions satisfying the property that every evaluation of the expression either diverges or reduces to a positive integer value, whereas {u :int | u > 0} ∀∃ is the typeof expressions that always terminate and reduce to a positive integer value, and {u :int | u > 0} ∃∃is the type of expressions such that there exists an evaluation of the expression that reduces toa positive value. To also cope with non-determinism from program inputs (i.e., whether the program should behave in a certain way for every input or for some input), we further qualify thebindings in the type environment and the arguments of function types by ∀ or ∃. For example,(x :∀ int) → {u :int | u > x } ∀∃ is the type of functions that, given any integer argument x, always
returns some integer u greater than x. Likewise, (x : ∃ int) → {u :int | u > x } ∀∃ is the type offunctions where there exists an integer argument x such that every evaluation of the function with

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:3

the argument returns some integer u greater than x. The modes exhibit a natural form of duality,that is, ∀ = ∃, ∃ = ∀ and Q 1Q 2 = (Q 1 )(Q 2 ).1
The types enable a seamless combination of both universal and existential reasoning within asingle deduction system. To our knowledge, such a combination has not been fully explored in the
program verification literature, especially in the presence of higher-order functions (cf. Section 7
for further discussion). We briefly demonstrate the power of the combined reasoning by examples
in Section 2. We defer a more detailed exposition to the later sections of the paper.
We show that our type system enjoys a number of desirable meta-theoretic properties. First,
thanks to the duality property, the types are closed under complement. More precisely, for any
type σ , there is a (syntactically definable) complement type ¬σ that satisfies Jσ K ∩ J¬σ K = ∅ andJσ K ∪ J¬σ K = JT K where T is the simple type that σ and ¬σ refine. Here, Jσ K denotes the semanticsof the type σ and is, roughly, the set of expressions that behave according
q pc yto σ (cf. Section 5 forpc
details). As an example, let σid = (x :∀ int) → {u :int | u = x } ∀∀ . Then, σid is the set of functions
that takes an integer argument and either diverges
q pc yor returns the given integer. The complementpc¬σid is (x : ∃ int) → {u :int | u , x } ∃∃ , and ¬σid is the set of functions where there exists an
integer argument and an evaluationthat
integer value fromq pc y ofq thepcfunctionyq returns
q a different
pc y
pc y
the given argument. Indeed, σid ∩ ¬σid = ∅ and σid ∪ ¬σid = Jint → intK, where
Jint → intK is the set of partial (non-deterministic) functions from integers to integers.2
We also show that our type system is sound and relatively complete. Soundness says that if thetype judgement Γ ⊢ e : σ is derivable, then e ∈ JΓ ⊢ σ K, where JΓ ⊢ σ K is the semantics of the typeσ under the type environment Γ (cf. Theorem 6.12). Conversely, completeness says that e ∈ JΓ ⊢ σ K
implies that Γ ⊢ e : σ is derivable (cf. Theorem 6.25). As expected, the completeness result is relative
to the assumption that the background theory for refinement predicates is sufficiently expressible
to encode arbitrary functions definable in the target programming language [Damm and Josko
1983; German et al. 1983, 1989; Goerdt 1985; Honda et al. 2006; Olderog 1984; Reus and Streicher
2011; Unno et al. 2013]. Additionally, we need to assume that the background theory is sufficiently
expressible to handle termination of non-deterministic programs. As usual for type systems of thiskind, soundness is an imperative requirement that ensures the veracity of the verification result,while completeness says that, at least in theory, the verification system is as precise as possible.
We summarize the main contributions of the paper below.
• We present a novel type system for verification of non-deterministic higher-order functional
programs. The type system facilitates combined universal and existential reasoning, and isable to verify rich classes of properties including (conditional) safety, non-safety, termination,and non-termination.
• We show that the type system enjoys desirable meta-theoretic properties. Specifically, weshow that the type system is sound and relatively complete, and that the types are closed
under complement.
The rest of the paper is organized as follows. In Section 2, we give an informal overview of thetype system by examples, focusing on the combined reasoning aspect. Section 3 formalizes thetarget programming language, and Section 4 and Section 5 formally present the type system. For
exposition, we split the presentation in two parts so that we first present a simpler type systemthat is sound but incomplete in Section 4 and then describe the relatively-complete full type system
in Section 5. The simpler system lacks the intricacies that are needed for relative completeness,such as Gödel encoding of function-type values and intersection and union types. However, it issuited for conveying the essence of how universal and existential reasoning can be integrated in
1 We refer to Section 4 for the formal definition of the types.
2 Technically, for relative completeness, we need to restrict the domain of functions to the definable ones (cf. Section 6).

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:4

Hiroshi Unno, Yuki Satake, and Tachio Terauchi
e (a)

e (b)

let rec f x y =if x <= y then0else
f (x-1) yin
let x = 10**9 in
let y = 0 in
let z = * in(f x y) + z

let rec f x y =if x <= y then0
else
let w = * inif w > x thenf (x-1) y
else
f x y
in
let x = 10**9 in
let y = 0 in
let z = * in(f x y) + z{u :int | u = 1} ∃∃e (c)let rec app f x =if x > 0 thenapp f (x-1)
else
f x
in
let rec g x =if x = 0 then()else
app g xinlet b = * inif b then g (-1)
else (){u :int | u = 1} ∃∃{u :unit | ⊥} ∃∀Fig. 1. Examples and the corresponding propertiesa type system. Section 6 discusses the meta-theoretic properties of the type system. We discuss
related work in Section 7, and conclude the paper in Section 8. Omitted proofs are given in theextended version of this paper [Unno et al. 2017].
2

INFORMAL OVERVIEW

We give an informal overview of the type system, with the focus on demonstrating the power of
combined universal and existential reasoning.
Example 2.1. Consider the program e (a) shown in Fig. 1, written in an OCaml like syntax. The
program calls the function f with the argument x set to 109 and y set to 0, and adds a nondeterministic integer value z to the returned result. Here, the expression ∗ evaluates to a nondeterministic integer. We would like to prove that there exists an evaluation of the program that
results in the final value of 1. The property is expressed by the type {u :int | u = 1} ∃∃ . Therefore,
we would like derive the judgement ⊢ e (a) : {u :int | u = 1} ∃∃ . To do this, we first derive that f has
the following type σf∀∃ .
σf∀∃ ≜ (x :∀ int) → (y :∀ {u :int | u ≤ x }) → {u :int | u = 0} ∀∃The type says that the function, given any arguments x and y such that y ≤ x, always terminates andreturns 0. Note that this is a conditional termination property. As we shall show in more detail later inthe paper, such a derivation can be done by using the well-founded relation x > x ′ ∧ y = y ′ ∧ x ≥ yand the typing rule T-Total (cf. Fig. 5).
Then, by applying the subtyping rule T-Sub (cf. Fig. 5), we deriveΓ ⊢ f : σf∀∃ Γ ⊢ σf∀∃ <: σf∃∃
(T-Sub)Γ ⊢ f : σf∃∃where Γ is the type environment at the sub-derivation and σf∃∃ is the following type.
σf∃∃ ≜ (x :∀ int) → (y :∀ {u :int | u ≤ x }) → {u :int | u = 0} ∃∃Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:5

The type says that, given any arguments x and y such that y ≤ x, there is an evaluation of thefunction that results in the return value of 0. Indeed, the property holds for any function having
the type σf∀∃ . Using σf∃∃ , we derive the type {u :int | u = 0} ∃∃ for the function application f x y(cf. T-App∀ in Fig. 5). From this and the rule T-Rnd for typing non-deterministic choices, we
obtain the type {u :int | u = 1} ∃∃ for the whole program. The type system handles existential
non-deterministic choices by the Skolemization technique (cf. T-Skolem in Fig. 5). Roughly, thetechnique synthesizes a predicate that specifies a sufficient condition for the existential boundvariable to be used universally in the context, and checks the non-emptiness of the bound typeconditioned on the predicate and the current typing context. In the case of this example, we havethe existential variable binding z: ∃ {u :int | ⊤}, where ⊤ represents tautology. We synthesize theSkolemization predicate ϕ(z) ≜ z = 1, and check the non-emptiness of ∃z.⊤ ∧ ϕ(z) (which holds
trivially).
▲
The example above demonstrates the application of (conditional) termination verification, which
proves that for every inputs (satisfying a certain condition) the function terminates and reduces toa certain value, to prove the existence of an evaluation satisfying a certain property. Importantly,
the termination verification only requires a quite simple well-foundedness termination argument.
Note that verifying the example by more standard methods such as state space exploration andtesting can be much more costly, because such methods would go through one billion recursivefunction calls in order to discover an evaluation path reaching the program output.
Example 2.2. Next, we consider the program e (b) shown in Fig. 1. The program is a modification ofe (a) . The function f now has an additional control path so that, when x > y, it non-deterministicallychooses an integer value for w and calls f (x − 1) y if w > x or calls f x y otherwise. The program
still satisfies the property {u :int | u = 1} ∃∃ because, starting from x = 109 and y = 0, there exists
an evaluation path of the function that leads to the return value of 0. To verify the property, thetype system derives the type σf∃∃ for the modified f.
The derivation of σf∃∃ for f is similar to that of deriving the type σf∀∃ for the unmodified f
in Example 2.1, and it is done by the application of T-Total. It may use the same well-founded
relation x > x ′ ∧ y = y ′ ∧ x ≥ y, except that we now must handle the internal non-deterministic
choice in the function. The latter is done by T-Rnd and the Skolemization of the existential binding
w: ∃ {u :int | ⊤} with the predicate ϕ(x, w) ≜ w > x. Then, using the type σf∃∃ for f, we derive thetype {u :int | u = 1} ∃∃ for the whole program in the same way as in Example 2.1.
▲
In Example 2.2, the modified f has an internal non-determinism that needs to be properly handled
to derive the target property. The example demonstrates the ability of the type system to combine
reasoning via well-foundedness termination argument and existential non-determinism. As result,
we obtain a succinct proof of the existence of a non-trivial evaluation path.
Example 2.3. Next, we consider the program e (c) shown in Fig. 1, which is adopted from [Kuwahara et al. 2014]. It contains a higher-order recursive function app and a recursive function g. We
would like to verify that the program has the type {u :unit | ⊥} ∃∀ . Here, ⊥ represents contradiction.
Therefore, the type specifies that there exists a non-terminating evaluation, that is, it expresses
the (unconditional) non-termination property. Indeed, the program satisfies the property because
the evaluation of the function application g n with any negative integer n induces the following
infinite sequence of function calls: g n →∗ app g n →∗ g n →∗ . . . .
In order to derive the judgement ⊢ e (c) : {u :unit | ⊥} ∃∀ , we derive the following types σapp andσg for app and g, respectively.
σg
σapp

≜
≜

(x :∀ {u :int | u < 0}) → {u :unit | ⊥} ∀∀( f :∀ (x :∀ {u :int | u ≤ 0}) → {u :unit | ⊥} ∀∀ ) → {u :unit | ⊥} ∀∀Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:6

Hiroshi Unno, Yuki Satake, and Tachio Terauchi

e ::= x | n | v 1 op v 2 | ifz v then e 1 else e 2| rec( f ,H
x ,e) | v 1 v 2 | let x = e 1 in e 2 | let x = ∗ in e(values) v ::= x | n | rec( f ,H
x ,e) vH
(simple types) T ::= int | T1 → T2
(simple type environments) A ::= ∅ | A,x : T(expressions)Fig. 2. The syntax of L.
ϵn 1 op n 2 −→ JopK (n 1 ,n 2 )(E-Op)

let x = v in e −→ [v/x]e

ifz 0 then e 1 else e 2 −→ e 1(E-IfZ)e 1 −→ e 1′

ϵ

n,0

ϵ

n
H

(E-Let)nHϵifz n then e 1 else e 2 −→ e 2′(E-IfNZ) let x = e 1 in e 2 −→ let x = e 1 in e 2ϵe =⇒ e|Hx | = |Hv|
(E-App)ϵrec( f ,H
x ,e) vH −→ [rec( f ,H
x ,e)/f , vH/Hx ]en

let x = ∗ in e −→ [n/x]e(E-LetV)

n
f2

n
f1

e 1 −→ e 2

e 2 =⇒ e 3
n
f1 ·f
n2

(E-Rnd)(E-Refl)(E-Trans)

e 1 =⇒ e 3

Fig. 3. The operational semantics of L.

The derivation of the function types are done by the applications of the rule T-Partial (cf. Fig. 5).
Note that the types express safety properties. For instance, σg says that the function always diverges
given any negative integer argument. Equipped with these types for g and app, we derive thedesired type {u :unit | ⊥} ∃∀ for the program. This involves applying T-Rnd, and the Skolemizationof the existential binding b: ∃ {u :bool | ⊤} with the predicate ϕ(b) ≜ b = true.
▲
Example 2.3 demonstrates how our type system allows proofs of safety properties to be used
for proving non-termination. While such a combination has been observed previously [Chen et al.
2014; Kuwahara et al. 2015], to our knowledge, our work is the first to realize the combination in a
unified framework of a type system.
3

PRELIMINARIESIn this section, we introduce a simple higher-order strict functional language with non-determinism,
L, which is the target of our refinement type system. Fig. 2 shows the syntax of L. Here, x is ameta-variable ranging over variables, and n represents integer constants. xH represents a sequenceof variables. We write ϵ for the empty sequence and |H
x | for the length of xH. For simplicity, ourlanguage has only integers as a base type. The symbol op ranges over binary integer operators andis either the integer addition + or the integer multiplication ×. An expression rec( f ,H
x ,e) representsa (possibly recursive) function f with arguments xH and a body e. We here assume that |H
x | , 0. An
expression let x = ∗ in e generates a random integer n and evaluates e with x bound to n, andis the only source of (internal) non-determinism. The value rec( f ,H
x ,e) vH represents a function
closure where |H
v | < |H
x |. We write fvs(e) for the set of free variables that occur in e. We say that e isclosed if fvs(e) = ∅.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:7(qualified types) σ := ϕ  τ Q 1 Q 2(dependent refinement types) τ ::= x ϕ | (x :Q τ ) → σ(type environments) Γ ::= ∅ | Γ, x :Q τ
Fig. 4. The syntax of refinement types.

We assume that the expressions are simply-typed. Also, to simplify the proof of relative completeness (cf. Section 6.3), we assume that the sub-expressions e 1 and e 2 of ifz v then e 1 else e 2 ,rec( f ,H
x ,e 1 ), let x = e in e 1 , and let x = ∗ in e 1 only evaluate to integers. This does not lose
generality because an arbitrary program can be converted to such a form by, for example, thecontinuation-passing style (CPS) transformation.3nH

Fig. 3 shows the call-by-value operational semantics of the language. Here, e −→ e ′ means that e
is reduced to e ′ in one step with n
H = n if an integer n is randomly generated during the reduction
n
H

and n
H = ϵ if the reduction is deterministic. The multi-step reduction relation e =⇒ e ′ means thate is reduced to e ′ in zero or more number of steps and n
H is the sequence of integers randomly
generated during the reduction.
The evaluation rules are mostly self-explanatory. We comment on the less standard rules. In
E-Rnd, the expression let x = ∗ in e is reduced to [n/x] e for a randomly generated integer n. In
E-op, J+K and J×K respectively represent the integer addition and multiplication. The evaluation
relation satisfies the following property.
n
H

n
H

ϵ

ϵ

Proposition 3.1. If e =⇒ e 1 and e =⇒ e 2 , then e 1 =⇒ e 2 or e 2 =⇒ e 1 .
4

REFINEMENT TYPE SYSTEM

We present our refinement type system. For exposition, we present a simpler type system that issound but incomplete in this section, and then describe the relatively-complete full type system in
Section 5. The simpler system lacks the intricacy that are needed for relative completeness, such as
Gödel encoding of function-type values and intersection and union types. However, it is suitedfor conveying the essence of how universal and existential reasoning can be integrated in a typesystem.
Fig. 4 shows the syntax of refinement types. Here, Q is either ∀ or ∃. A refinement base type
x ϕ , equipped with a refinement predicate ϕ, represents the type of integers x that satisfy
ϕ. Here, ϕ is an integer arithmetic formula.4 We write ⊤ and ⊥ respectively for tautology andcontradiction. We write |= ϕ when ϕ is valid. We often abbreviate x ϕ as int when ϕ is valid(e.g., {x | ⊤} = int). The type (x :∀ τ ) → σ is a dependent function type, consisting of the argument
type τ and the return type σ . It represents a type of functions that, given any argument x of thetype τ , behave according to the type σ . By contrast, the dependent function type (x : ∃ τ ) → σ withthe existentially bound argument is the type of functions that, given some argument x of the type τ ,behave according to σ . We sometimes abbreviate (x :∀ τ ) → σ as τ → σ if x does not occur in σ . In
(x :∀ τ ) → σ and (x : ∃ τ ) → σ , the variable x is interpreted as integers in the refinement predicatesin σ , even when the argument type τ is a function type. In the latter, the passed functions are
assumed to be encoded as integers (cf. Section 5.1). We let σ range over types qualified by the ∀-∃3 An analogous assumption is used in the previous work on higher-order program verification [Kobayashi 2009; Terauchi

2010; Unno et al. 2013].
4 For relative completeness, we require that the background theory of refinement predicates is second-order Peano arithmetic,

but any subset (e.g., quantifier-free first-order theory of linear arithmetic) is sufficient for soundness.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:8

Hiroshi Unno, Yuki Satake, and Tachio Terauchi

modes. A qualified type is also equipped with a logical formula ϕ, which we call a guard. We often
abbreviate ϕ  τ Q 1 Q 2 as τ Q 1 Q 2 when ϕ is ⊤. Later in Section 5, we extend σ to range over guarded
intersection and union types. For this section, it is safe to assume that guard formulas are always ⊤,except for the return type of the function at the typing rule T-Total where the formula is used
to express the well-foundedness condition (cf. Section 4.1). We often write ty(τ ) (resp. ty(σ )) for
the simple type obtained from τ (resp. σ ) by removing refinement predicates, qualifiers, guards,
intersections, and unions.
We write fvs(τ ) and fvs(σ ) for the set of free variables of τ and σ respectively, which are definedinductively as shown below.
fvs( x ϕ ) ≜ fvs(ϕ) \ {x }fvs((x :Q τ ) → σ ) ≜ fvs(τ ) ∪ (fvs(σ ) \ {x })fvs(ϕ  τ Q 1 Q 2 ) ≜ fvs(ϕ) ∪ fvs(τ )Note that the scope of x in x ϕ is ϕ, and the scope of x in (x :Q τ ) → σ is σ (but not τ ).
We define the order ⊑ among the qualifiers as follows: Q∃ ⊑ Q∀ and ∀Q ⊑ ∃Q for any Q. Notethat ({∀∀,∀∃, ∃∀, ∃∃}, ⊑) is a lattice. The order is used to formalize the subtyping relationship(cf. Section 4.1). The intuition behind the order can be understood as follows: total correctness
types can be used as partial correctness types and demonic types can be used as angelic types. Notethat ∀∃ is the strongest element, and we often abbreviate τ ∀∃ as τ .
We remark that a value can always be assigned the qualifier ∀∃ because it is pure, i.e., it nevercauses non-termination or non-determinism. Note also that, because our target language L is strict,an argument passed to a function is always a value. Therefore, they too can be safely assumed to bequalified by ∀∃. This is why the function argument types and the types bound in type environments
do not carry qualifiers (i.e., they are of the form x :Q τ rather than x :Q σ ). Also, a partial application
rec( f ,H
x ,e) vH (i.e., where |H
v | < |Hx |) is a value and is pure. Then, because function bodies only
evaluate to integers, each function can be assigned a type of the form (x 1 :Q 1 τ1 ) → (· · · → ((xm :Qmτm ) → σ ) ∀∃ · · · ) ∀∃ where σ is a (qualified and guarded) refinement base type. We often abbreviateH
H = Q 1 , · · · ,Qm . In what
the type as (Hx :Q Hτ ) → σ , where xH = x 1 , · · · ,xm , Hτ = τ1 , · · · ,τm , and Q

Q
Q
1
2
follows, we assume that τ in ϕ  τ
is of the form x ϕ .
As usual, we assume that the variables bound in a type environment are distinct. We write Γ,ϕfor Γ,ν :∀ ν ϕ where ν is fresh. We define dom(Γ) = {x | x :Q τ ∈ Γ}, and write Γ(x ) = τ if
x :Q τ ∈ Γ. We also use ∆ as a meta-variable ranging over type environments that do not contain anexistential binding x : ∃ τ (and use Γ to range over type environments that contain or do not containexistential bindings).
4.1

Typing Rules

Fig. 5 shows the typing and subtyping rules. A typing judgement Γ ⊢ e : σ means that an expression
e has a type σ under a type environment Γ. A subtyping judgement Γ ⊢ σ1 <: σ2 means that σ1 is asubtype of σ2 under Γ.
In Fig. 6, the auxiliary functions Γ ⊢ ϕ , ⌊⊢ x : τ ⌋ and ⌊⊢ x : σ ⌋ return an arithmetic formula.
Intuitively, Γ ⊢ ϕ holds if ϕ is valid for any valuation of the variables conforming to Γ whereas⌊⊢ x : τ ⌋ (resp. ⌊⊢ x : σ ⌋) represents the condition for x to satisfy the property denoted by τ (resp.
σ ). Roughly, these functions provide Gödel encodings of the denotational semantics of the types(cf. Section 5.2). The formal definition of the notations TeU, x ⇓, ev(x,y), valT (x ), expT (x ), andapp(x,y) are deferred to Section 5.1 (TeU is used in the definition of the auxiliary function ⌊v⌋ in
Fig. 6). Roughly, TeU is the encoding function for expressions, x ⇓ is the predicate which states thatthe expression encoded by x terminates, ev(x,y) says that the expression encoded by x evaluates
to the value encoded by y, valT (x ) (resp. expT (x )) represents that x encodes an L-definable value
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...
∆,x :Q 1 int ⊢ e : τ Q 1 Q 2

τf = (Hx :Q Hτ ) → τQ∀
H∆,H
x :Q Hτ , f :∀ τf ⊢ e : τ Q ∀H(T-Partial)∆ ⊢ rec( f ,H
x ,e) : τf

τf′ = (Hy :Q Hτ ′ ) → ϕ  (τ ′ ) Q ∃Hτ = (Hx :Q Hτ ) → τ Q ∃ =α (Hy :Q Hτ ′ ) → (τ ′ ) Q ∃fxH ∩ yH = ∅ fvs(ϕ) ⊆ ( xH,Hy ∪ dom(∆))
HQ|= ∆ ⊢ WF (λH
xyH.ϕ) ∆,H
x: H
τ , f :∀ τf′ ⊢ e : τ Q ∃HH∆ ⊢ rec( f ,H
x ,e) : τf
∆ ⊢ v 1 : (x :∀ τ ) → σ(T-App∀)(T-App∃)ty(∆(x )) = int(T-VInt)∆ ⊢ n : {x | x = n}
∆ ⊢ v 1 : int∆ ⊢ v 2 : int∆ ⊢ v 1 op v 2 : x x = (v 1 op v 2 )∆ ⊢ v : int∆,v = 0 ⊢ e 1 : σ∆,v , 0 ⊢ e 2 : σ∆ ⊢ ifz v then e 1 else e 2 : σ
Q Q∆,x :∀ τ∆ ⊢ e 1 : τ1 1 2
Q1Q2
x < fvs(τ2 )1 ⊢ e 2 : τ2

Q Q
∆ ⊢ let x = e 1 in e 2 : τ2 1 2∆,x : ∃ τ , Γ ⊢ e : σ(T-Skolem)∆ ⊢ e : σ′

∆ ⊢ σ ′ <: σ∆ ⊢ τ1 <: τ2(T-Sub)(T-VFun)(S-Guard)

Q 1Q 1′ ⊑ Q 2Q 2′
Q Q′(S-Qual)∆ ⊢ τ1 1 1 <: τ2 2 2|= ∆ ⊢ ϕ 1 ⇒ ϕ 2∆ ⊢ ν ϕ 1 <: ν ϕ 2∆ ⊢ τ2 <: τ1(S-Int)∆,x :∀ τ2 ⊢ σ1 <: σ2∆ ⊢ (x :∀ τ1 ) → σ1 <: (x :∀ τ2 ) → σ2ty(∆(x )) , int∆ ⊢ x : ∆(x )(T-Rnd)Q Q′∆
h ⊢ v1i|= ∆,x :∀ τ , Γ ⊢ x = ⌊v 2 ⌋∆ ⊢ x : {ν | ν = x }∆ ⊢ let x = ∗ in e : τ Q 1 Q 2hi|= ∆,x : ∃ τ ⊢ ϕ∆,x :∀ τ ,ϕ, Γ ⊢ e : σ∆ ⊢ ϕ 1  σ1 <: ϕ 2  σ2

: (x : ∃ τ ) → σ∆, Γ ⊢ v 1 v 2 : [⌊v 2 ⌋ /x]σx < fvs(τ )∆⊢e :σ(T-Total) |= ∆ ⊢ ϕ 2 ⇒ ϕ 1 ∆,ϕ 2 ⊢ σ1 <: σ2∆ ⊢ v2 : τ∆ ⊢ v 1 v 2 : [⌊v 2 ⌋ /x]σ12:9

(S-Fun∀∀)∆ ⊢ τ <: τ1∆ ⊢ τ <: τ2∆,x : ∃ τ ⊢ σ1 <: σ2∆ ⊢ (x :∀ τ1 ) → σ1 <: (x : ∃ τ2 ) → σ2

(S-Fun∀∃)(T-Int)∆ ⊢ τ1 <: τ2∆,x :∀ τ1 ⊢ σ1 <: σ2(T-Op) ∆ ⊢ (x : ∃ τ1 ) → σ1 <: (x : ∃ τ2 ) → σ2

(S-Fun∃∃)∆ ′ = ∆,x 1 :∀ τ1 ,x 2 :∀ τ2 ,y1 :∀ τ1 ,y2 :∀ τ2|= ∆ ′ ⊢ x 1 = x 2 ∧ y1 = y2 ⇒ x 1 = y1∆,x :∀ τ1 ,y :∀ τ2 ,x = y ⊢ σ1 <: σ2(T-If)
σϕ,Q = TH → ν ϕ QQ∆,x :∀ τ1 ,y : ∃ τ2 ,x , y ⊢ σ1 <: σ⊥, ∃∆,y :∀ τ2 ,x : ∃ τ1 ,x , y ⊢ σ⊤,∀ <: σ2(T-Let)∆ ⊢ (x : ∃ τ1 ) → σ1 <: (y :∀ τ2 ) → σ2
(S-Fun∃∀)Fig. 5. The derivation rules of Γ ⊢ e : σ and Γ ⊢ σ1 <: σ2 (except those for intersections and unions).

(resp. expression) of the simple type T , and app(x,y) returns the integer that encodes the applicationof the function expression encoded by x to the value encoded by y. Note that the encoding function⌊v⌋ for values does nothing if v is an integer value.
We describe the typing rules. The rule T-Partial (resp. T-Total) assigns a partial (resp. total)
correctness type to a recursive function f . T-Partial is the standard rule for typing recursive
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:10Hiroshi Unno, Yuki Satake, and Tachio Terauchihi∅⊢ϕ =ϕ⌊⊢ x : (τ ,∀∃)⌋ = x⇓ ∧ ⊢ x : τ ∀∀
h
i 



Γ,x :∀ τ ⊢ ϕ = Γ ⊢ ∀x .(⌊⊢ x : τ ⌋ ⇒ ϕ)⌊⊢ x : (τ ,∀∀)⌋ = ∀y.(ev(x,y) ⇒ ⊢ y : τ )
h
i 



⌊⊢ x : (τ , ∃∃)⌋ = ∃y.(ev(x,y) ∧ ⊢ y : τ )Γ,x : ∃ τ ⊢ ϕ = Γ ⊢ ∃x .(⌊⊢ x : τ ⌋ ∧ ϕ)
h
i



⌊⊢ x : (τ , ∃∀)⌋ = ¬(x⇓) ∨ ⊢ x : τ ∃∃⊢ hx : ν  ϕ = [x/ν ]ϕihiQ⊢ x : ν : τ → σ = valty(τ →σ ) (x ) ∧ ν :Q τ ⊢ ∀r .(r = app(x,ν ) ⇒ ⌊⊢ r : σ ⌋)hi
⊢ x : ϕ  τ Q 1 Q 2 = expty(τ ) (x ) ∧ (ϕ ⇒ ⌊⊢ x : (τ ,Q 1Q 2 )⌋)v⌊v⌋ =  TvU
(if v is an integer value)(otherwise)

Fig. 6. The auxiliary functions for the typing rules.

functions, and as expected, it ensures partial correctness. By contrast, T-Total requires that thepair of the arguments xH passed to a call to f and those yH passed to its recursive call is included in awell-founded relation in order to guarantee termination. We call a predicate p = λH
x .ϕ well-foundedt 1 ,Ht2 , . . .
and write WF (p), if the arity of p is 2 × n for some n and there is no infinite sequence H
such that |H
ti | = n and p(Hti ,Hti+1 ) holds for all i ≥ 1. Also, we write τ1 =α τ2 if τ1 and τ2 are alphaequivalent. Let us consider the following expression as an example:
e sum ≜ rec(sum,x, ifz x then 0 else let r = sum (x − 1) in x + r )We can derive the judgement ⊢ e sum : {x | x ≥ 0} → y y ≥ x ∀∃ because we can derive Γsum ⊢
let r = sum (x − 1) in x + r : y y ≥ x ∀∃ forΓsum ≜ x :∀ {x | x ≥ 0} , sum:∀ x ′ x ′ ≥ 0 → x > x ′ ≥ 0  y ′ y ′ ≥ x ′ ∀∃ ,x , 0
and |= WF (λ(x,x ′ ).x > x ′ ≥ 0). The rule is analogous to those proposed previously for asserting
termination in dependent-refinement type systems [Vazou et al. 2014; Xi 2001].
In the rule T-Let, the qualifiers of the types of the consecutively executed expressions e 1 ande 2 must coincide, and the variable x which stores the value of e 1 is always bound universally. By
contrast, in the rule T-Rnd, the variable x which stores the randomly generated integer is allowed
to be bound existentially, assuming that the qualifier of the type of the body e is of the form ∃Q.
For example, the derivation of x :∀ int ⊢ let y = ∗ in x + y : {ν | ν = 0} ∃∃ has the following root.
x :∀ int,y : ∃ int ⊢ x + y : {ν | ν = 0} ∃∃x :∀ int ⊢ let y = ∗ in x + y : {ν | ν = 0} ∃∃As we shall show below, the antecedent x :∀ int,x : ∃ int ⊢ x + y : {ν | ν = 0} ∃∃ can be derived byapplying the T-Skolem rule.
T-App∀ and T-App∃ are rules for function applications v 1 v 2 . T-App∀ is the standard rule forfunction applications in dependent refinement type systems (see, e.g., [Rondon et al. 2008; Terauchi
2010; Unno and Kobayashi 2009]). Recall that the notation ⌊v⌋ denotes the encoding of the value v.
By contrast, T-App∃ is a non-standard rule introduced for handling function types (x : ∃ τ ) → σ
with the existential binding. For the sake of exposition,
assume here thathi Γ only contains existential
bindings. Then, roughly, the antecedent |= ∆,x :∀ τ , Γ ⊢ x = ⌊v 2 ⌋ says that for any valuation
conforming to the type environment ∆,x :∀ τ , we can select some valuation of the existentiallybound variables in Γ such that ⌊v 2 ⌋ becomes equivalent to the valuation of x. That is, it checks
if every value of τ can be obtained by selecting the values of existentially bound variables inΓ. If the check succeeds, the rule concludes that v 1 v 2 has the type [⌊v 2 ⌋ /x]σ . For example, letProceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:11

e ≜ let y = ∗ in f y and ∆ ≜ f :∀ (x : ∃ int) → {z | ⊥} ∃∀ . The type of f says that there is an
integer n such that f n may diverge. By T-Rnd and T-App∃, we havehi∆ ⊢ f : (x : ∃ int) → {z | ⊥} ∃∀ |= ∆,x :∀ int,y : ∃ int ⊢ x = y∆,y : ∃ int ⊢ f y : {z | ⊥} ∃∀∆ ⊢ e : {z | ⊥} ∃∀hiBecause |= ∆,x :∀ int,y : ∃ int ⊢ x = y holds, we can conclude that e also has the type {z | ⊥} ∃∀ ,and therefore may diverge. Note that if the type of f were (x : ∃ int) → {z | ⊥} ∀∀ instead, T-Rnd
would not allow e to have the incorrect type {z | ⊥} ∀∀ saying that e always diverges.
The rule T-Skolem skolemizes an existentially bound variable x : ∃ τ in the type environment,
which may be introduced by the rules T-Partial, T-Total, and T-Rnd. As remarked in Section 2, therule introduces a Skolemization predicate ϕ that specifies a sufficient condition for the existentiallybound variable to be used universally in the context (which is expressed by the antecedent ∆,x :∀τ ,ϕ, Γ ⊢ e : σ ), and checks the non-emptiness of the boundh type conditionedon the predicate andi∃the current typing context (expressed by the antecedent |= ∆,x : τ ⊢ ϕ ). For example, x :∀ int,y : ∃inth ⊢ x + y : {z | z = 0} ∃∃ fromthe above discussion is derivable by using T-Skolem becausei|= x :∀ int,y : ∃ int ⊢ y = −x and x :∀ int,y :∀ int,y = −x ⊢ x + y : {z | z = 0} ∃∃ are derivable.
Note that we need to apply the Skolemization rule eagerly before we apply the other rules because
it requires the type environment ∆ to contain no existential binding.5
The rule T-Sub weakens a type assigned to an expression into a subtype. The rule S-Guard can beused to eliminate the guard of types introduced by T-Total. The rule S-Qual changes the qualifier oftypes according to the order ⊑. The rules S-Int and S-Fun∀∀ are standard and adopted from the previous work on dependent refinement types for partial correctness [Rondon et al. 2008; Terauchi 2010;
Unno and Kobayashi 2009]. The subtyping rules S-Fun∀∃, S-Fun∃∃, and S-Fun∃∀ are for deriving
subtyping judgements related to function types that handle function types (x : ∃ τ ) → σ with the existential binding. In the rule S-Fun∃∀, the antecedent |= ∆ ′ ⊢ x 1 = x 2 ∧ y1 = y2 ⇒ x 1 = y1 checks
that the intersection of the sets of values represented by τ1 and τ2 is empty or singleton, and σ⊥, ∃(resp. σ⊤,∀ ) denotes the empty set (resp. the set of all the expressions whose simple type is ty(σ2 )).
For example, we can derive ⊢ (x : ∃ {x | x ≥ 0}) → y y = x ∀∃ <: (x : ∃ int) → y y ≥ 0 ∀∃ by
S-Fun∃∃, ⊢ (x :∀ {x | x ≥ 0}) → y y = x ∀∃ <: (x : ∃ {x | x ≤ 1}) → y y = 1 ∀∃ by S-Fun∀∃,and ⊢ (x : ∃ {x | x = 1}) → y y = 0 ∀∀ <: (x :∀ {x | x = 1 ∨ x = 2}) → y x = 1 ⇒ y = 0 ∀∀ by
S-Fun∃∀. These rules are useful for adjusting the types of function arguments and free variables
that are provided by external environments.
4.2

ExamplesWe show the type derivations of Examples 2.1, 2.2 and 2.3. The examples are desugared as follows.
f ) ine (a) ≜ let f = rec(f, (x,y),e (a)let x = 10∗∗9 in let y = 0 in let z = ∗ in let w = f x in let w ′ = w y in w ′ + zf ) ine (b ) ≜ let f = rec(f, (x,y),e (b)
let x = 10∗∗9 in let y = 0 in let z = ∗ in let w = f x in let w ′ = w y in w ′ + ze (c ) ≜ let app = rec(app, f x,e app ) in let g = rec(g,x,e g ) in
let b = ∗ in ifz b then g (−1) else 0
5 Though we could design the type system based on a lazy Skolemization approach, the Skolemization rule must be anyway

applied before we type-check expressions consisting of multiple sub-expressions so that we can synchronize the valuationof existentially bound variables across the sub-expressions.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:12Hiroshi Unno, Yuki Satake, and Tachio Terauchi

f , ef , e
where e (a)and e g are the following expressions.
(b ) appf ≜ let v = x ≤ y in ifz v then 0 else (let v = x − 1 in let f ′ = f v in f ′ y)e (a)f ≜ let v = x ≤ y ine (b)
ifz v then 0
else let w = ∗ in let v = w > x in
ifz v then let v = x − 1 in let f′ = f v in f′ y else let f′ = f x in f′ ye app ≜ let v = x > 0 in ifz v then app f (x − 1) else f x
e g ≜ let v = x = 0 in ifz v then 0 else app g x
Here, Boolean values are encoded as integers. That is, for integers m, n and  ∈ {<, ≤}, m JK n isdefined to be the binary operation that returns 0 if m  n and returns 1 otherwise.

Γ2 ⊢ f : σf∀∃

(T-VFun)· · · ∀∃ ⊑ ∃∃(S-Qual)Γ2 ⊢ σf∀∃ <: σf∃∃
(T-Sub)Γ2 ⊢ f : σf∃∃
..
.

..
.
(T-Sub)∃∃ ⊢ w + z : τ ∃∃
Γ2 ,w : τu=0e (a)(T-Let)′ : τ ∃∃
Γ1 ,z :∀ int,z = 1 ⊢ e (a)e (a)(T-Skolem)′ : τ ∃∃
Γ1 ,z : ∃ int ⊢ e (a)
e (a)

..
.

′ : τ ∃∃
Γ1 ,z : ∃ int ⊢ e (a)
e (a)

f :
x : int,y : int, f : τf ⊢ e (a){u | u = 0} ∀∃|= ⊢ WF (p)f ) :σ⊢ rec(f, (x,y),e (a)f∀∃′ : τ ∃∃
Γ1 ⊢ let z = ∗ in e (a)e (a)(T-Rnd)..
.

(T-Let)(T-Total)⊢ e (a) : τe∃∃(a)

(T-Let)Fig. 7. Type derivation of Example 2.1

Derivation of Example 2.1. Fig. 7 shows the derivation for Example 2.1. We focus only on the
key parts of the derivation. Here, we would like to type e (a) as τe∃∃
, where τe (a) = {u | u = 1}. As(a)shown in the lower part of the figure, we first deconstruct the let bindings f, x, and y by applying
the rule T-Let to the bodies three times.
Then, as shown in the left branch of the figure, we apply T-Total with the well-founded relationf ) as σp(x,y,x ′,y ′ ) ≜ x > x ′ ∧ y = y ′ ∧ x ≥ y to type the term rec(f, (x,y),e (a)f∀∃ where τf =(x ′ :∀ int) → (y ′ :∀ int) → p(x,y,x ′,y ′ )  {u | u = 0} ∀∃ (cf. Example 2.1 for the definition ofσf∀∃ ). Hence, f is also given the type σf∀∃ . In the right branch, we apply T-Rnd to the judgement′ : τ ∃∃ , whereΓ1 ⊢ let z = ∗ in e (a)e (a)′≜ let w = f x in let w ′ = w y in w ′ + ze (a)Γ1 ≜ f : σf∀∃ ,x : {u | u = 10∗∗9} ,y : {u | u = 0}

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:13

We now would like to deconstruct let binding w, however, the environment Γ1 ,z : ∃ int includes
an existential binding of z, so that we first apply T-Skolem and eliminate the existential binding
from the environment, as shown in the upper part of the figure.
Let Γ2 be an environment Γ1 ,z : ∃ int,z = 1. We apply subtyping rules to derive Γ2 ⊢ f : σf∃∃ and′ : τ ∃∃ .
derive the judgement Γ2 ⊢ e (a)
e (a)
..
.
′

f :
x :∀ int,y :∀ {u | u ≤ x } , f:∀ τf ,w :∀ int,w > x ⊢ e (b{u | u = 0} ∃∃)′f :x :∀ int,y :∀ {u | u ≤ x } , f:∀ τf ,w : ∃ int ⊢ e (b{u | u = 0} ∃∃
)

···

′

f :
x :∀ int,y :∀ {u | u ≤ x } , f:∀ τf ⊢ let w = ∗ in e (b{u | u = 0} ∃∃)(T-Rnd)(T-Let)(T-If)

f :x :∀ int,y :∀ {u | u ≤ x } , f:∀ τf ⊢ e (b{u | u = 0} ∃∃)f ) :σ⊢ rec(f, (x,y),e (bf∃∃)(T-Skolem)(T-Total)Fig. 8. Type derivation of Example 2.2

Derivation of Example 2.2. The derivation of e (b ) is similar to that of e (a) except for the derivationf ) :σof ⊢ rec(f, (x,y),e (bf∃∃ (cf. Example 2.1 for the definition of σf∃∃ ). Fig. 8 shows the key parts)f ) :σof the derivation. We first apply T-Total to the judgement ⊢ rec(f, (x,y),e (bf∃∃ and obtain)f :the judgement x :∀ int,y :∀ {u | u ≤ x } , f:∀ τf ⊢ e (b{u | u = 0} ∃∃ where τf ≜ (x ′ :∀ int) → (y ′ :∀)int) → (x > x ′ ∧ y = y ′ ∧ x ≥ y)  {u | u = 0} ∃∃ .
f′ is the following expression.
This is followed by the applications of T-Let and T-If. Here, e (b)
let v = w > x in ifz v then let v = x − 1 in let f′ = f v in f′ yelse let f′ = f x in f′ y
In the then branch, we apply T-Rnd to deconstruct the let binding of w and apply T-Skolem withrespect to w. The rest of the derivation is analogous to Example 2.1.
..
.
Γ3 ,b :∀ int,b = 0 ⊢ g (−1) : {u | ⊥} ∃∀(T-Int)
Γ3 ,b :∀ int,b = 0,b , 0 ⊢ 0 : {u | u = 0} ∀∃(T-Sub)
Γ3 ,b :∀ int,b = 0,b , 0 ⊢ 0 : {u | ⊥} ∃∀(T-If)
Γ3 ,b :∀ int,b = 0 ⊢ ifz b then g (−1) else 0 : {u | ⊥} ∃∀(T-Skolem)
Γ3 ,b : ∃ int ⊢ ifz b then g (−1) else 0 : {u | ⊥} ∃∀(T-Rnd)Γ3 ⊢ let b = ∗ in ifz b then g (−1) else 0 : {u | ⊥} ∃∀..
.
Fig. 9. Type derivation of Example 2.3

Derivation of Example 2.3. Fig. 9 shows the key parts of the derivation for Example 2.3. Here,Γ3 ≜ app :∀ σapp , g :∀ σg . The derivation of the types σapp for app and σg for g are standard andomitted (cf. e.g., [Rondon et al. 2008; Terauchi 2010; Unno and Kobayashi 2009]).
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:14Hiroshi Unno, Yuki Satake, and Tachio Terauchi

To derive Γ3 ⊢ let b = ∗ in ifz b then g (−1) else 0 : {u | ⊥} ∃∀ , we first deconstruct the letbinding of b and apply T-Skolem with ϕ ≜ b = 0. Next, we apply T-If. In the left branch of thederivation, we obtain the judgement Γ3 ,b :∀ int,b = 0 ⊢ g (−1) : {u | ⊥} ∃∀ , which is justified by
the types of g and app. In the right branch, we obtain the judgement Γ3 ,b :∀ int,b = 0,b , 0 ⊢ 0 :{u | ⊥} ∃∀ . Note that T-Sub can be applied because b = 0 ∧ b , 0 |= ⊥.
5

RELATIVE COMPLETENESS EXTENSION

We present the relative completeness extension to the refinement type system. The key componentsof the extension are Gödel encoding of function-type values (that was treated only informally in
Section 4) and guarded intersection and union types.
We extend the syntax of refinement types (cf. Fig. 4) by extending the qualified types σ to guarded
intersection and union types:(guarded intersection and union types) σ :=Q i j Q i′ j
Wℓ Vmi 
i=1
j=1 ϕ i j  τi jWℓWℓ VmiHere, we assume that ℓ,m 1 , . . . ,m ℓ ≥ 1. We often omit i=1
if ℓ = 1, and omit i=1
j=1 ifℓ = m ℓ = 1. Note that the qualified types in the non-extended system are of the latter restricted form.
Q i j Q i′ j
Wℓ VmiH
Note also that we can safely assume that σ is always of the form (Hx :Q Hτ ) → i=1
(ϕ
τ
)
i
j
ij
j=1
Q i j Q i′ j
Wℓ Vmior i=1 j=1 (ϕi j  τi j
) such that ty(τi j ) = int.
The union types are used to express the complement of intersection types, as shown later in thissection. On the other hand, the guarded intersection types allow the type system to collectively
express different behaviors of functions and expressions depending on their arguments and freevariables, and are essential for the proof of relative completeness (cf. Section 6.3) where such types
are used to build the strongest type ST(e; pH) of an expression e with respect to given postconditions
pH, whose formal definition is deferred to Section 5.1.
The notion of free variables are extended to intersection and union types as shown below.
mi
mi
ℓ ^
ℓ [
_
[
fvs *.
σi j +/ ≜fvs(σi j ), i=1 j=1 - i=1 j=1

Example 5.1. We can use a guarded intersection type to summarize (conditional) termination/nontermination behavior of a function. The type
(x : int) → (x > 0  int∀∃ ) ∧ (x < 0  y ⊥ ∀∀ ) ∧ (x = 0  int ∃∃ ) ∧ (x = 0  y ⊥ ∃∀ )says functions of this type always terminate if the argument x is positive, always diverge if x is
negative, and otherwise, non-deterministically terminate or diverge.
▲
Next, we formally define the complement types. As discussed in Section 1, we define the complements of the qualifiers as follows: ∀ = ∃ and ∃ = ∀.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:15

Definition 5.2 (Complement Types). The complement type ¬σ of σ is defined by:′′¬ τ QQ ≜ (¬τ ) (Q )(Q )¬ (ϕ  σ ) ≜ (¬ϕ  {x | ⊥} ∀∃ ) ∧ ¬σ
mi
mi
ℓ ^
ℓ _
_
^
¬ *.
σi j +/ ≜ DNF *.
¬σi j +/
, i=1 j=1
- 
, i=1 j=1

¬ x ϕ ≜ x ¬ϕ¬((x :Q τ ) → σ ) ≜ (x :Q τ ) → ¬σ
where DNF transforms a given intersection and union type to the disjunctive normal form.
Note here that ¬ (ϕ  σ ) can be interpreted as ϕ ∧ ¬σ because  means a (type-level) logicalimplication. In the definition, the left-hand side ϕ of the intersection is represented as the guarded
type ¬ϕ  {x | ⊥} ∀∃ . The complement ¬σ of a given type σ can be used to witness that a given
expression violates the specification represented by σ . Thus, we believe complement types pave a
way to develop, in a future work, a verification method that simultaneously attempts a proof anda refutation in a cooperative and unified manner. In Section 6.1, we show the correctness of thedefinition, thereby showing that the types are closed under complement.
5.1

Encoding

Relative completeness for higher-order programs requires a means of precisely expressing propertiesof function values (i.e., partial applications). Following the previous work [Damm and Josko 1983;
German et al. 1983, 1989; Goerdt 1985; Honda et al. 2006; Olderog 1984; Reus and Streicher 2011;
Unno et al. 2013], we accomplish this by Gödel encoding. We remark that, as shown in [Unno et al.
2013], it is often possible to avoid explicit encoding in practice and that the encoding is unnecessary
for soundness.6
We use a meta-variable w to range over closed values. A value substitution θ maps each variablex ∈ dom(θ ) to a closed value of the same simple type as x. We write θ (e) for e but with eachvariable x replaced by θ (x ). For an expression e and a closed value w, let EvaluatesTo(e,w ) be the
n
H

n
H

condition ∃Hn . e =⇒ w, and AlwaysTerminates(e) be the condition ∀π ∈ Zω .∃Hn ∈ Pref (π ).∃w. e =⇒w where Zω denotes the set of infinite sequences of integers and Pref (π ) denotes the set offinite prefixes of the infinite sequence π . Note that EvaluatesTo(e,w ) means that there exists a(terminating) evaluation of e that reduces to the closed value w, and AlwaysTerminates(e) meansthat the evaluation of e always terminates. We define e ∼ e ′ by induction on the simple type of e
and e ′ as follows: for any closed value w and substitution θ with dom(θ ) = fvs(e) ∪ fvs(e ′ ),• AlwaysTerminates(θ (e)) ⇔ AlwaysTerminates(θ (e ′ )),• if ⊢s θ (e) : int, EvaluatesTo(θ (e),w ) ⇔ EvaluatesTo(θ (e ′ ),w ),• if ⊢s θ (e) : T1 → T2 and EvaluatesTo(θ (e),w ), then there is w ′ such that EvaluatesTo(θ (e ′ ),w ′ )and w w ′′ ∼ w ′w ′′ for any closed value w ′′ with ⊢s w ′′ : T1 , and• if ⊢s θ (e) : T1 → T2 and EvaluatesTo(θ (e ′ ),w ), then there is w ′ such that EvaluatesTo(θ (e),w ′ )and w w ′′ ∼ w ′w ′′ for any closed value w ′′ with ⊢s w ′′ : T1 .
Here, ⊢s is the typing relation of the simple type system.
We are now ready to describe the encoding. We write TeU for an integer term (in the theory of
second-order integer arithmetic) that encodes the expression e where fvs(TeU) = fvs(e). We assume
6 Technically, without encoding, the meaning of soundness would be different for open programs with free function-type

variables as the variables would also range over non-definable functions.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:16Hiroshi Unno, Yuki Satake, and Tachio Terauchi

that if e ∼ e ′ then |= TeU = Te ′U, which indicates that the quotient set of expressions induced by
the encoding is no more precise than the one induced by the equivalence relation ∼. We write Tθ U
(resp. ⌊θ ⌋) for the integer substitution that maps each (possibly non-integer) variable x ∈ dom(θ )to the integer Tθ (x )U (resp. ⌊θ (x )⌋). (Recall the definition of ⌊v⌋ in Fig. 6.)
We assume that there exist a binary function app : Z × Z → Z, a binary relation ev ⊆ Z × Z, andunary relations ⇓, valT , expT ⊆ Z for each type T such that, for any expression e, a value v, and avalue substitution θ where fvs(e) ∪ fvs(v) ⊆ dom(θ ), the following conditions hold:• |= Tθ U(TeU) = Tθ (e)U• |= app(Tθ U(TeU), ⌊θ ⌋ (⌊v⌋)) = Tlet x = θ (e) in x (θ (v))U• |= ev(Tθ U(TeU), ⌊θ ⌋ (⌊v⌋)) if and only if ∃w.(EvaluatesTo(θ (e),w ) ∧ w ∼ θ (v))• |= Tθ U(TeU)⇓ if and only if AlwaysTerminates(θ (e))• |= valT (⌊θ ⌋ (⌊v⌋)) if and only if ⊢s θ (v) : T• |= expT (Tθ U(TeU)) if and only if ⊢s θ (e) : T

Note that it follows from the conditions that |= TxU = x, |= ⌊θ ⌋ (⌊v⌋) = ⌊θ (v)⌋, and if |= Te 1 U =Te 2 U then e 1 ∼ e 2 . We write TeU⇑, meaning that e always diverges, as an abbreviation of the formula¬∃x .ev(TeU,x ). Accordingly, we define AlwaysDiverges(e) by ¬∃x .EvaluatesTo(e,x ). We also write
app(x,y1 , . . . ,ym ) as an abbreviation of app(. . . (app(app(x,y1 ),y2 ), . . . ),ym ).
We now formalize the strongest type ST(e; pH) of an expression e with respect to given postconditions pH, using the Gödel encoding and the guarded intersection types. Let the simple type of e
be TH → int. Note that, in our language, e is a function value if |TH| , 0, and an integer expression
otherwise. Thus, ST(e; p1 , . . . ,pm ) is defined as follows:
app(TeU,Hx )⇓  ν ev(app(TeU,Hx ),ν ) ∀∃ , 








∀∀


app(TeU,H
x
)⇑

⊥}
,
{ν
|








∃∀


^

¬app(TeU,Hx)⇓∧¬app(TeU,H
x
)⇑

⊥}
,
{ν
|


∀H



∃∃
(H
x: T) →
∃ν .(ev(app(TeU,Hx ),ν ) ∧ p1 (Hx ,ν ))  ν p1 (Hx ,ν )
,










..






.







∃∃


∃ν
.(ev(app(TeU,H
x
),ν
)
∧
p
(H
x
,ν
))

ν
p
(H
x
,ν
)
m
m



Here, ν ev(app(TeU,Hx ),ν ) ∀∃ represents the strongest postcondition for the ∀∃ mode, andthe guard app(TeU,Hx )⇑ and ¬app(TeU,Hx )⇓ ∧ ¬app(TeU,Hx )⇑ for the postcondition {ν | ⊥} ∀∀ and∃∀{ν | ⊥} represent the weakest precondition for e to always diverge and non-deterministicallydiverge, respectively. For each i ∈ {1, . . . ,m}, the guard ∃ν .(ev(app(TeU,Hx ),ν ) ∧pi (Hx ,ν )) represents
the weakest precondition of the given postcondition ν pi (Hx ,ν ) ∃∃ . In Section 6.3, we use strongest
types to prove the relative completeness.
5.2

Denotational Semantics

We define the denotational semantics of types. The denotation JΓ ⊢ σ K of a guarded intersection
and union type σ under a type environment Γ is the set of expressions defined as shown in Fig. 10.
The denotation Jτ K of a refinement type τ is the set of closed values defined as follows:J x ϕ K ≜ n |= [n/x] ϕq Qy   
(x : τ ) → σ ≜ w ∈ Jty(τ → σ )K Qw ′ ∈ Jτ K .w w ′ ∈ J w ′ /x σ K
Finally, the denotation JT K of a simple type T is the set of closed expressions defined as:
JT K ≜ {e | ⊢s e : T }Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:17

J∅ ⊢ σ K ≜ Jσ K
q Qy 
x : τ , Γ ⊢ σ ≜ e Qw ∈ Jτ K . [w/x] e ∈ J[⌊w⌋ /x] Γ ⊢ [⌊w⌋ /x] σ K
tm |
tm |
m
m
_
[
^
\
Jσi K
Jσi K
σi ≜
σi ≜
i=1

i=1

i=1

i=1

Jϕ  σ K ≜ if |= ϕ then Jσ K else Jty(σ )K
(
(
)
)
q QQy
n
H
ω
1 2
τ
≜ e ∈ Jty(τ )K Q 1 π ∈ Z .Q 2n
H ∈ Pref (π ).Q 2w ∈ w e =⇒ w .w ∈ Jτ K
Fig. 10. The denotational semantics of types.

For a type environment ∆ consisting of only universal bindings, we write θ |= ∆ if dom(θ ) = dom(∆)
and θ (x ) ∈ Jθ (τ )K for all (x :∀ τ ) ∈ ∆.
The following are immediate from the definition of the denotational semantics.
Proposition 5.3 (Subject Reduction). We have
q
y
q
y
n
H
• If e ∈ τ ∀Q and e −→ e ′, then e ′ ∈ τ ∀Q .
q
y
q
y
n
H
• If e ∈ τ ∃Q and e is not a value, then e −→ e ′ ∈ τ ∃Q for some n
H and e ′.
n
H1

Proposition 5.4 (Subject Expansion). Suppose that e −→ e 1 ∈ Jσ K. If e 1 = e 2 holds for any n
H2n
H2and e 2 such that e −→ e 2 , then e ∈ Jσ K.

Next, we state several lemmas about the denotational semantics that we use to prove metatheoretic properties of the type system in Section 6.
Lemma 5.5. The following two are equivalent:• e ∈ J∆, Γ ⊢ σ K• θ (e) ∈ J⌊θ ⌋ (Γ) ⊢ ⌊θ ⌋ (σ )K for all value substitutions θ with θ |= ∆.
qyThe following lemma states that τ Q 1 Q 2 restricted to closed values is equivalent to Jτ K.
(
qy)
Lemma 5.6. Jτ K = w | w ∈ τ Q 1 Q 2 holds for any τ , Q 1 , and Q 2 .
yq
The definition of τ Q 1 Q 2 can be rewritten as shown in the following lemma:
Lemma 5.7. We have
q y (
q y)
• τ ∀∃ = e ∈ Jty(τ )K AlwaysTerminates(e) ∧ e ∈ τ ∀∀q ∀∀ y • qτ y = e ∈ Jty(τ )K ∀w ∈ Jty(τ )K .(EvaluatesTo(e,w ) ⇒ w ∈ Jτ K)• τ ∃∃ = (e ∈ Jty(τ )K ∃w ∈ Jty(τ )K .(EvaluatesTo(e,w ) ∧ w )∈ Jτ K)
q ∃∀ yqy• τ= e ∈ Jty(τ )K ¬(AlwaysTerminates(e)) ∨ e ∈ τ ∃∃The following lemma says that refinement types are no more precise than the relation ∼:Lemma 5.8. If e ∼ e ′ then e ∈ J∆ ⊢ σ K ⇔ e ′ ∈ J∆ ⊢ σ K for any ∆ and σ .
Proof. The statement follows from Lemma 5.7 and the assumption explained in Section 5.1 that
the Gödel encoding we adopted is not more precise than the equivalence relation ∼.
□Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:18Hiroshi Unno, Yuki Satake, and Tachio Terauchi

We next define the type subsumption relation JΓ ⊢ σ1 <: σ2 K for guarded intersection and union
types:J∅ ⊢ σ1 <: σ2 K ≜ Jσ1 K ⊆ Jσ2 K
q Q
yx : τ , Γ ⊢ σ1 <: σ2 ≜ Qw ∈ Jτ K . J[⌊w⌋ /x] Γ ⊢ [⌊w⌋ /x] σ1 <: [⌊w⌋ /x]σ2 K

Similarly, we define the subsumption relation JΓ ⊢ τ1 <: τ2 K for refinement types:J∅ ⊢ τ1 <: τ2 K ≜ Jτ1 K ⊆ Jτ2 K
yq Q
x : τ , Γ ⊢ τ1 <: τ2 ≜ Qw ∈ Jτ K . J[⌊w⌋ /x] Γ ⊢ [⌊w⌋ /x] τ1 <: [⌊w⌋ /x]τ2 K

We often abbreviate J∅ ⊢ σ1 <: σ2 K and J∅ ⊢ τ1 <: τ2 K respectively as Jσ1 <: σ2 K and Jτ1 <: τ2 K. We
obtain the following properties of the subsumption relations:Lemma 5.9. The following two are equivalent:• J∆, Γ ⊢ σ1 <: σ2 K
• J⌊θ ⌋ (Γ) ⊢ ⌊θ ⌋ (σ1 ) <: ⌊θ ⌋ (σ2 )K for all value substitutions θ with θ |= ∆.
Also, the following two are equivalent:• J∆, Γ ⊢ τ1 <: τ2 K
• J⌊θ ⌋ (Γ) ⊢ ⌊θ ⌋ (τ1 ) <: ⌊θ ⌋ (τ2 )K for all value substitutions θ with θ |= ∆.
5.3

Extended Typing Rules

We extend the typing rules by the rules shown in Fig 11 that handle guarded intersection and union
types. The figure also shows the extension of the auxiliary function ⌊⊢ x : σ ⌋ to intersection andunion types. Now, having the complete definition of the encoding functions ⌊⊢ x : τ ⌋, ⌊⊢ x : σ ⌋and Γ ⊢ ϕ , we formalize their relationship to the denotational semantics. As shown below, theencoding functions are related to the semantics as follows.
Lemma 5.10. |= [⌊w⌋ /x] ⌊⊢ x : τ ⌋ if and only if w ∈ Jτ K.

Lemma 5.11. Let e be a closed expression. We have |= [TeU/x] ⌊⊢ x : σ ⌋ if and only if e ∈ Jσ K.
Lemma 5.12. The following two are equivalent:• |= ∆, Γ ⊢ ϕ• |= ⌊θ ⌋ ( Γ ⊢ ϕ ) for any value substitutions θ with θ |= ∆.

We explain the additional rules for handling guarded intersection and union types shown in
Fig. 11. The auxiliary function CNF in the rule S-∨ transforms a given type to the conjunctive normal
form. The rule T-Rec∧ generalizes T-Partial and T-Total to guarded intersection types. Thus,
T-Rec∧ can replace the specific rules T-Partial and T-Total. The rule T-VFun∧ is for function
variables. We already have the rule T-VFun for them but the rule T-VFun∧ can assign the strongest
type of the variable expressed by using the Gödel encoding. The type assigned by T-VFun is in
general not the strongest and insufficient for establishing the relative completeness. The ruleT-Guard∧ can introduce a guarded intersection type of an arbitrary expression. The rules S-∨, S-∧,and S-∧∨⊥ are for rearranging a given intersection and union type. For example, we can derive:

 




x :∀ {x | x ≥ 0} ,x , 0 ⊢ x ≥ 1  y y ≥ x − 1 ∀∃ ∧ x < 1  y y ≥ x − 1 ∀∀ <: y y ≥ 0 ∀∃The rules S-Qual⊥ and S-Fun⊥ (resp. the rules S-Guard⊤, S-Qual⊤, and S-Fun⊤) are necessary
for relatively-completely deriving subtyping judgements ∆ ⊢ σ1 <: σ2 such that Jθ (σ1 )K = ∅ (resp.
Jθ (σ2 )K = Jty(σ2 )K) for any θ |= ∆. Finally, the rules S-Case and S-Trans can be used to combine
subtyping rules.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:19


V
V  ′
′
Q i Q i′H
H ′
τf = (Hx :Q Hτ) → m) =α (Hy :Q Hτ )→ mϕi  (τi′ ) Q i Q i
i=1 (ϕ i  τi
i=1



V  (j )H ′′ Q i Q i′
xH ∩ yH = ∅τf(j ) = (Hy :Q Hτ )→ mi=1 ϕ i  (τi )(j )′ϕi(j ) = if Q i′ = ∃ then ϕi′ ∧ ϕ WF
h else ϕi
i

(j )
(j )
fvs(ϕ WF ) ⊆ ( xH,Hy ∪ dom(∆))|= ∆ ⊢ WF (λH
xyH.ϕ WF
)
Qj Q′
H
∆,H
x :Q Hτ ,ϕ j , f :∀ τf(j ) ⊢ e : τ j j(j = 1, . . . ,m)∆ ⊢ rec( f ,H
x ,e) : τf
Q Q′ty(∆(x )) , int(T-VFun∧)∆ ⊢ x : ST(x; pH)∆ ⊢ σi <: σ(i = 1, . . . , ℓ)Wℓ
∆ ⊢ i=1 σi <: σhhiiV|= ∆ ⊢ ¬∃r . ⊢ r : mi=1 σiVℓW∆ ⊢ i=1
σi <: mi=ℓ+1 ¬σi(S-∨)(S-∧∨⊥)Vℓ
CNF (σ ′ ) = i=1σi∆ ⊢ σ <: σi(i = 1, . . . , ℓ)ty(τ ) = TH → int∆ ⊢ TH → {ν | ⊥}Q ∃ <: τ
fvs(ϕ) ⊆ dom(∆)∆,ϕ ⊢ σ1 <: σ2∆, ¬ϕ ⊢ σ1 <: σ2(S-Case)(S-Guard⊤)ty(σ ) = int∆ ⊢ σ <: ϕ  {ν | ⊤}Q ∀(S-Fun⊥)(S-∧)

ty(σ1 ) = ty(σ2 )∆ ⊢ σ1 <: ⊥  σ2

(S-Qual⊥)∆ ⊢ {ν | ⊥}Q ∃ <: σ∆,ϕi ⊢ e : τi i i (i = 1, . . . ,m)(T-Guard∧)V
Q i Q i′∆⊢e : m)i=1 (ϕ i  τi

∆ ⊢ σ <: σ ′ty(σ ) = int∆ ⊢ σ1 <: σ2(T-Rec∧)ty(τ ) = TH → int∆ ⊢ τ <: TH → {ν | ⊤}Q ∀∆ ⊢ σ1 <: σ2(S-Qual⊤)(S-Fun⊤)∆ ⊢ σ2 <: σ3∆ ⊢ σ1 <: σ3(S-Trans)

 _

mi h
mi
ℓ ^
ℓ ^
_
i
 =
⊢ x :
⊢
x
:
σ
σ
i
j
i
j


i=1 j=1
 i=1 j=1
Fig. 11. The extension of the typing rules and the auxiliary function ⌊⊢ x : σ ⌋ for intersections and unions.

5.4

Toward Automation

We briefly remark on how one may automate the type checking and type inference for our typesystem. Though automated type inference is out of the scope of the present paper, we havecarefully designed the type system to allow a future extension to automated inference, based on
our experiences on developing refinement type inference and related methods [Hashimoto andUnno 2015; Kobayashi et al. 2011; Kuwahara et al. 2015, 2014; Terauchi 2010; Unno and Kobayashi
2009; Unno et al. 2013].
To develop a practical type checking or inference method, we need to devise a sound approximation of the Gödel encoding used to establish relative completeness (in the rule T-VFun∧ andthe auxiliary functions). One possibility is to adopt the approach of [Unno et al. 2013] and use
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:20Hiroshi Unno, Yuki Satake, and Tachio Terauchi

as the background theory an efficiently decidable theory such as the quantifier-free first-ordertheory of linear integer arithmetic instead of the second-order Peano arithmetic, and employ a lessprecise but sound encoding of function values.7 Note however that, unlike [Unno et al. 2013], we
also need check the non-emptiness of ∃x ∈ Jσ K .ϕ at Skolemization. For the type semantics that
we defined, this can be difficult when σ is a function type. One way to make the non-emptinesschecking practical is to enlarge the domain of functions to arbitrary mathematical higher-ordernon-deterministic functions instead of the definable ones. This substantially simplifies the problem(indeed, the check can then be done by calling the decision procedure for the background theory).
As remarked in Section 5.1, such a change still retains soundness, except that now function-type
variables are assumed to also range over non-definable ones.
We remark that, the type inference requires, besides a sound approximation of the Gödel encoding,the synthesis of inductive invariants (expressed as dependent refinement types), well-founded
relations (in T-Total and T-Rec∧), and predicates for Skolemization (in T-Skolem). A possible
approach to automating such tasks is to leverage constraint solving of existentially-quantified Hornclauses with well-foundedness constraints, for which existing techniques are available [Beyene
et al. 2013; Hashimoto and Unno 2015; Kuwahara et al. 2015, 2014; Popeea and Rybalchenko 2012;
Unno et al. 2013].
6

META-PROPERTIES OF THE TYPE SYSTEM

This section shows meta-properties of the type system. In Section 6.1, we prove the correctness ofthe type complement operator ¬, thereby proving that the types are closed under complement inour system. We then prove the soundness and the relative completeness respectively in Sections 6.2
and 6.3.
6.1

Correctness of Complement Types

The correctness is stated and proved using the denotational semantics as follows.
Theorem 6.1 (Correctness of Complement Types). We have
• For any σ and integer substitution ρ with dom(ρ) = fvs(σ ), Jρ (¬σ )K = Jty(σ )K \ Jρ (σ )K holds.
• For any τ and integer substitution ρ with dom(ρ) = fvs(τ ), Jρ (¬τ )K = Jty(τ )K \ Jρ (τ )K holds.

Proof. By mutual induction on the structure of σ and τ .

• Case σ = τ Q 1 Q 2 : Let ρ be an integer substitution with dom(ρ) = fvs(σ ). By I.H., we obtainJρ (¬τ )K = Jty(τ )K \ Jρ (τ )K. We then haveJρ (¬σ )K = J(ρ (¬τ )) Q 1 Q 2 KnH= {e ∈ Jty(ρ (¬τ ))K | Q 1 π ∈ Zω .Q 2n
H ∈ Pref (π ).Q 2w ∈ {w | e =⇒ w }.w ∈ Jρ (¬τ )K}nH= {e ∈ Jty(τ )K | ¬(Q 1 π ∈ Zω .Q 2n
H ∈ Pref (π ).Q 2w ∈ {w | e =⇒ w }.w ∈ Jρ (τ )K)}
= Jty(σ )K \ Jρ (σ )K• Case σ = ϕ  σ ′: Let ρ be an integer substitution with dom(ρ) = fvs(σ ). By I.H., we obtainJρ (¬σ ′ )K = Jty(σ ′ )K \ Jρ (σ ′ )K. If |= ρ (ϕ) holds, we getqyJρ (¬σ )K = ρ (¬ϕ)  {x | ⊥} ∀∃ ∩ Jρ (¬σ ′ )K = Jρ (¬σ ′ )K = Jty(σ ′ )K \ Jρ (σ ′ )K = Jty(σ )K \ Jρ (σ )K
7 The approximation is motivated by the observation that programmers rarely write programs whose correctness relies

heavily on function-type arguments.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:21

Otherwise (i.e., |= ρ (¬ϕ)), we haveqyJρ (¬σ )K = ρ (¬ϕ)  {x | ⊥} ∀∃ ∩ Jρ (¬σ ′ )K = ∅ = Jty(σ )K \ Jty(σ ′ )K = Jty(σ )K \ Jρ (σ )KWℓ Vmi• Case σ = i=1
j=1 σi j : Let ρ be an integer substitution with dom(ρ) = fvs(σ ). By I.H., we
obtain Jρ (¬σi j )K = Jty(σi j )K \ Jρ (σi j )K. We then have
u
}
mi
mi 
ℓ _
ℓ [
^
\

*.
Jρ (¬σ )K = vDNF *.
Jty(σi j )K \ Jρ (σi j )K +/ρ (¬σi j ) +/~ =i=1 , j=1
, i=1 j=1mℓ \i[*. Jρ (σ )K+/ = Jty(σ )K \ Jρ (σ )K= Jty(σ )K \ij
i=1 , j=1

• Case τ = x ϕ : Let ρ be an integer substitution with dom(ρ) = fvs(τ ). We then haveJρ (¬τ )K = J x ¬ρ (ϕ) K = Jty(τ )K \ Jρ (τ )K.
• Case τ = ((x :Q τ ′ ) → σ ): Let ρ be an integer substitution with dom(ρ) = fvs(τ ). By I.H., we
obtain Jρ ′ (¬σ )K = Jty(σ )K \ Jρ ′ (σ )K for any ρ ′ with dom(ρ ′ ) = fvs(σ ). We thus getrzJρ (¬τ )K = (x :Q ρ (τ ′ )) → ρ (¬σ ))(  
= w ∈ Jty(ρ (τ ′ ) → ρ (¬σ ))K Qw ′ ∈ Jρ (τ ′ )K .w w ′ ∈ J w ′ /x ρ (¬σ )K  
= w ∈ Jty(τ )K ¬(Qw ′ ∈ Jρ (τ ′ )K .w w ′ ∈ J w ′ /x ρ (σ )K)= Jty(τ )K \ Jρ (τ )K

6.2□

Soundness

We now prove the soundness of our type system with respect to the denotational semantics. We
first show the necessary lemmas.
The following lemmas are used respectively to establish the soundness of the subtyping rules
S-Guard, S-Qual, S-Fun∀∀, S-Fun∀∃, S-Fun∃∃, and S-Fun∃∀.
Lemma 6.2. Jϕ 1  σ1 <: ϕ 2  σ2 K if |= ϕ 2 ⇒ ϕ 1 and Jσ1 <: σ2 K.
r
z
Q Q′
Q Q′
Lemma 6.3. τ1 1 1 <: τ2 2 2 if Jτ1 <: τ2 K and Q 1Q 1′ ⊑ Q 2Q 2′ .
qyqyLemma 6.4. (x :∀ τ1 ) → σ1 <: (x :∀ τ2 ) → σ2 if Jτ2 <: τ1 K and x :∀ τ2 ⊢ σ1 <: σ2 .
qyqyLemma 6.5. (x :∀ τ1 ) → σ1 <: (x : ∃ τ2 ) → σ2 if Jτ <: τ1 K, Jτ <: τ2 K, and x : ∃ τ ⊢ σ1 <: σ2 forsome τ .
qyqyLemma 6.6. (x : ∃ τ1 ) → σ1 <: (x : ∃ τ2 ) → σ2 if Jτ1 <: τ2 K and x :∀ τ1 ⊢ σ1 <: σ2 .
qyLemma 6.7. (x : ∃ τ1 ) → σ1 <: (y :∀ τ2 ) → σ2 if the following conditions hold:hi• |= x 1 :∀ τ1 ,x 2 :∀ τ2 ,y1 :∀ τ1 ,y2 :∀ τ2 ⊢ x 1 = x 2 ∧ y1 = y2 ⇒ x 1 = y1 ,• x :∀ τ1 ,y :∀ τ2 ,x = y ⊢ σ1 <: σ2 ,• x :∀ τ1 ,y : ∃ τ2 ,x , y ⊢ σ1 <: TH → {ν | ⊥} ∃∃ ,• y :∀ τ2 ,x : ∃ τ1 ,x , y ⊢ TH → {ν | ⊤} ∀∀ <: σ2 , and• ty(σ1 ) = TH → int.
We thus obtain the soundness of the subtyping rules with respect to the subsumption relations.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:22Hiroshi Unno, Yuki Satake, and Tachio Terauchi

Lemma 6.8 (Soundness of Subtyping). We have:• JΓ ⊢ σ1 <: σ2 K if Γ ⊢ σ1 <: σ2 .
• JΓ ⊢ τ1 <: τ2 K if Γ ⊢ τ1 <: τ2 .
We next show lemmas that are used to establish the soundness of the typing rules T-Partial,
T-Total, and T-Rec∧ for recursive functions. The following lemma provides a sufficient condition
for a recursive function to be included in the denotation of a partial correctness function type.
r
z
q y
H
H
Lemma 6.9. Suppose that e ∈ xH:Q H
τ , f : τf ⊢ τ Q ∀ . Then, rec( f ,H
x ,e) ∈ τf , where τf = (Hx :QHτ ) → τ Q ∀.
Next, we state the sufficient condition for a recursive function to be included in the denotationof a total correctness function type.
Lemma 6.10. Let τf and τf′ be types of the form τf = (Hx :Q Hy :Q Hτ ) → τ Q ∃ and τf′ = (Hτ ′ ) → ϕ(τ ′ ) Q ∃that satisfy the following condition• xH ∩ yH = ∅;H ′• τf =α (Hy :Q Hτ ) → (τ ′ ) Q ∃ ;• |= WF (λH
xyH.ϕ); and• fvs(ϕ) ⊆ xH,H
y .
r
z
q y
H
Q
Then, e ∈ xH: H
τ , f : τf′ ⊢ τ Q ∃ implies rec( f ,H
x ,e) ∈ τf .
H

H

For guarded intersection types, we get the following generalization of Lemmas 6.9 and 6.10.
V
Q i Q i′H
Lemma 6.11. Let τf and τf(j ) be types of the form τf = (Hx :Q Hτ) → m) and τf(j ) =i=1 (ϕ i  τi
V
′
H ′
(H
y :Q Hτ )→ m(ϕ (j )  (τi′ ) Q i Q i ) that satisfy the following condition: i=1 i• xH ∩ yH = ∅;

V  ′
H ′
′ Q i Q i′ ;• τf =α (Hy :Q Hτ )→ mi=1 ϕ i  (τi )(j )• ϕi(j ) = ϕi′ ∧ ϕ WF
if Q i′ = ∃ and ϕi(j ) = ϕi′ otherwise;hi(j )• |= ∆ ⊢ WF (λH
xyH.ϕ WF
) ; and(j )• fvs(ϕ WF) ⊆ ( xH,Hy ∪ dom(∆)).
r
z
q y
Qj Q′
H
Then, we have rec( f ,H
x ,e) ∈ τf if e ∈ xH:Q H
τ ,ϕ j , f : τf(j ) ⊢ τ j j for each j ∈ {1, . . . ,m}.

Finally, we obtain the following soundness theorem by induction on the derivation of Γ ⊢ e : σ .
Theorem 6.12 (Soundness). e ∈ JΓ ⊢ σ K if Γ ⊢ e : σ .
6.3

Relative CompletenessWe prove the relative completeness of our type system with respect to the denotational semantics.
We first show the necessary lemmas.
The following lemma ensures that we can always apply Skolemization first to eliminate existentially bound variables.
qyLemma 6.13 (Skolemization). If e ∈ ∆,x h: ∃ τ , Γ ⊢ σ , thenthere exists ϕ with fvs(ϕ) ⊆ (fvs(∆) ∪
i
q
y
∀
∃
{x }) such that e ∈ ∆,x : τ ,ϕ, Γ ⊢ σ and |= ∆,x : τ ⊢ ϕ .
qyProof. Suppose that e ∈ ∆,x : ∃ τ , Γ ⊢ σ . By Lemma 5.5, we get ∃w ∈ J⌊θ ⌋ (τ )K .[w/x](θ (e)) ∈J⌊θ ⌋ (Γ) ⊢ [⌊w⌋ /x](⌊θ ⌋ (σ ))K for any value substitution θ with θ |= ∆. There exists ϕ with fvs(ϕ) ⊆(dom(∆) ∪ {x }) such that:
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:23• ∀w ∈ J⌊θ ⌋ (τ )K . |= [⌊w⌋ /x](⌊θ ⌋ (ϕ)) ⇒ [w/x](θ (e)) ∈ J⌊θ ⌋ (Γ) ⊢ [⌊w⌋ /x](⌊θ ⌋ (σ ))K and• ∃w ∈ J⌊θ ⌋ (τ )K . |= [⌊w⌋ /x](⌊θ ⌋ (ϕ)) for any value substitution θ with θ |= ∆.
hiqyBy Lemma 5.5, we obtain e ∈ ∆,x :∀ τ ,ϕ, Γ ⊢ σ . By Lemma 5.12, we get |= ∆,x : ∃ τ ⊢ ϕ .
□The following lemmas are used respectively to establish the relative completeness of the subtyping
rules S-Guard, S-Qual⊥, S-Qual⊤, S-Qual, S-Fun∀∀, S-Fun∀∃, S-Fun∃∃, and S-Fun∃∀.8
Lemma 6.14. If ∅ , Jϕ 1  σ1 K ⊆ Jϕ 2  σ2 K , Jty(σ2 )K, then |= ϕ 2 ⇒ ϕ 1 and Jσ1 <: σ2 K.
rz
Lemma 6.15. If x ϕ Q 1 Q 2 = ∅, then |= ¬ϕ and Q 2 = ∃.
rzLemma 6.16. If x ϕ Q 1 Q 2 = JintK, then |= ϕ and Q 2 = ∀.
r
z r
z
Q Q′
Q Q′
Lemma 6.17. If ∅ , τ1 1 1 ⊆ τ2 2 2 , Jty(τ2 )K, then Jτ1 <: τ2 K and Q 1Q 1′ ⊑ Q 2Q 2′ .
q
y
q
y

Lemma 6.18.q If ∅ , (x :∀ τ1 y) → σ1 ⊆ (x :∀ τ2 ) → σ2 , w ⊢s w : ty(τ2 ) → ty(σ2 ) , thenJτ2 <: τ1 K and x :∀ τ2 ⊢ σ1 <: σ2 .
q
y
q
y

Lemma 6.19. If ∅ , q(x :∀ τ1 ) → σ1 y⊆ (x : ∃ τ2 ) → σ2 , w ⊢s w : ty(τ2 ) → ty(σ2 ) , thenJτ <: τ1 K, Jτ <: τ2 K, and x : ∃ τ ⊢ σ1 <: σ2 for some τ .
q
y
q
y

Lemma 6.20.q If ∅ , (x : ∃ τ1 y) → σ1 ⊆ (x : ∃ τ2 ) → σ2 , w ⊢s w : ty(τ2 ) → ty(σ2 ) , thenJτ1 <: τ2 K and x :∀ τ1 ⊢ σ1 <: σ2 .
q
y q
y 
Lemma 6.21. If ∅ , (x : ∃ τ1 ) → σ1 ⊆ (y :∀ τ2 ) → σ2 , w ⊢s w : ty(τ2 ) → ty(σ2 ) , then thefollowing conditions hold:hi• |= x 1 :∀ τ1 ,x 2 :∀ τ2 ,y1 :∀ τ1 ,y2 :∀ τ2 ⊢ x 1 = x 2 ∧ y1 = y2 ⇒ x 1 = y1 ,• x :∀ τ1 ,y :∀ τ2 ,x = y ⊢ σ1 <: σ2 ,• x :∀ τ1 ,y : ∃ τ2 ,x , y ⊢ σ1 <: TH → {ν | ⊥} ∃∃ ,• y :∀ τ2 ,x : ∃ τ1 ,x , y ⊢ TH → {ν | ⊤} ∀∀ <: σ2 , and• ty(σ1 ) = TH → int.
We then obtain the following relative completeness of the subtyping rules with respect to thesubsumption relations.
Lemma 6.22 (Relative Completeness of Subtyping). We have:• ∆ ⊢ τ1 <: τ2 if J∆ ⊢ τ1 <: τ2 K.
• ∆ ⊢ σ1 <: σ2 if J∆ ⊢ σ1 <: σ2 K.

The following lemma states the correctness of the strongest type ST(e; pH).
Qi j Q ′Wℓ VmiH
Lemma 6.23. Suppose that e ∈ J∆ ⊢ σ K for some σ = (Hx :Q Hτ ) → i=1
(ϕi j  τi j i j ). Let
j=1
(
)


pH = p | i ∈ {1, . . . , ℓ} , j ∈ {1, . . . ,mi } ,Q i j = ∃,τi j = ν p(Hx ,ν ) . We have J∆ ⊢ ST(e; pH) <: σ K.

The following lemma says that the typing rules can in fact assign the strongest type ST(e; pH) to
any simply-typed expression e.

Lemma 6.24. Suppose that A ⊢s e : TH → int for some A and TH. We then have ∆ ⊢ e : ST(e; pH) forany ∆ and pH such that ty(∆) = A, and each element p of pH is well-formed (i.e., the arity of p is |TH| + 1
and fvs(p) ⊆ dom(A)).
8 To prove the lemmas, we use an extension of the denotational semantics of types that ranges over L-definable expressions

that may use the operators ev and ⇓.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:24Hiroshi Unno, Yuki Satake, and Tachio Terauchi

Finally, we obtain the following relative completeness theorem.
Theorem 6.25 (Relative Completeness). Γ ⊢ e : σ if e ∈ JΓ ⊢ σ K.

Proof. By the rule T-Skolem and Lemma 6.13, it suffices to show that ∆ ⊢ e : σ is implied bye ∈ J∆ ⊢ σ K for any ∆. By Lemmas 6.23 and 6.22, we obtain ∆ ⊢ ST(e; pH) <: σ for some well-formed
pH. By Lemma 6.24 and the rule T-Sub, we get ∆ ⊢ e : σ .
□7

RELATED WORKThis paper proposes a refinement-type-based approach to verifying non-deterministic higher-orderfunctional programs. The type system combines universal and existential reasoning in a unified
framework, and is able to soundly-and-relatively-completely verify various important classes ofproperties including safety, non-safety, conditional termination, and conditional non-termination.
To our knowledge, our work is the first of its kind.
As remarked in Section 1, previous work on higher-order program verification employs rather
disparate methods to verify different classes of properties [Hashimoto and Unno 2015; Jhala et al.
2011; Kobayashi et al. 2011; Koskinen and Terauchi 2014; Kuwahara et al. 2015, 2014; Murase et al.
2016; Ong and Ramsay 2011; Rondon et al. 2008; Terauchi 2010; Unno and Kobayashi 2009; Unno
et al. 2013; Vazou et al. 2014; Zhu and Jagannathan 2013; Zhu et al. 2015]. To our knowledge, there
has only been a limited consideration for combined universal and existential reasoning in thesetting of higher-order program verification (with a few notable exceptions such as the use ofsafety to prove non-termination by way of iterative predicate abstraction and higher-order model
checking in [Kuwahara et al. 2015]). By contrast, we have proposed a unified type-based frameworkin which the type judgements expressing universal and existential facts can be readily combined
as sub-derivations to derive the goal fact. As demonstrated in Section 2, the seamless combined
reasoning offers powerful verification tactics that permit succinct proofs of non-trivial verification
instances.
In the context of verification of programs with first-order functions and procedures, previous
work has considered combining universal and existential reasoning [Ball et al. 2005; Godefroid andHuth 2005; Godefroid et al. 2001, 2010; Gurfinkel and Chechik 2006; Gurfinkel et al. 2006, 2008]. (Inthe literature, universal-existential reasoning is sometimes referred to as may-must.) However, to
our knowledge, no previous work covers the combination patterns of this paper nor proposes aunified deduction system to carry out the combined reasoning. For instance, [Godefroid et al. 2001]
proposes a safety and non-safety property verification method for first-order programs that allows a
combined use of may function summaries and must function summaries. May summaries correspondH
to the types of the form (Hx :∀ Hτ and τ are restricted to baseτ ) → τ ∀∀ of our type system (where H
types), whereas must summaries say that, for every state satisfying the postcondition, there is astate satisfying the precondition and an evaluation of the function from the pre state that converges
to the post state. Their approach does not have notions corresponding to the other modes supported
by our system. Therefore, for example, their approach cannot use a conditional termination proof
via well-foundedness termination argument to deduce the existence of an evaluation path satisfying
a certain fact, as we have done in Example 2.1 and Example 2.2. Such reasoning is also beyond thescope of the approaches proposed in [Gurfinkel and Chechik 2006; Gurfinkel et al. 2006, 2008]. On
the other hand, our system lacks an exact counterpart of their must summaries, and we leave for
future work to investigate the implications of incorporating such a notion.9
9 However, must summaries are only built from concrete evaluation paths and used as such in [Godefroid et al. 2001], and it

is possible to do the examples in their paper with our system by using the types of the form (Hx :∃ Hτ ) → τ ∃∃ in place of mustsummaries.
H

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:25

The combined universal and existential reasoning is often considered in the context of verifying
temporal logic properties [Beyene et al. 2013; Cook et al. 2015; Cook and Koskinen 2013; Gabbay
and Pnueli 2008; Godefroid and Huth 2005; Godefroid et al. 2001; Shoham and Grumberg 2004, 2007].
This is because such properties can themselves be a combination of safety and liveness properties,
or contain alternations of universal and existential branches (for branching logics). Compared to
our work that handle higher-order and non-deterministic programs, these works typically focus onmuch simpler transition systems but handle richer temporal properties.10 Similar to our work, theyreason about AG and AF based on inductive invariants and well-founded relations, and some haverules for reasoning about EG and EF via Skolemization [Cook et al. 2015; Cook and Koskinen 2013].
We generalize such reasoning to the higher-order setting using refinement types and well-founded
relations over (Gödel encoded) higher-type objects. An advantage of our system, especially in thecontext of expressive programming languages like higher-order functional languages, is that itallows modular reasoning thanks to the compositional nature of the type system.
By contrast, the existing work on temporal logic property verification for higher-order programs
has paid little attention to the combined reasoning aspect. For instance, the method proposed by[Murase et al. 2016] applies the automata-theoretic reduction to convert the verification problem
wholly to a fair termination problem, and the method proposed by [Koskinen and Terauchi 2014]
considers only one-sided “blackbox” combination patterns that connect external oracle analyses’
results to their type and effect system (also, neither approach addresses branching logics).11 Our
current system does not support temporal logics. Nonetheless, we believe that the ideas developedin this paper will contribute to improving the methods for verifying temporal logic propertiesof higher-order programs. We leave for future work to extend our approach to the full range of
temporal logic properties.
The previous work has proposed dependent refinement type systems for partial and total correctness verification [Bengtson et al. 2011; Rondon et al. 2008; Swamy et al. 2011, 2016; Terauchi 2010;
Unno and Kobayashi 2009; Vazou et al. 2014; Xi 2001]. The majority of such works only address
partial correctness, with [Swamy et al. 2016; Vazou et al. 2014; Xi 2001] being the exception that also
address total correctness (or just termination). Total correctness is verified via typing rules similar tothe ones of our work. Also, while many of them (often implicitly) support demonic non-determinism,to our knowledge, none of them supports angelic non-determinism. We remark that the complexityof our type system is mainly due to supporting (1) angelic non-determinism, (2) the combined
universal and existential reasoning, and (3) relative completeness. If we drop the support for (1),then our system can be simplified by removing the existential bindings in the type environment
and the arguments of function types, and removing the rules T-Rnd, T-Skolem, and T-App∃. If wedrop (2), then our system can be further simplified by removing the rules S-Qual, S-Fun∀∃, andS-Fun∃∀. And, if we drop (3), then we can remove Gödel encoding, guarded intersection and union
types, and the additional rules from Section 5 for handling them.
Our type system is sound and relatively-complete. The well-known issue in achieving relativecompleteness for higher-order programs is the representation of function-type parameters. Following the previous work on relatively complete verification of higher-order programs [Dammand Josko 1983; German et al. 1983, 1989; Goerdt 1985; Honda et al. 2006; Olderog 1984; Reus
and Streicher 2011; Unno et al. 2013], we completely handle function parameters by encoding
them as first-order data ([Unno et al. 2013] shows how such a formalism can be made practical
10 In the terminology of temporal logics, the specifications in our system are limited to the forms p ⇒ AGq, p ⇒ AF q,
p ⇒ EGq, and p ⇒ E F q.
11 Sound and complete verification methods exist for finite-data higher-order programs (i.e., higher-order recursion schemes)
for the expressive class of (branching) modal µ-calculus [Kobayashi and Ong 2009; Ong 2006]. However, it is unclear how
such methods may be adopted to infinite data programs.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:26Hiroshi Unno, Yuki Satake, and Tachio Terauchi

for automation by avoiding explicit encoding). However, while the previous work only consideredsafety properties (i.e., partial correctness), our system is sound and relatively-complete also for
non-safety, conditional termination and conditional non-termination.
8

CONCLUSION

We have presented a novel type system for verification of non-deterministic higher-order functional
programs. The type system is a dependent refinement type system extended to support universal andexistential reasoning, and is sound and relatively-complete for the verification of various importantclasses of properties including safety, non-safety, conditional termination, and conditional nontermination. We have shown that the type system allows combined universal and existential
reasoning, which can lead to succinct proofs of hard verification instances. We believe that thiswork will serve as a theoretical foundation toward automatic verification of non-deterministic
higher-order programs, and also pave the way for new verification methods that combine universal
and existential reasoning.
ACKNOWLEDGMENTS
We thank Naoki Kobayashi and anonymous referees for useful comments and Jean Yang for being
our shepherd. This work was supported by JSPS KAKENHI Grant Numbers 15H05706, 16H05856,
17H01720, and 17H01723; JSPS Bilateral Programs; and JSPS Core-to-Core Program, A.Advanced
Research Networks.
REFERENCES
Thomas Ball, Orna Kupferman, and Greta Yorsh. 2005. Abstraction for Falsification. In Computer Aided Verification, 17th
International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings (Lecture Notes in Computer
Science), Kousha Etessami and Sriram K. Rajamani (Eds.), Vol. 3576. Springer, 67–81. https://doi.org/10.1007/11513988_8
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Sergio Maffeis. 2011. Refinement types forsecure implementations. ACM Trans. Program. Lang. Syst. 33, 2 (2011), 8:1–8:45. https://doi.org/10.1145/1890028.1890031
Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses.
In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013.
Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 869–882.
https://doi.org/10.1007/978-3-642-39799-8_61
Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O’Hearn. 2014. Proving Nontermination via
Safety. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014,
Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13,
2014. Proceedings (Lecture Notes in Computer Science), Erika Ábrahám and Klaus Havelund (Eds.), Vol. 8413. Springer,
156–171. https://doi.org/10.1007/978-3-642-54862-8_11
Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi. 2007. Proving that programs
eventually do something good. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2007, Nice, France, January 17-19, 2007, Martin Hofmann and Matthias Felleisen (Eds.). ACM, 265–276.
https://doi.org/10.1145/1190216.1190257
Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015. On Automation of CTL* Verification for Infinite-State Systems. In
Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings,
Part I (Lecture Notes in Computer Science), Daniel Kroening and Corina S. Pasareanu (Eds.), Vol. 9206. Springer, 13–29.
https://doi.org/10.1007/978-3-319-21690-4_2
Byron Cook and Eric Koskinen. 2013. Reasoning about nondeterminism in programs. In ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm
and Cormac Flanagan (Eds.). ACM, 219–230. https://doi.org/10.1145/2491956.2491969
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2006. Termination proofs for systems code. In Proceedings of the
ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June
11-14, 2006, Michael I. Schwartzbach and Thomas Ball (Eds.). ACM, 415–426. https://doi.org/10.1145/1133981.1134029
Werner Damm and Bernhard Josko. 1983. A Sound and Relatively * Complete Hoare-Logic for a Language With Higher
Type Procedures. Acta Inf. 20 (1983), 59–101. https://doi.org/10.1007/BF00264295

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:27

Dov M. Gabbay and Amir Pnueli. 2008. A Sound and Complete Deductive System for CTL* Verification. Logic Journal of the
IGPL 16, 6 (2008), 499–536. https://doi.org/10.1093/jigpal/jzn018
Steven M. German, Edmund M. Clarke, and Joseph Y. Halpern. 1983. Reasoning About Procedures as Parameters. In Logicsof Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings (Lecture Notes in
Computer Science), Edmund M. Clarke and Dexter Kozen (Eds.), Vol. 164. Springer, 206–220. https://doi.org/10.1007/
3-540-12896-4_365
Steven M. German, Edmund M. Clarke, and Joseph Y. Halpern. 1989. Reasoning about Procedures as Parameters in the
Language L4. Inf. Comput. 83, 3 (1989), 265–359. https://doi.org/10.1016/0890-5401(89)90040-0
Patrice Godefroid and Michael Huth. 2005. Model Checking Vs. Generalized Model Checking: Semantic Minimizations for
Temporal Logics. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA,
Proceedings. IEEE Computer Society, 158–167. https://doi.org/10.1109/LICS.2005.28
Patrice Godefroid, Michael Huth, and Radha Jagadeesan. 2001. Abstraction-Based Model Checking Using Modal Transition
Systems. In CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001,
Proceedings (Lecture Notes in Computer Science), Kim Guldstrand Larsen and Mogens Nielsen (Eds.), Vol. 2154. Springer,
426–440. https://doi.org/10.1007/3-540-44685-0_29
Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and SaiDeep Tetali. 2010. Compositional may-must program analysis:
unleashing the power of alternation. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo and Jens Palsberg(Eds.). ACM, 43–56. https://doi.org/10.1145/1706299.1706307
Andreas Goerdt. 1985. A Hoare Calculus for Functions Defined by Recursion on Higher Types. In Logics of Programs,
Conference, Brooklyn College, June 17-19, 1985, Proceedings (Lecture Notes in Computer Science), Rohit Parikh (Ed.), Vol. 193.
Springer, 106–117. https://doi.org/10.1007/3-540-15648-8_9
Arie Gurfinkel and Marsha Chechik. 2006. Why Waste a Perfectly Good Abstraction?. In Tools and Algorithms for theConstruction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings(Lecture Notes in Computer Science), Holger Hermanns and Jens Palsberg (Eds.), Vol. 3920. Springer, 212–226. https://doi.org/10.1007/11691372_14
Arie Gurfinkel, Ou Wei, and Marsha Chechik. 2006. Yasm: A Software Model-Checker for Verification and Refutation. In
Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings(Lecture Notes in Computer Science), Thomas Ball and Robert B. Jones (Eds.), Vol. 4144. Springer, 170–174. https://doi.org/10.1007/11817963_18
Arie Gurfinkel, Ou Wei, and Marsha Chechik. 2008. Model Checking Recursive Programs with Exact Predicate Abstraction.
In Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea, October
20-23, 2008. Proceedings (Lecture Notes in Computer Science), Sung Deok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee,and Mahesh Viswanathan (Eds.), Vol. 5311. Springer, 95–110. https://doi.org/10.1007/978-3-540-88387-6_9
Kodai Hashimoto and Hiroshi Unno. 2015. Refinement Type Inference via Horn Constraint Optimization. In Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings (Lecture Notes in
Computer Science), Sandrine Blazy and Thomas Jensen (Eds.), Vol. 9291. Springer, 199–216. https://doi.org/10.1007/
978-3-662-48288-9_12
Kohei Honda, Martin Berger, and Nobuko Yoshida. 2006. Descriptive and Relative Completeness of Logics for Higher-Order
Functions. In Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14,
2006, Proceedings, Part II (Lecture Notes in Computer Science), Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo
Wegener (Eds.), Vol. 4052. Springer, 360–371. https://doi.org/10.1007/11787006_31
Ranjit Jhala, Rupak Majumdar, and Andrey Rybalchenko. 2011. HMC: Verifying Functional Programs Using Abstract
Interpreters. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011.
Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Vol. 6806. Springer,
470–485. https://doi.org/10.1007/978-3-642-22110-1_38
Naoki Kobayashi. 2009. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedingsof the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA,
January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 416–428. https://doi.org/10.1145/1480881.1480933
Naoki Kobayashi and C.-H. Luke Ong. 2009. A Type System Equivalent to the Modal Mu-Calculus Model Checking ofHigher-Order Recursion Schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS
2009, 11-14 August 2009, Los Angeles, CA, USA. IEEE Computer Society, 179–188. https://doi.org/10.1109/LICS.2009.29
Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. 2011. Predicate abstraction and CEGAR for higher-order model checking.
In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011,
San Jose, CA, USA, June 4-8, 2011, Mary W. Hall and David A. Padua (Eds.). ACM, 222–233. https://doi.org/10.1145/
1993498.1993525

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

12:28Hiroshi Unno, Yuki Satake, and Tachio Terauchi

Eric Koskinen and Tachio Terauchi. 2014. Local temporal reasoning. In Joint Meeting of the Twenty-Third EACSL Annual
Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer
Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM,
59:1–59:10. https://doi.org/10.1145/2603088.2603138
Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, and Naoki Kobayashi. 2015. Predicate Abstraction and CEGAR for Disproving
Termination of Higher-Order Functional Programs. In Computer Aided Verification - 27th International Conference, CAV
2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II (Lecture Notes in Computer Science), Daniel Kroening
and Corina S. Pasareanu (Eds.), Vol. 9207. Springer, 287–303. https://doi.org/10.1007/978-3-319-21668-3_17
Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi. 2014. Automatic Termination Verification forHigher-Order Functional Programs. In Programming Languages and Systems - 23rd European Symposium on Programming,
ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble,
France, April 5-13, 2014, Proceedings (Lecture Notes in Computer Science), Zhong Shao (Ed.), Vol. 8410. Springer, 392–411.
https://doi.org/10.1007/978-3-642-54833-8_21
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. 2016. Temporal verification ofhigher-order functional programs. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar(Eds.). ACM, 57–68. https://doi.org/10.1145/2837614.2837667
Ernst-Rüdiger Olderog. 1984. Correctness of Programs with Pascal-Like Procedures without Global Variables. Theor. Comput.
Sci. 30 (1984), 49–90. https://doi.org/10.1016/0304-3975(84)90066-5
C.-H. Luke Ong. 2006. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In 21th IEEE Symposiumon Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings. IEEE Computer Society, 81–90.
https://doi.org/10.1109/LICS.2006.38
C.-H. Luke Ong and Steven J. Ramsay. 2011. Verifying higher-order functional programs with pattern-matching algebraic
data types. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2011, Austin, TX, USA, January 26-28, 2011, Thomas Ball and Mooly Sagiv (Eds.). ACM, 587–598. https://doi.org/10.1145/
1926385.1926453
Corneliu Popeea and Andrey Rybalchenko. 2012. Compositional Termination Proofs for Multi-threaded Programs. In Tools
and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of
the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012.
Proceedings (Lecture Notes in Computer Science), Cormac Flanagan and Barbara König (Eds.), Vol. 7214. Springer, 237–251.
https://doi.org/10.1007/978-3-642-28756-5_17
Bernhard Reus and Thomas Streicher. 2011. Relative Completeness for Logics of Functional Programs. In Computer Science
Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen,
Norway, Proceedings (LIPIcs), Marc Bezem (Ed.), Vol. 12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 470–480.
https://doi.org/10.4230/LIPIcs.CSL.2011.470
Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In Proceedings of the ACM SIGPLAN 2008
Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, Rajiv Gupta andSaman P. Amarasinghe (Eds.). ACM, 159–169. https://doi.org/10.1145/1375581.1375602
Sharon Shoham and Orna Grumberg. 2004. Monotonic Abstraction-Refinement for CTL. In Tools and Algorithms for theConstruction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European
Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings(Lecture Notes in Computer Science), Kurt Jensen and Andreas Podelski (Eds.), Vol. 2988. Springer, 546–560. https://doi.org/10.1007/978-3-540-24730-2_40
Sharon Shoham and Orna Grumberg. 2007. A game-based framework for CTL counterexamples and 3-valued abstractionrefinement. ACM Trans. Comput. Log. 9, 1 (2007), 1. https://doi.org/10.1145/1297658.1297659
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang. 2011. Secure distributed
programming with value-dependent types. In Proceeding of the 16th ACM SIGPLAN international conference on Functional
Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier
Danvy (Eds.). ACM, 266–278. https://doi.org/10.1145/2034773.2034811
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016.
Dependent types and multi-monadic effects in F. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and
Rupak Majumdar (Eds.). ACM, 256–270. https://doi.org/10.1145/2837614.2837655
Tachio Terauchi. 2010. Dependent types from counterexamples. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposiumon Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, Manuel V. Hermenegildo andJens Palsberg (Eds.). ACM, 119–130. https://doi.org/10.1145/1706299.1706315

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.

Relatively Complete Refinement Type System for Verification of Higher-Order ...

12:29

Hiroshi Unno and Naoki Kobayashi. 2009. Dependent type inference with interpolants. In Proceedings of the 11th International
ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal,
António Porto and Francisco Javier López-Fraguas (Eds.). ACM, 277–288. https://doi.org/10.1145/1599410.1599445
Hiroshi Unno, Yuki Satake, and Tachio Terauchi. 2017. Relatively Complete Refinement Type System for Verification ofHigher-Order Non-Deterministic Programs. Extended version, available from http://www.cs.tsukuba.ac.jp/~uhiro/.
Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi. 2013. Automating relatively complete verification of higher-orderfunctional programs. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’13, Rome, Italy - January 23 - 25, 2013, Roberto Giacobazzi and Radhia Cousot (Eds.). ACM, 75–86. https://doi.org/10.1145/2429069.2429081
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Refinement types for Haskell. In
Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September
1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 269–282. https://doi.org/10.1145/2628136.2628161
Hongwei Xi. 2001. Dependent Types for Program Termination Verification. In 16th Annual IEEE Symposium on Logic in
Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society, 231–242. https://doi.org/10.1109/LICS.2001.932500
He Zhu and Suresh Jagannathan. 2013. Compositional and Lightweight Dependent Type Inference for ML. In Verification,
Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013.
Proceedings (Lecture Notes in Computer Science), Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.), Vol. 7737.
Springer, 295–314. https://doi.org/10.1007/978-3-642-35873-9_19
He Zhu, Aditya V. Nori, and Suresh Jagannathan. 2015. Learning refinement types. In Proceedings of the 20th ACM SIGPLAN
International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, Kathleen
Fisher and John H. Reppy (Eds.). ACM, 400–411. https://doi.org/10.1145/2784731.2784766

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 12. Publication date: January 2018.