A Fixpoint Logic and Dependent Effects for
Temporal Property Verification
Yoji Nanjo

Hiroshi Unno

University of Tsukuba
nanjo@logic.cs.tsukuba.ac.jp

University of Tsukuba / RIKEN AIPuhiro@cs.tsukuba.ac.jp

Eric Koskinen

Tachio Terauchi

Stevens Institute of Technology
eric.koskinen@stevens.edu

Waseda University
terauchi@waseda.jp

Abstract
Existing approaches to temporal verification of higher-order functional programs have either sacrificed compositionality in favorof achieving automation or vice-versa. In this paper we present
a dependent-refinement type & effect system to ensure that welltyped programs satisfy given temporal properties, and also give analgorithmic approach—based on deductive reasoning over a fixpoint
logic—to typing in this system. The first contribution is a novel
type-and-effect system capable of expressing dependent temporal
effects, which are fixpoint logic predicates on event sequences andprogram values, extending beyond the (non-dependent) temporal
effects used in recent proposals. Temporal effects facilitate compositional reasoning whereby the temporal behavior of program parts
are summarized as effects and combined to form those of the larger
parts. As a second contribution, we show that type checking andtypability for the type system can be reduced to solving first-orderfixpoint logic constraints. Finally, we present a novel deductive
system for solving such constraints. The deductive system consistsof rules for reasoning via invariants and well-founded relations,and is able to reduce formulas containing both least and greatest
fixpoints to predicate-based reasoning.
CCS Concepts • Theory of computation → Programming
logic; Program verification; • Software and its engineering→ Formal software verification;
Keywords higher-order programs, temporal verification, fixpoint
logic, dependent temporal effects, dependent refinement types
ACM Reference Format:
Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi. 2018. A
Fixpoint Logic and Dependent Effects for Temporal Property Verification.
In LICS ’18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science,
July 9–12, 2018, Oxford, United Kingdom. ACM, New York, NY, USA, 22 pages.
https://doi.org/10.1145/3209108.3209204

1

Introduction

Recent years have seen many new approaches for verifying temporal properties of higher-order programs. At first, these works were
Permission to make digital or hard copies of all or part of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. 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.
LICS ’18, July 9–12, 2018, Oxford, United Kingdom© 2018 Association for Computing Machinery.
ACM ISBN 978-1-4503-5583-4/18/07. . . $15.00
https://doi.org/10.1145/3209108.3209204

restricted to safety properties [9, 20, 23–25], termination [13, 28],
non-termination [14], or finite data [18]. Algorithmic reductions
based on higher-order recursion schemes [7, 8] and constrainedHorn clause solving [3] have enjoyed automation success. Other
works have shown that the automata-theoretic reduction to fairtermination [27] can be lifted to the higher-order setting [16]. Stillother works have permitted reasoning about angelic-vs-demonic
nondeterminism [26].
Meanwhile there has been a sub-community, whose aim is tosupport temporal specifications directly in the type system, in theform of temporal effects. The promise of this approach is that it may
lead to a more compositional verification strategy, where temporalreasoning can be done locally (at the level of terms, expressions,functions, etc.) and combined together via an orchestrating typesystem to reason about the overall program [4, 12, 21]. These works,
however, required an over-approximation to cope with the effects ofrecursive functions. In particular, the temporal effects in prior work
are simply sets of event traces that coarsely over-approximate theactual temporal behavior of the program terms either via ω-regularsets [4] or else by allowing recursive functions to have any infinite
effect [12]. These treatments preclude specifying value-dependent
temporal properties as effects, and also, for infinite-state programs,
the over-approximation may result in loss of precision even when
the goal property to be verified is non-dependent.
In summary, while recent works have led to advanced noncompositional algorithmic approaches, the state-of-the-art is that
we don’t have a clear theory to connect compositional type &
effect-based approaches with algorithmic verification techniques.
Bridging this gap could mean exploiting the best of both worlds.
In this paper, we bridge this gap, presenting methods for algorithmic verification of temporal properties specified as effects.
Our first step is to raise the bar a little higher. We introduce theconcept of dependent temporal effects. Our types have the form
(τ & (Φ µ , Φν )) where we use dependent-refinement types and, as inprior work [4, 12, 21], the effects are a pair: Φ µ corresponding to
the finite effects and Φν corresponding to the infinite effects. Unlike
prior work, we treat these (finite and infinite) effects of program
expressions as predicates on finite and infinite (respectively) event
sequences–i.e., a predicate on Σ∗ and a predicate on Σω –over somealphabet of events Σ. As discussed below, the predicates are also on
program values, thus making the effects value-dependent. Moreover, we express these predicates in a fixpoint logic that permits
least- and greatest-fixpoints of predicate variables and has basetheories of integers and finite/infinite event sequences. We can
express, for example, that the effect of a function foo n is given by

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchiµthe pair (Φfoo , Φνfoo ) defined as:µΦfoo ≜ λx .⊥4. A deductive proof system that employs invariants and wellfounded relations to solve formulas in the fixpoint logic
containing both least and greatest fixpoints. (Sec. 5)
5. A soundness proof for our deductive rules. (Theorem 5.2)

Φνfoo ≜ λx .x ∈ ((Ready · Sendn ) | Wait)ω

The effect predicate Φ µ specifies that there are no finite effects
whereas Φν specifies that the infinite behavior is to repeatedly
generate either (i) a Ready event and n Send events or (ii) a single
Wait event. Notice, in particular, that n is a parameter to foo, making
this effect dependent with respect to foo’s argument.
Next, we provide dependent temporal effect typing rules, which
relate the effects of one program part to the effects of others, accumulating proof obligations in the form of constraints along the way.
The recursive function definition rule highlights our treatment, as
well as the benefit of treating effects as finite/infinite predicates. In
prior work, over-approximations of effects were used. Here we instead relate the effect Φ of the body of the function e with the effectof the overall recursive function rec(f , xe, e) with two constraints:
a least fixpoint constraint relating finite effects Φ µ to the finite
effects of rec(f , xe, e) and a greatest fixpoint constraint relating theinfinite effects Φν to the infinite effects of rec(f , xe, e). These effects
of recursive functions have the form:µΦfoo = λx .(µX µ (n, x). . . .)(n, x) Φνfoo = λx .(νX ν (n, x). . . .)(n, x)
where X µ and X ν are effect predicate variables (cf. Sec.4.1). Our
treatment of effects as predicates is key to enabling an overall
type system that is able to remain precise, even in the context ofrepresenting infinite behaviors. In our type system, constraints arealso imposed, for example, in instances of subtyping.
The question then remains: how do we solve these constraints?
Addressing this question leads to the next contribution of our work,
which achieves a marriage between type-and-effect-based temporal
specifications [4, 12, 21] and algorithmic verification approaches [8,9, 13, 16, 20, 22–24]. We introduce a deductive system for reasoning
about these fixpoint constraints. The deductive proof rules let us
address least- and greatest-fixpoint constraints that appear in thetyping tree. The rules reduce the fixpoint subformula to reasoning
about invariants and well-founded relations. The use of invariants
and well-founded relations is motivated by their use in safety andliveness verification of infinite state programs (as mentioned above),and enables solving constraints that cannot be solved by a simple
unrolling of the fixpoint formula. Also, from an engineering pointof view, one can leverage existing tools to synthesize invariants
and well-founded relations. The particular strategy we employ
depends on the kind of fixpoint (least or greatest) and whether theyoccur in negative or positive position in the formula. Our deductive
system then has a collection of further approximation rules, definedinductively on the structure of the formula, that further reduce theformulas to predicate-based reasoning.
Contributions. In summary, we make the following contributions:
1. Dependent temporal effects, expressed in a first-order fixpoint logic over theories of integers and finite/infinite event
sequences, wherein those integers can depend on program
values. (Sec. 3)
2. A type system for dependent temporal effects, supporting
programs written in an ML-like language with higher-orderfeatures and ranging over infinite data. (Sec. 4.4)
3. A soundness proof of our type system. (Theorem 4.1)

Organization. In the next section, we give an example and use it tohighlight our main contributions, as well as some further examples
to show the applicability of our work. In Sec. 3 we give our ML-likelanguage and in Sec. 4 we present our type system and associatedsoundness theorem. Our deductive fixpoint proof system is given
in Sec. 5. We conclude with a discussion of related work in Sec. 6.
Omitted materials appear in the extended technical report [17].

2

Overview

We now give a summary of our techniques, using the example
shown in Fig. 1. At the end of this section we provide further
examples (Fig. 2) that illustrate the applicability of our work.
Our type and effect system, extended with dependent temporal
effects can be illustrated with this messenger example. This example
simulates a client interacting with a server. The messenger program
calls until_ready which will make a nondeterministic boolean
choice: in one case it will trigger the event Ready and otherwise
it will Wait and again call until_ready. If the Ready event everoccurs, then until_ready will return, and send_msgs will generate
n instances of Send. Finally, messenger will recur. This program has
no finite traces. Its infinite traces follow the form of the dependentω-regular expression ((Ready · Sendn ) | Wait)ω . Notice that thiseffect depends on the input to the program n. Although this example
is simple, it already illustrates a property that cannot be expressedin prior work [3, 9, 13, 14, 16, 20, 23–26, 28]. In fact, this effectexpression escapes classical LTL or the µ-calculus.
We now discuss how our approach can conclude the above dependent ω-regular expression, highlighting the contributions along
the way. The typings for the recursive procedures in this example
can be found in Fig. 1. (The full type derivation for send_msgs is also
shown, and the type derivation for until_ready is given in [17].)
The overall type for send_msgs is τsend_msgs = (n : {n | n ≥ 0}) →(unit & Φsend_msgs ). We assume that the reader is already familiar
with dependent-refinement types such as above, which states that
send_msgs is a function from non-negative integers to unit, having
effects described by Φsend_msgs . As in prior work [4, 12], effects areµgiven as pairs, i.e., Φsend_msgs = (Φsend_msgs , Φνsend_msgs ) the firstcorresponding to the finite effects of send_msgs and the latter tothe infinite effects.
In this paper, we introduce dependent temporal effects. To thisend, we begin by treating each component’s effect as predicates. For
send_msgs, we have:µΦsend_msgs =Φνsend_msgs =λx .(µX µ (n, x).(n = 0 ∧ x = ϵ∨n , 0 ∧ ∃y.x = Send · y ∧ X µ (n − 1, y)))(n, x)
λx .(νX ν (n, x).
n , 0 ∧ ∃y.x = Send · y ∧ X ν (n − 1, y))(n, x)

As discussed later, our type system is able to derive this judgmentµfrom the syntax of the program. The first component Φsend_msgs_
describes the effects of the finite traces of send msgs via a predicate
λx ._ where x will be a candidate event sequence. The body is a least
fixpoint equation over a predicate variable X µ , parameterized byvariables n and x. The fixpoint’s body has two cases: when n = 0,then the event sequence is simply empty, denoted ϵ. Otherwise,A Fixpoint Logic and Dependent Effects for
Temporal Property Verification(a) Source Codelet rec until_ready () =if * then(event[Ready]; ())
else(event[Wait];
until_ready ())
let rec send_msgs n =if n = 0 then ()else(event[Send];
send_msgs (n-1))
let rec messenger n =until_ready ();LICS ’18, July 9–12, 2018, Oxford, United Kingdom(b) Typing Rules and Final Effect Approximations
Types= unit → (unit & Φuntil_ready )= λx .(µX µ (x).x = Ready ∨ ∃y.x = Wait · y ∧ X µ (y))(x)= λx .(νX ν (x).∃y.x = Wait · y ∧ X ν (y))(x)= (n : {n | n ≥ 0}) → (unit & Φsend_msgs )= λx .(µX µ (n, x). n = 0 ∧ x = ϵ ∨ n , 0 ∧ ∃y.x = Send · y ∧ X µ (n − 1, y) )(n, x)= λx .(νX ν (n, x).n , 0 ∧ ∃y.x = Send · y ∧ X ν (n − 1, y))(n, x)= (n : {n | n ≥ 0}) → (unit & Φmessenger )′′µ= λx .(µX µ (n, x).∃y1 , y2 .x = y1 · y2 ∧ (Φuntil_ready · Φsend_msgs ) (y 1 ) ∧ X µ (n, y 2 ))(n, x)′′ν© (Φuntil_ready · Φsend_msgs ) (x)∨ª®)(n, x)Φνmessenger = λx .(νX ν (n, x).­­ ∃y1 , y2 .x = y1 · y2 ∧®
′′µ(Φuntil_ready · Φsend_msgs ) (y1 ) ∧ X ν (n, y2 )«¬Final Effect Approximations
τuntil_readyµΦuntil_readyνΦuntil_readyτsend_msgsµ
Φsend_msgs
νΦsend_msgs
τmessengerµΦmessenger′
Φuntil_ready
′
Φsend
_msgs
′
Φmessenger

send_msgs n;
messenger n= (λx .x ∈ Wait∗ · Ready, λx .x ∈ Waitω )= (λx .x ∈ Sendn , λx .⊥)= (λx .⊥, λx .x ∈ (Ready · Sendn | Wait)ω )(c) Type Derivation Tree for send_msgs, including Deductive Fixpoint Rules (⊩)
..
..
.
.
send_msgs : τ , n = 0 ⊢ () : σif send_msgs : τ , n > 0 ⊢ ev[Send]; send_msgs (n − 1) : σif
send_msgs : τ , n ≥ 0 ⊢n≥0⊢

if n = 0 then ()else (ev[Send]; send_msgs (n − 1))

: σif

A
B

(unit & Φsend_msgs )′<:(unit & Φsend_msgs )..
.

⊢ rec(send_msgs, n, · · · ) : (n : n ≥ 0) → (unit & Φsend_msgs )′⊢ rec(send_msgs, n, · · · ) : (n : n ≥ 0) → (unit & Φsend_msgs )τ ≜ (n : n ≥ 0) → (unit & (λx .X µ (n, x), λx .X ν (n, x)))σif ≜ (unit & (λx .n = 0 ∧ x = ϵ ∨ n , 0 ∧ ∃y.x = Send · y ∧ X µ (n − 1, y), λx .∃y.x = Send · y ∧ X ν (n − 1, y)))|= n ≥ 0 ⇒ (x ∈ Sendn ⇒ x ∈ Sendn )A:|= (n = 0 ∧ x = ϵ ∨ ∃y.x = Send · y ∧ y ∈ Sendn−1 ) ⇒ x ∈ Sendnµ′µ⊩ n ≥ 0 ⇒ (x ∈ Sendn ⇒ x ∈ Sendn )⊩ n ≥ 0 ⇒ (Φsend_msgs (x) ⇒ Φ send_msgs (x))|=|= (p1 (n, x) ∧ n , 0 ∧ x , Send · x ′ ) ⇒ ¬(x = Send · x ′ )X ν (n, x); p1 ; p2 ; n , 0 ∧ x , Send · x ′ ↑ x = Send · x ′(p1 (n, x) ∧ n , 0 ∧ x = Send · x ′ )⇒ (p1 (n − 1, x ′ ) ∧ p2 (n, x, n − 1, x ′ ))X ν (n, x); p1 ; p2 ; n , 0 ∧ x = Send · x ′ ↑ X ν (n − 1, x ′ )|= (p1 (n, x) ∧ n = 0) ⇒ ¬(n , 0)X ν (n, x); p1 ; p2 ; n , 0 ↑ x = Send · x ′ ∧ X ν (n − 1, x ′ )X ν (n, x); p1 ; p2 ; n = 0 ↑ n , 0

X ν (n, x); p1 ; p2 ; n , 0 ↑ ∃y.x = Send · y ∧ X ν (n − 1, y)X ν (n, x); p1 ; p2 ; ⊤ ↑ n , 0 ∧ ∃y.x = Send · y ∧ X ν (n − 1, y)

B:|= n ≥ 0 ⇒ (¬(n ≥ 0) ⇒ ⊥)⊩ n ≥ 0 ⇒ (¬(n ≥ 0) ⇒ ⊥)⊩ n ≥ 0 ⇒ (Φνsend_msgs (x) ⇒ Φ ′νsend_msgs (x))
p1 ≜ λ(n, x).n ≥ 0

p2 ≜ λ(n 1 , x 1 , n 2 , x 2 ).n 1 > n 2 ≥ 0

Figure 1. Clockwise: (a) Source code for messenger; (b) Types & effects for recursive functions along with our final effect conclusions; and(c) type derivation for send_msgs, including the use of our deductive proof rules (⊩) in subtrees A and B.
the predicate specifies that x will be the Send event, followed bysome event sequence y and that X µ (n − 1, y) must hold. Overall,this fixpoint is applied to variables n and x.
The second component Φνsend_msgs describes the infinite effects
of send_msgs. Not surprisingly, a greatest fixpoint equation is used,with predicate variable X ν again parameterized by n and x. The
n = 0 case is finite and not possible. We will see momentarily thatthe other infinite case is also not possible.

LICS ’18, July 9–12, 2018, Oxford, United Kingdom

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi

Amortized Complexity
let rev l =Higher-Order

Web Server Fairness

let rec zoom () =let rec aux l acc = match l with

let rec listener npool pend =event[Zoom]; zoom ()if * && pend < npool then| [] -> acc | h::t ->(event[Accept];

event[Tick]; aux t (h::acc)

let rec shrink t f d =in aux l []let is_empty (l1,l2) = l1 = [] && l2 = []if f () <= 0 thenlet enqueue e (l1,l2) = event[Enq];(l1,e::l2)

else

let rec dequeue (l1,l2) = match l1 withlistener npool (pend + 1))
else if pend > 0 then(event[Handle];

zoom ()

listener npool (pend - 1))
else(event[Shrink];| [] -> dequeue (rev l2, [])let t' = f() - d in(event[Wait];| e::l1' -> event[Deq]; (e, (l1', l2))

shrink t' (fun x -> t') d)listener npool pend)

let rec main (l1,l2) =if * then main (enqueue 42 (l1,l2))
else if is_empty (l1,l2) then ()let server npool =let shrinker t d =listener npool 0

shrink t (fun x -> t) delse main (snd (dequeue (l1,l2)))
main : ((l1, l2) : int list × int list) → (unit & Φ)
Φ µ = λx .# (x) + |l2| = #(x) = # (x) − |l1|EnqΦν = λx .⊤

Tick

Deq

shrinker : (t : {t | t ≥ 0}) →(d : {d | d > 0 ∧ t mod d = 0}) →(unit & Φ)
Φ µ = λx .⊥Φν = λx .x ∈ Shrinkt /d · Zoomω

: (npool : {ν | ν ≥ 0}) →(unit & (λx .⊥, λx .ϕ))x ∈ (Σ∗ · (Σ \ Accept)npool+1 )ω
ϕ=⇒ x ∈ (Σ∗ · Wait)ω
serverFigure 2. Further examples of programs and corresponding dependent temporal effects that we are able to verify using our approach.
Our typing judgments impose proof obligations in the form of
constraints. Most notably, the type rule for recursive function definition (cf. T-Fun in Sec. 4) for a function f requires that the effectof a total application of f be compatible with the effect of the
body of f , which is itself derived from the typing rules. Roughly,
T-Fun works as follows. First, it checks that the body of f has
finite/infinite effect pair (Φ µ , Φν ), under a typing environment
where a total application of f has some finite/infinite effect pair(λx ∈ Σ∗ .X µ (ex , x), λx ∈ Σω .X ν (ex , x)). X µ and X ν are finite and infinite predicate variables, respectively. Given this, the effect of a total
application of the recursive function is then the effect pair (λx ∈Σ∗ .q µ (ex , x), λx ∈ Σω .qν (ex , x)) where our type system requires thatq µ = µX µ (ex , x).Φ µ (x) and qν = νX ν (ex , x).[q µ /X µ ]Φ µ (x). In thisway, we require that the finite (resp., infinite) effects of the recursivefunction be given by a least (resp., greatest) fixpoint over a predicate
variable X µ (resp., X ν ). The type system also generates constraints
in other rules, such as the subtyping rules (S-Qual, etc.) of the form
(τ1 & Φ1 ) <: (τ2 & Φ2 ). In these cases, the type system requires thatµ
the finite (resp., infinite) effects Φ1 (resp., Φν1 ) is approximated byµ
the finite (resp., infinite) effects Φ2 (resp., Φν2 ).
Addressing the recursive function rule in the type soundness
proof is a challenge due to the infinite effects. We use a semantics of types and an infinite sequence of approximations for therecursive function and its infinite effect. This infinite sequence ofapproximations is used to construct the greatest fixpoint.
The types for messenger are given in the second column of Fig. 1.
Let us consider the send_msgs recursive function, whose overall
type is given by the dependent-refinement type τsend_msgs , that
constrains input n to be greater than or equal to 0. The overall effectµΦsend_msgs has two parts: the finite effect Φsend_msgs and the infiniteνeffect Φsend_msgs . These effect predicates involve predicate variables
X µ and X ν , quantified with a least and greatest fixpoint, respectively.
Notice that X µ and X ν are parameterized by n, which is a program
variable: the input to messenger. This highlights our support for

dependent temporal effects, showing how they are treated intimately
with the fixpoint constraints on recursive functions.
Solving Fixpoints via Our Deductive Proof Rules. The deductive rules enable us to conclude the final effects:′
Φuntil_ready
′
Φsend
_msgs
′
Φmessenger= (λx .x ∈ Wait∗ · Ready, λx .x ∈ Waitω )= (λx .x ∈ Sendn , λx .⊥)= (λx .⊥, λx .x ∈ (Ready · Sendn | Wait)ω )Intuitively, until_ready has finite behaviors that repeat Wait finitely
many times followed by Ready. The infinite behaviors of until_readyare infinite repetition of Wait. send_msgs has only finite behaviors,
specifically, repetition of Send n times, where n is the input tothe overall program messenger. Finally, messenger has only infinite effects, that arises from a combination of the other two functions. Notice that our approach follows the classical compositional
spirit of type systems: conclusions about terms are derived independently and then combined together to construct conclusions
about compound terms. Similarly, our conclusion about the dependent temporal effects of method messenger is constructed after wehave reached conclusions about the effects of its callees (including
approximations of these callees).
So, how do we come to these final approximations of all functions? Our sub-typing rules (cf. Fig. 7 in Sec. 4) allow us to introduce
an approximation effect predicate Φ ′ of effect predicate Φ provided
that we can show that ∀x .Φ ′ (x) ⇒ Φ(x). For send_msgs, the subtyping appears in Fig. 1, with premises A and B.
Our deductive system comprises rules for reasoning about theseformulas that contained least- and greatest- fixpoint formulas buried
within them. The key idea is to reduce these tricky subformulas toinvariants and well-founded relations, both described as predicates,
and then symbolically manipulate the side-conditions that arise
until they can be handled by base solvers. The process begins with
one of four main rules, under- or over-approximate (as the casemay be) least and greatest fixpoints, depending on whether theyA Fixpoint Logic and Dependent Effects for
Temporal Property Verification
appear in a negative or positive position in the fixpoint formula.
We’ll now look at how two of the rules can be used for the example.
First, looking at the finite effects of send_msgs, our rules allow usµ
to show, for example, that λx .x ∈ Sendn approximates Φsend_msgs
by using invariant predicates that over-approximate the least fixpoints. This can be seen in the deductive proof rule in subtree
A. We have a formula, where the least fixpoint occurs in a negaµ
tive position, i.e., inside Φsend_msgs . Our proof rule (Fp-Lfp− ) lets
us approximate this buried least fixpoint with λ(n, x).x ∈ Sendn
by using the pre-fixpoint. In the first premise of the rule, we consider only the fixpoint and must show that when we substituteλ(n, x).x ∈ Sendn into the fixpoint formula, the result is approximated by λ(n, x).x ∈ Sendn . In the second premise, we use thisinformation, eliminating the fixpoint.
Next, looking at the infinite effects of send_msgs, our proof
system lets us show that the goal effect approximation λx .⊥ ofΦνsend_msgs holds. This is done by, first, over-approximating thegreatest fixpoint subformula that occurs in a negative position using a predicate and a well-foundedness check. Note that the typing
judgments accumulate the invariant that n ≥ 0, and that it is incorporated into the deductive proof rule in subtree B. The rule
(Fp-Gfp− ) lets us replace the GFP formula (νX (ex ).ψ )(et ) by somepredicate ¬p1 (et ). There is a side condition, however, that we mustalso provide a relational well-foundedness predicate p2 which witnesses that ¬p1 over-approximates νX (ex ).⊤ ∧ ψ . In the send_msgs
example, we use the predicate ¬(n ≥ 0) to approximate the GFP
formula in Φνsend_msgs . What remains is the side-condition, where
we use p2 = n 1 > n 2 ≥ 0 to witness that ¬p1 over-approximatesn , 0 ∧ ∃y.x = Send · y ∧ X ν (n − 1, y).
We treat this side-condition of witnessing predicates’ approximations itself as a judgment (denoted X (ex ); p1 ; p2 ; ⊤ ↑ ψ ) as well as
an analogous least-fixpoint judgment (denoted X (ex ); p1 ; p2 ; ⊥ ↓ ψ )in another series of proof rules. These rules are inductively definedover ψ , letting us discharge this obligation syntactically down topredicate reasoning, as can be seen in the rest of proof subtree B.
Specifically, we use a rule for conjunction (Apxν -∧), existential
quantification (Apxν -∃), and then conjunction again. Each rulehas premises for each sub-formula(e) and predicate-oriented side
conditions. We will discuss these rules in Sec. 5.
Other Examples & Applications. The messenger example is intended to be a small example that highlights some of the main
aspects of our work. In Fig. 2 we provide the source code and effectbased temporal properties for more examples, demonstrating theapplicability of our approach. (The types for these examples are
given in [17].) We now discuss each program.
Amortized Complexity. This example involves functions that manipulate a pair of integer lists. The main loop will nondeterministically enqueue a new integer, via enqueue which adds the element to
the l2 list. If main finds that the list is empty, it terminates. Otherwise, it iterates, but only after applying dequeue to the list. dequeue
shuffles elements between l1 and l2: if l1 is empty, it moves everything from l2 to l1 and, otherwise, it dequeues by returning a pairof the dequeued item and the new queue (l1’,l2). Here, #a(x) is
the number of a’s in x. The temporal effect Φ of main asserts that,when the program terminates, the number of enqueues plus thelength of l2 is equal to the number of dequeues minus the lengthof l1, which is equal to the number of Tick’s.

LICS ’18, July 9–12, 2018, Oxford, United Kingdom(events) a ::∈ Σ(expressions) e ::= x | n | v 1 op v 2 | rec(f , xe, e) | v 1 v 2 | ev[a]| ifz v then e 1 else e 2 | let x = e 1 in e 2(values) v ::= x | n | rec(f , xe, e) ve(where |ev | < |ex |)(simple types) T ::= int | T1 → T2
Figure 3. Syntax of L
Higher-Order Functions. The second example shrinker contains
a higher-order function shrink. The example is adopted from asimilar example in [12]. Here, shrink takes an argument f which
is a function from unit to int, and an integer argument d. Then, it
recursively calls itself by passing a function that returns d less than
the given function, until f returns a non-positive value. Here, t isa ghost parameter that is used to represent sufficient information
about the passed function (see., e.g., [25]). The effect Φ asserts thatshrinker never terminates, and its infinite executions emit theevent sequences Shrinkt/d · Zoomω . That is, shrink is called t/dtimes, followed by infinitely many calls to zoom.
Server Fairness/Liveness. The function listener in this example
simulates a non-terminating loop within, e.g., a web server, thatawaits new incoming connections (Wait), accepts them (Accept)
and dispatches them to an appropriate handler (Handle). Argument
pend is the number of clients that have been accepted but not yet
dispatched and argument npool is an upper bound on the amountof clients that can be accepted but yet undispatched at a given time.
The use of * indicates a non-deterministic boolean choice.
One critical property is that every accepted connection is eventually handled, i.e., that the pool of pending clients eventually
becomes empty. This is, however, not true in general since infinitely many new clients may preempt handling pending clients. The
property must be instead weakened to include a fairness constraintthat all infinite event streams satisfy (Σ∗ · (Σ \ {Accept})npool+1 )ω ,i.e., that there will always eventually be a time when new connections won’t be accepted for npool + 1 steps. (Technically, this does
ensure that the pool of clients always eventually becomes empty,
even though less than npool + 1 steps may be needed.)
These examples demonstrate an interesting connection of our
method and works that have been focused on resource analysis andcost semantics. One way of thinking about the execution time ofa program is by considering the events generated by the program(as we discuss in Sec. 3, we require programs not to have infinite
event-less executions). Our dependent temporal effects are capableof expressing specifications of programs that limit the number of
events that could possibly be generated, a phenomenon that corresponds to an upper bound on computation time. We believe that
there is interesting future work to be explored at the intersectionof these two research tracks.

3

Target Language

The syntax of an ML-like (i.e., typed, higher-order, and call-byvalue) functional language L is shown in Fig. 3. Here, n, x, and a aremeta-variables ranging respectively over integers, term variables,and events. Σ represents a finite set of events. We write xe for a
finite sequence of variables and |e
x | for the length of xe. We also
write ϵ for the empty sequence. We use a meta-variable ϖ (resp.

LICS ’18, July 9–12, 2018, Oxford, United Kingdom(formulas) ϕ ::= ⊤ | ⊥ | A(et ) | ¬ϕ | ϕ 1 ∧ ϕ 2 | ϕ 1 ∨ ϕ 2| ϕ 1 ⇒ ϕ 2 | ∀x ∈ S.ϕ | ∃x ∈ S.ϕ | X (e
t)
e
e
e
e
| (µX (ex : S).ϕ)(t ) | (νX (ex : S).ϕ)(t)
e(terms) t ::= x | f (et)(predicates) p ::= λex ∈ S.ϕ(sorts) S ::∈ {Z, Σ∗ , Σω }Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi(effects) Φ ::= (λx ∈ Σ∗ .ϕ µ , λx ∈ Σω .ϕν )(effect qualified types) σ ::= (τ & Φ)
(dependent refinement types) τ ::= {x | ϕ} | (x : τ ) → σ(type environments) Γ ::= ∅ | Γ, x : τ
Figure 5. Syntax of types and effects

Figure 4. Syntax of fixpoint logic
4.2π ) to represent a finite (rep. infinite) sequence of events. We write
ϖ · π (resp. ϖ · ϖ ′ ) for the concatenation of the finite ϖ and theinfinite π (resp. finite ϖ ′ ) sequences. op represents binary integer
operators such as +, −, ×, =, and <. We assume that boolean andunit values are encoded as integers (e.g., true = 0 and false = 1).
We assume that expressions are simply-typed. An expression
ev[a] raises the event a. An expression ifzv then e 1 else e 2 reduces
to e 1 if v = 0 and e 2 otherwise. We abbreviate let x = e 1 in e 2 as e 1 ; e 2
if x does not occur in e 2 . An expression rec(f , xe, e) represents a(possibly recursive) function f with the arguments xe (where |ex | ≥ 1)and the body e. We assume that rec(f , xe, e) is productive: if a runof the function is non-terminating, it exhibits an infinite sequenceof events. The assumption can be easily enforced by inserting adummy event command in the beginning of each function definition.
Note that, for simplicity, we omit non-deterministic choice ∗ andalgebraic data structures such as lists, which are used in our running
examples, from the language L. It is easy to extend our type system
in Sec. 4 with these features (see, e.g., [24, 26]).
The operational semantics of L is defined by the set of inductive
and coinductive rules for deriving judgments of the form e ⇓ v & ϖ
and e ⇑ ⊥ & π . The former is for terminating evaluations and meansthat the evaluation of e terminates with the final result value v
producing the finite sequence of events ϖ. The latter is for nonterminating evaluations and means that the evaluation of e diverges
producing the infinite sequence of events π . The rules are analogous
to the ones from [12] and deferred to the extended report [17].

4Type System

4.1

First-Order Fixpoint Logic

The types in our dependent-refinement type system embed predicates in the first-order fixpoint logic over integers and finite andinfinite event sequences. Fig. 4 shows the syntax. Meta-variable X
represents predicate variables. A(et ) represents atomic formulas suchas the equality on integers and sequences. f represents constants
such as integers n, the empty sequence ϵ, and singleton sequences aas well as functions such as the sequence concatenation and integer
arithmetic operators. We write ⊤ and ⊥ respectively for tautologye ).ϕ (resp. νX (ee ).ϕ) repand contradiction. The formula µX (e
x: T
x: T
resents the least (resp. greatest) fixpoint (of the function λX .λex∈e .ϕ). We assume that X in µX (ee ).ϕ and νX (ee ).ϕ occurs
T
x: T
x: T
only positively in ϕ. We sometimes omit sorts when they are obvious from the context. We define (λex .ϕ)(et ) ≜ [et /ex ]ϕ and write
p1 ⊑ p2 if ∀e
x .p1 (ex ) ⇒ p2 (ex ) holds. We also write ¬λex .ϕ for λex .¬ϕ.
We write |= ϕ if ϕ is valid. We define the formal semantics of thisfirst-order fixpoint formulas in [17]. We write fv(ϕ) (resp. fpv(ϕ))
for the set of free term (resp. predicate) variables in ϕ. We also
define fv(λx .ϕ) ≜ fv(ϕ) \ {x } and fpv(λx .ϕ) ≜ fpv(ϕ).

Syntax of Types and Effects

The syntax of types and effects is shown in Fig. 5. An effect Φ is a pairof predicates λx ∈ Σ∗ .ϕ µ and λx ∈ Σω .ϕν , which may contain freeterm and predicate variables. We write Φ µ (resp. Φν ) for λx ∈ Σ∗ .ϕ µ(resp. λx ∈ Σω .ϕν ). Φ µ specifies a set of valid finite event sequences
for terminating runs. On the other hand, Φν specifies a set of valid
infinite event sequences for non-terminating runs. We define theconcatenation Φ1 · Φ2 of effects Φ1 and Φ2 as follows.1µµ(λx ∈ Σ∗ .∃x 1 , x 2 ∈ Σ∗ .x = x 1 · x 2 ∧ Φ1 (x 1 ) ∧ Φ2 (x 2 ),µ

λx ∈ Σω .Φν1 (x) ∨ (∃y ∈ Σ∗ , z ∈ Σω .x = y · z ∧ Φ1 (y) ∧ Φν2 (z)))
We also define a special effect Φval ≜ (λx ∈ Σ∗ .x = ϵ, λx ∈ Σω .⊥).
Note that Φval is an identity with respect to ·, that is, Φval · Φ =Φ · Φval = Φ for any Φ. We often abbreviate (τ & Φval ) as τ .
An effect qualified type is of the form (τ & Φ) where τ is a dependent refinement type (described below) and Φ is an effect. Roughly,
the qualified type (τ & Φ) is the type of expressions e such that, 1.)
for all terminating run e ⇓ v & ϖ, v conforms to the type τ and ϖsatisfies Φ µ , and 2.) for all non-terminating run e ⇑ ⊥ & π , ϖ satisfiesΦν . Sec. 4.3 formally defines the semantics of the qualified types.2
An integer refinement type {x | ϕ} is the type of integers x thatsatisfy the formula ϕ. We often abbreviate {x | ⊤} as int. A dependent function type (x : τ ) → σ is the type of functions that take anargument x of the type τ and behave according to the return type σ .
Note that the scope of x is within σ , and hence effects in σ can depend on the argument x. For example, ((x : int) → (int & Φ1 ) & Φ2 )is the type of expressions that exhibit event sequences conforming
to Φ2 when evaluated, and cause event sequences conforming to Φ1
when applied to some integer argument x. We write (ex: eτ ) → (τ &Φ)for (x 1 : τ1 ) → ((x 2 : τ2 ) → (· · · (x n : τn ) → (τ &Φ) · · ·&Φval )&Φval ),that is, the latent effect of partially applying the function is Φval .
Note that a type of such a form can be given to a recursive function rec(f , xe, e) where |ex | = |e
τ | as partial applications to f (i.e.,
applying less than |ex | many arguments) do not raise any events.
We abbreviate (x : τ ) → σ as τ → σ when x does not occur in σ .
A type environment Γ is a sequence of variable bindings x : τ .
We define Γ(x) ≜ τ if x : τ ∈ Γ. We abbreviate Γ, ν : {ν | ϕ} as Γ, ϕif ν < fv(ϕ) and ν never occurs elsewhere. Note that type bindings
in type environments and arguments of function types are of theform (x : τ ) instead of (x : σ ). This is because the target language
L is call-by-value, and hence variables are always bound to values
whose evaluation never exhibits temporal effects.
We define auxiliary functions sty(σ ), fv(σ ), and fpv(σ ). sty(σ )represents the simple type corresponding to the qualified type σ .
fv(σ ) (resp. fpv(σ )) represents the set of free term (resp. predicate)
1 Note that this generalizes the concatenation of non-dependent temporal effects fromprevious works [4, 12].
2 Readers familiar with type and effect systems may find the qualified type notation
atypical. We use the notation to simplify the presentation: for example, subtyping andsubeffecting can be defined at once.

A Fixpoint Logic and Dependent Effects for
Temporal Property VerificationJΓ ⊢ σ K ≜ {e | ∀θ ∈ sty(Γ).(θ |= Γ) ⇒ θ (e) ∈ Jθ (σ )K}(∀ϖ, w.(e ⇓ w & ϖ) ⇒






(w ∈ Jτ K) ∧ (|= Φ µ (ϖ))) ∧J(τ & Φ)K ≜ e ∈ sty(τ )(∀π .(e ⇑ ⊥ & π ) ⇒ (|= Φν (π ))) 
J{x | ϕ}K ≜ {n | |= [n/x]ϕ}J(x : τ ) → σ K ≜ {w ∈ sty(τ → σ ) | ∀w ′ ∈ Jτ K.w w ′ ∈ J[w ′ /x]σ K}
Figure 6. Semantic typing

variables that occur in σ . The definitions are standard and deferredto the extended report [17]. We extend the notions to type environments and define sty(Γ), fv(Γ), and fpv(Γ) in the obvious way.
We remark that our type and effects are essentially the extension of the types from the previous work on dependent-refinement
type systems [12, 20, 23, 24, 28, 30] with dependent temporal effects which are first-order fixpoint logic predicates on program
values and (finite and infinite) event sequences. Note that, as in
the previous work, the dependent types are restricted to facilitate(semi-)automated reasoning via modern SMT and constraint solving techniques. Namely, the types can only depend on non-functionand effect-free terms.
4.3

Semantic Typing

To formalize the type soundness theorem (cf. Theorem 4.1), we
define the semantics of qualified types. Fig. 6 defines the semantics. Here, w is a meta-variable ranging over closed values (i.e.,
fv(w) = ∅). We write e ∈ T if the expression e has the simple
type T . Similarly, we write w ∈ T if the closed value w has thetype T . We write θ ∈ E for a simple type environment E and aclosed value substitution θ if dom(θ ) = dom(E) and θ (x) ∈ E(x)for any x ∈ dom(E). Also, we write θ |= Γ if dom(θ ) = dom(Γ) and∀(x : τ ) ∈ Γ.θ (x) ∈ Jθ (τ )K hold.
Note that JΓ ⊢ σ K denotes the set of open expressions that behave
according to σ under an environment conforming to Γ. Similarly,
Jσ K (resp. Jτ K) denotes the set of closed expressions (resp. values)that behave according to σ (resp. τ ). For instance, for τ = (x : {u |u ≥ 0}) → ({ν | ν > x } & Φ) where Φ = (λz ∈ Σ∗ .z ∈ ax , λz ∈Σω .⊥), Jτ K are the set of closed functions from integers to integers
which, when given a non-negative integer x as the argument, raises
the event a x many times and returns an integer greater than x.
We also define the semantics of subtyping relation as follows,which says when a (qualified) type is a subtype of another in thegiven type environment.
JΓ ⊢ σ1 <: σ2 K ≜ ∀θ ∈ sty(Γ).(θ |= Γ) ⇒ Jθ (σ1 )K ⊆ Jθ (σ2 )KJΓ ⊢ τ1 <: τ2 K ≜ ∀θ ∈ sty(Γ).(θ |= Γ) ⇒ Jθ (τ1 )K ⊆ Jθ (τ2 )K

Sec. 4.4 shows the rules for deriving subtyping judgments.
4.4

Typing Rules

Fig. 7 shows the typing rules. The rules derive judgments of theform Γ ⊢ e : σ , saying that e behaves according to σ under a value
environment conforming to Γ.
We describe the typing rules. The rules T-Const for typing integer constants, T-VInt for typing integer-type term variables, andT-VFun for typing function-type variables, T-Op for typing integer

LICS ’18, July 9–12, 2018, Oxford, United KingdomΓ ⊢ n : ({x | x = n} & Φval )sty(Γ(x)) = int
T-VIntΓ ⊢ x : ({u | u = x } & Φval )T-Conststy(Γ(x)) , int
T-VFunΓ ⊢ x : (Γ(x) & Φval )x < fv(τ2 ) ∪ fv(Φ2 ) Γ ⊢ e 1 : (τ1 & Φ1 ) Γ, x : τ1 ⊢ e 2 : (τ2 & Φ2 )T-Let
Γ ⊢ let x = e 1 in e 2 : (τ2 & Φ1 · Φ2 )
Γ ⊢ v 1 : ((x : τ ) → (τ ′ & Φ) & Φval ) Γ ⊢ v 2 : (τ & Φval )T-AppΓ ⊢ v 1 v 2 : [v 2 /x](τ ′ & Φ)Γ ⊢ v 1 : (int & Φval ) Γ ⊢ v 2 : (int & Φval )T-OpΓ ⊢ v 1 op v 2 : ({x | x = v 1 op v 2 } & Φval )Γ, v = 0 ⊢ e 1 : σ Γ, v , 0 ⊢ e 2 : σT-IfΓ ⊢ ifz v then e 1 else e 2 : σ
Φ = (λx ∈ Σ∗ .x = a, λx ∈ Σω .⊥)Γ ⊢ ev[a] : ({x | x = 0} & Φ)

T-Event

τf′ = (ex: eτ ) → (τ & (λx ∈ Σ∗ .X µ (ex , x), λx ∈ Σω .X ν (ex , x)))′
Γ, f : τf , xe : eτ ⊢ e : (τ & Φ)q µ = µX µ (ex , x).Φ µ (x) qν = νX ν (ex , x).[q µ /X µ ]Φν (x)τf = (ex: eτ ) → (τ & (λx ∈ Σ∗ .q µ (ex , x), λx ∈ Σω .qν (ex , x)))
Γ ⊢ rec(f , xe, e) : (τf & Φval )T-Fun⊩ ⌊Γ ⊢ ϕ 1 ⇒ ϕ 2 ⌋Γ ⊢ e : σ1 Γ ⊢ σ1 <: σ2
S-Int
T-Sub
Γ ⊢ e : σ2Γ ⊢ {u | ϕ 1 } <: {u | ϕ 2 }µΓ ⊢ τ1 <: τ2µ⊩ ⌊Γ ⊢ ∀x ∈ Σ∗ .Φ1 (x) ⇒ Φ2 (x)⌋⊩ ⌊Γ ⊢ ∀x ∈ Σω .Φν1 (x) ⇒ Φν2 (x)⌋Γ ⊢ (τ1 & Φ1 ) <: (τ2 & Φ2 )S-QualΓ ⊢ τ2 <: τ1 Γ, x : τ2 ⊢ σ1 <: σ2S-FunΓ ⊢ (x : τ1 ) → σ1 <: (x : τ2 ) → σ2
Figure 7. Typing and subtyping rules

operations, T-If for typing conditional branches are straightforward extension of those from the previous work on dependentrefinement type systems [12, 20, 23, 24]. Note that Φval is assigned
as the effect of the expression in T-Const, T-VInt, T-VFun, and TOp because these expressions always terminate and raise no events.
T-Fun types recursive function definitions. As described in Sec. 2,
the main idea here is to introduce predicate variables X µ and X νrespectively representing the finite and infinite effects of the recursive function f being typed. Then, the rule types the body ofthe function, e, under the environment that f has these temporal
effects (expressed by the binding f : τf′ ), to obtain the qualified
type (τ & (Φ µ , Φν )). Then, the latent effect of the function can beobtained by, for the finite part, taking the least fixpoint of Φ µ (i.e.,q µ = µX µ (ex , x).Φ µ (x)), and the greatest fixpoint for the infinite
part using the least fixpoint solution for X µ appearing in the formula (i.e., νX ν (ex , x).[q µ /X µ ]Φν (x)). The rule adopts the one from
[4] and extend it to dependent type and effects.
The rule T-Let for typing let expressions extends a similar rulefrom the previous work [4, 12]. Note that concatenation is used
to obtain the effect of the expression in the conclusion, correctly

LICS ’18, July 9–12, 2018, Oxford, United Kingdom
accounting for the fact that the possible event traces of the expression are the concatenation of those of e 1 and e 2 . T-App types
function applications, and is a straightforward extension of thosefrom the previous work on dependent-refinement type systems
and (non-dependent) type-and-effect systems. As in a standard
type-and-effect system, the latent effect of the function, Φ, becomesthe effect of the function application. Note here that the variable
x may occur in the latent effect, which is substituted by v 2 in the
conclusion to account for the dependency. T-Event types event
raising operations and is self-explanatory. Finally, T-Sub is the
subsumption rule.
Fig. 7 also shows the rules for deriving subtyping judgments.
There, auxiliary functions ⌊Γ⌋ and ⌊Γ ⊢ ϕ⌋ are defined by:⌊∅⌋ ≜ ⊤
⌊Γ, x : {y | ϕ}⌋ ≜ ⌊Γ⌋ ∧ [x/y]ϕ⌊Γ ⊢ ϕ⌋ ≜ ⌊Γ⌋ ⇒ ϕ⌊Γ, x : (y : τ ) → σ ⌋ ≜ ⌊Γ⌋The rules S-Int and S-Fun for subtyping refinement integer types
and dependent function types are equivalent to those from theprevious work on dependent-refinement type systems. The rule
S-Qual is for subtyping effect qualified types. It asserts that thetype part of the qualified types τ1 and τ2 are in the subtyping
relationship. Further, it checks that the left effect Φ1 is a subeffect of
the right effect Φ2 . The subeffecting relation checks that the finite(resp. infinite) part of Φ1 logically implies the finite (resp. infinite)part of Φ2 , under the assertions implied by the type environment Γ.
For example, in the typing of messenger from Sec. 2, a subtyping′
judgment Γ ⊢ (τ & Φsend_msgs ) <: (int & Φsend_msgs ) is discharged
where Γ = n : {x | x ≥ 0}, τ is the refinement integer type′obtained for send_msgs n, and Φsend_msgs and Φsend_msgs are from
Fig. 1. S-Qual checks the subtyping by asserting the validity of n ≥µµ0 ⇒ ∀x ∈ Σ∗ .Φsend_msgs (x) ⇒ Φ ′ send_msgs (x) and n ≥ 0 ⇒ ∀x ∈
Σ∗ .Φνsend_msgs (x) ⇒ Φ ′νsend_msgs (x). Sec. 5 shows the deductive
system for solving such predicate fixpoint logic constraints.
We show that the type system is sound, that is, the judgments
derived by the typing rules respect the semantics. We define predicate substitution ρ to be a finite map from predicate variables toclosed predicates.
Theorem 4.1. If Γ ⊢ e : σ , then e ∈ Jρ(Γ) ⊢ ρ(σ )K for any predicate
substitution ρ with dom(ρ) = fpv(Γ) ∪ fpv(σ ).
We remark that the soundness holds for any background firstorder theory supporting basic integer arithmetic (i.e., those in L)
and concatenations of finite and infinite string over a finite alphabet.
Hence, our system can reap the benefits of recent advances in
automated deduction for various theories on integers, finite andinfinite string, and combinations thereof [1, 5].

5Deductive Proof System For First-Order
Fixpoint Logic

We now present our deductive system for the first-order fixpoint
logic introduced in Sec. 4.1. The deductive system is intended, but
not limited, to be used to discharge proof obligations that arise
during the process of type checking and inference for the typesystem presented in Sec. 4.4.
The deductive system comprises rules for reasoning via invariants and well-founded relations, and is able to solve formulas containing both least and greatest fixpoints. The key idea is to soundly
approximate formulas with fixpoints as formulas without fixpoints,

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi|= ψ
Fp-Valid⊩ψ|= [(λex .ψ ′ )/X ]ψ ⇒ ψ ′⊩ C − [[et /ex ]ψ ′ ]⊩ C − [(µX (ex ).ψ )(et )]|= ψ ′ ⇒ [(λex .ψ ′ )/X ]ψ

⊩ C + [[et /ex ]ψ ′ ]⊩ C + [(νX (ex ).ψ )(et )]Fp-Gfp+X (ex ); p1 ; p2 ; ⊤ ↓ nnf (ψ ) ⊩ C + [p1 (et )]⊩ C + [(µX (ex ).ψ )(et )]|= WF(p2 )⊩ C − [¬p1 (et )]−e⊩ C [(νX (ex ).ψ )(t )]|= WF(p2 )X (ex ); p1 ; p2 ; ⊤ ↑ nnf (ψ )Fp-Lfp−Fp-Lfp+Fp-Gfp−Figure 8. Proof rules for the fixpoint logic

which may be checked by off-the-shelf first-order theorem provers(SMT solvers) supporting the theories of integers and finite andinfinite strings over finite alphabet [1, 5].
A judgment ⊩ ϕ of the deductive system means that ϕ is valid.
The derivation rules for ⊩ ϕ are shown in Fig. 8. There, metavariable ψ ranges over formulas not containing fixpoint formulas(i.e., those of the form (µX (ex ).ϕ)(et ) and (νX (ex ).ϕ)(et )). The formulannf (ψ ) is the negation normal form of ψ , and |= WF(p) means thatthe predicate p = λex .ϕ is well-founded, that is, the arity of p is 2 × n
for some n and there is no infinite sequence e
t1, e
t 2 , . . . such that|eti | = n and p(eti , eti+1 ) holds for all i ≥ 1. C + (resp. C − ) is a formula
context whose hole occurs in a positive (resp. negative) position.
We now describe the rules. The rule Fp-Valid checks the validity
directly, and is applied when the given formula does not contain fixpoint formulas. Fp-Lfp− over-approximates a least fixpoint µX (ex ).ψ
that occurs in a negative position with a pre-fixpoint λe
x .ψ ′ of thefunction λX .λe
x .ψ . Note here that ψ and ψ ′ do not contain fixpoints.
An example of Fp-Lfp− can be seen in Sec. 2, where we discuss
proof subtree A. Meanwhile, Fp-Gfp+ is a dual rule and it underapproximates a greatest fixpoint νX (ex ).ψ that occurs in a positive
position with a post-fixpoint λe
x .ψ ′ of λX .λe
x .ψ .
By contrast, Fp-Lfp+ under-approximates a least fixpoint that
occurs in a positive position with a predicate p1 . Here, the auxiliary
judgment X (ex ); p1 ; p2 ;ψ ′ ↓ ψ is used to check that the well-foundedpredicate p2 witnesses that p1 under-approximates the least fixpointµX (ex ).ψ ′ ⇒ ψ . In a dual manner, Fp-Gfp− over-approximates agreatest fixpoint that occurs in a negative position with a predicate¬p1 . The auxiliary judgment X (ex ); p1 ; p2 ;ψ ′ ↑ ψ checks that thewell-founded predicate p2 witnesses that ¬p1 over-approximatesthe greatest fixpoint νX (ex ).ψ ′ ∧ ψ . An example of Fp-Gfp− can beseen in Sec. 2, where we discuss proof subtree B.
The rules in Fig. 8 reduce fixpoints to predicates but, in two cases,
lead to side conditions that the predicates indeed approximate thefixpoints. These conditions are treated themselves as judgments inthe auxiliary relations X (ex ); p1 ; p2 ;ψ ′ ↓ ψ and X (ex ); p1 ; p2 ;ψ ′ ↑ ψ ,defined in Fig. 9. There, we maintain the invariants that ψ is in
the negation normal form, ψ ′ does not contain X , and X may occur only positively in ψ . The rules let us then manipulate thejudgments to further reduce to predicate reasoning. The rules
Apx µ -∧ and Apx µ -∀ are similar to standard ones for first-orderlogic. Apx µ -∨ splits a judgment with the succedent of the form
ψ 1 ∨ ψ 2 into two judgments: one with the succedent ψ 1 and theantecedent conjuncted with ψ 1′ and the other with the succedentA Fixpoint Logic and Dependent Effects for
Temporal Property Verification

LICS ’18, July 9–12, 2018, Oxford, United Kingdom|= p1 (ex ) ∧ ψ ′ ⇒ ¬ψ|= p1 (ex) ∧ ψ ′ ⇒ ψ
Apx µ -BaseX (ex ); p1 ; p2 ;ψ ′ ↓ ψX (ex ); p1 ; p2 ;ψ ′ ↑ ψ|= p1 (ex ) ∧ ψ ⇒ p1 (et ) ∧ p2 (ex ,et)Apxν -RecX (ex ); p1 ; p2 ;ψ ↑ X (et)|= p1 (ex ) ∧ ψ ⇒ p1 (et ) ∧ p2 (ex ,et)Apx µ -RecX (ex ); p1 ; p2 ;ψ ↓ X (et)|= (p1 (ex ) ∧ ψ ) ⇒ (ψ 1′ ∨ ψ 2′ ) fv(ψi′ ) ⊆ {ex } X < fpv(ψi′ )X (ex ); p1 ; p2 ;ψ ∧ ψi′ ↑ ψi (i = 1, 2)

X (ex ); p1 ; p2 ;ψ ↓ ψ 1 X (ex ); p1 ; p2 ;ψ ↓ ψ 2
Apx µ -∧X (ex ); p1 ; p2 ;ψ ↓ ψ 1 ∧ ψ 2|= (p1 (ex ) ∧ ψ ) ⇒ (ψ 1′ ∨ ψ 2′ ) fv(ψi′ ) ⊆ {ex } X < fpv(ψi′ )X (ex ); p1 ; p2 ;ψ ∧ ψi′ ↓ ψi (i = 1, 2)
X (ex ); p1 ; p2 ;ψ ↓ ψ 1 ∨ ψ 2
X (ex ); p1 ; p2 ;ψ ′ ↓ [x ′ /x]ψx ′ < fv(ψ ′ ) ∪ fv(ψ ) ∪ {ex } ∪ fv(p1 ) ∪ fv(p2 )X (ex ); p1 ; p2 ;ψ ′ ↓ ∀x .ψ

Apxν -∧X (ex ); p1 ; p2 ;ψ ↑ ψ 1 ∧ ψ 2
X (ex ); p1 ; p2 ;ψ ↑ ψ 1

Apx µ -∨X (ex ); p1 ; p2 ;ψ ↑ ψ 2Apxν -∨X (ex ); p1 ; p2 ;ψ ↑ ψ 1 ∨ ψ 2|= (p1 (ex ) ∧ ψ ′ ) ⇒ ∃x ′ .ψ ′′ fv(ψ ′′ ) ⊆ {ex , x ′ } X < fpv(ψ ′′ )
′
′′
X (e
x ); p1 ; p2 ;ψ ∧ ψ ↑ [x ′ /x]ψx ′ < fv(ψ ′ ) ∪ fv(ψ ) ∪ {ex } ∪ fv(p1 ) ∪ fv(p2 )Apx µ -∀|= (p1 (ex ) ∧ ψ ′ ) ⇒ ∃x ′ .ψ ′′ fv(ψ ′′ ) ⊆ {ex , x ′ } X < fpv(ψ ′′ )X (ex ); p1 ; p2 ;ψ ′ ∧ ψ ′′ ↓ [x ′ /x]ψx ′ < fv(ψ ′ ) ∪ fv(ψ ) ∪ {ex } ∪ fv(p1 ) ∪ fv(p2 )X (ex ); p1 ; p2 ;ψ ′ ↓ ∃x .ψ

Apxν -BaseX (ex ); p1 ; p2 ;ψ ′ ↑ ∀x .ψ
Apx µ -∃X (ex ); p1 ; p2 ;ψ ′ ↑ [x ′ /x]ψx ′ < fv(ψ ′ ) ∪ fv(ψ ) ∪ {ex } ∪ fv(p1 ) ∪ fv(p2 )X (ex ); p1 ; p2 ;ψ ′ ↑ ∃x .ψ

Apxν -∀

Apxν -∃

Figure 9. Fixpoint approximation rules
ψ 2 and the antecedent conjuncted with ψ 2′ for some ψ 1′ and ψ 2′ suchthat ψ 1′ ∨ ψ 2′ holds provided the original antecedent does. Apx µ -∃generalizes Apx µ -∨ to judgments with the succedent of the form
∃x .ψ . Apx µ -Base exploits an external validity checker for formulas without fixpoints to discharge a judgment with the succedentψ , by assuming the predicate variables (including X ) that occur
t to thein ψ uninterpreted. Apx µ -Rec checks that the arguments erecursive occurrence of X satisfy p1 and the pair (ex ,et ) satisfies thewell-founded predicate p2 for any sequence of arguments xe of X ,in order to ensure that X is interpreted as an unbounded but finite
unfolding of µX (ex ).ψ . The rules Apxν -∗ are defined in a dual manner to Apx µ -∗. Note that the roles of ∧ and ∨ (also ∀ and ∃) areswitched. In the send_msgs derivation in Fig. 1, we used the greatest
fixpoint rules for conjunction (Apxν -∧), existential quantification(Apxν -∃), and conjunction again.
Lemma 5.1 shows that the approximation rules correctly under/over approximate least/greatest fixpoints. The soundness result(Theorem 5.2 immediately follows.
Lemma 5.1. Suppose thatψ is in negation normal form, X < fpv(ψ ′ ),and |= WF(p2 ). We have:
1. if X (ex ); p1 ; p2 ;ψ ′ ↓ ψ , then |= p1 (ex ) ⇒ (µX (ex ).¬ψ ′ ∨ ψ )(ex ),′′2. if X (ex ); p1 ; p2 ;ψ ↑ ψ , then |= (νX (ex ).ψ ∧ ψ )(ex ) ⇒ ¬p1 (ex ).
Theorem 5.2. If ⊩ ϕ, then |= ϕ.
The decidability of the deduction problem depends on the background first-order theory. It is undecidable for the fragment usedby our type system (indeed, it is already so with just linear integer
arithmetic). See [17] for details.

6

Related Work

Verification of higher-order programs is an active topic of research.
In recent years, numerous approaches have been proposed forautomatically (or semi-automatically) verifying a wide range of

temporal properties, including safety properties [6, 9, 19, 20, 23–25,
31, 32], termination [13, 28], non-termination [3, 14], and properties
expressed in linear µ-calculus [12, 16].
However, the existing proposals employ rather disparate techniques to verify the different classes of properties. For instance,
the safety property verification method of [9] applies predicate abstraction with CEGAR to iteratively reduce the problem to that ofhigher-order model checking [7, 18], whereas the termination verification method of [13] and linear µ-calculus verification method of[16] are based on a reduction to binary reachability analysis via program transformation. By contrast, we propose a unified type-based
approach to verify an expressive range of temporal properties given
as dependent-refinement types carrying dependent temporal effects.
The class of properties supported by our method subsumes thoseconsidered in the previous work mentioned above aside from thenon-termination property handled by [3, 14]. (Non-termination is
not within the scope of our work because it is a branching property.
See below for further discussion.)
An important classes of properties that are not addressed in thispaper are branching properties, such as those expressible in the
branching µ-calculus. Sound and complete methods for the classexist for well-typed finite-data higher-order programs (i.e., higherorder recursion schemes) [8, 18]. For infinite-data higher-order programs, a recent work by Unno et al. [26] proposes a type system thatcan uniformly deduce some restricted forms of branching properties
such as conditional non-safety and conditional non-termination.
However, their work does not address general temporal properties(even for the linear subclass). We leave the extension to branchingproperties as future work.
The dependent effects of our work are inspired by temporal
effects from the previous work on type-and-effect systems for temporal property verification [4, 12, 21]. Like in our work, temporal
effects facilitate compositional reasoning whereby the temporal

LICS ’18, July 9–12, 2018, Oxford, United Kingdom
behavior of program sub-terms are summarized as effects and combined to derive those of larger parts. However, the effects there were
non-dependent and also often coarsely over-approximate the actual
temporal behavior. For instance, [4, 21] only allow (ω-)regular setsof event sequences, and [12] (without oracles) always assigns Σωas the infinite effect part of a recursive function. Our work extends
the effects to dependent effects, which are fixpoint predicates on
event sequences and program values that can precisely capture
the temporal behavior, thereby enabling precise specification andverification of rich value-dependent temporal properties.
Our dependent temporal effects are first-order predicate fixpoint
logic formulas on event sequences and program values. While fixpoint logics such as µ-calculus are prevalent in temporal property
verification, most existing works only focus on the propositional
fragment (even for verification of infinite state systems [12, 16]),
and few considers temporal properties specified in a general predicate fixpoint logic. In [22], a system for deriving entailments in a
predicate fixpoint logic using well-founded induction is presented.
However, verification is not within the scope of their work.
An orthogonal direction of extension to the fixpoint logic is
to include higher-order propositions (or predicates) [15, 29]. In a
recent work, Kobayashi et al. [11] have proposed to apply suchhigher-order fixpoint logic (HFL) for verification of higher-orderprograms. Similar to our approach, they encode the verification
problem as problems in the fixpoint logic. More concretely, theirapproach encodes the given higher-order program as a HFL formula
so that the verification problem is reduced to a model checking
problem for HFL. However, their work does not present concretemeans to solve the obtained fixpoint logic problem (besides the casefor the propositional fragment which they show to be equivalent
to model checking of higher-order recursion schemes [10, 11]),
whereas we propose a deductive system for solving the fixpoint
logic constraints generated by the type-based verification process.
On the other hand, compared to our work that uses first-orderfixpoint logic, the use of higher-order logic may prove advantageous
in being able to more naturally model verification problems forhigher-order programs, analogous to the recent proposal of higherorder constrained Horn clauses for safety verification of higher-orderprograms [2]. We leave as future work for a deeper investigationof the relation.

7

Conclusion and Future Work

We have presented a novel method for reasoning about the temporal
properties of higher-order programs. We use a type-based, compositional approach that is, in contrast to prior work [12], nonethelessamenable to algorithmic verification. Also, our treatment with effectpredicates and predicate variables, has led to least/greatest-fixpoint
typing rules that do not sacrifice precision, as was the case in otherprior work. We also present a deductive fixpoint proof system thatallows us to introduce approximations in the form of invariants
and well-founded relations.
In future work, we plan to build on our type system and develop
type inference algorithms, automating our type system and deductive fixpoint proof system. We also plan to explore relationships
between our dependent temporal events and works on resource
analysis, as discussed with the amortized complexity example atthe end of Sec. 2.

Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi

Acknowledgments
We thank Naoki Kobayashi and anonymous referees for helpfulcomments and suggestions. This research was supported in partby MEXT Kakenhi 15H05706, 16H05856, 17H01720, and 17H01723;
JSPS Core-to-Core Program, A.Advanced Research Networks; JSPS
Bilateral Collaboration Research; the National Science Foundation(NSF) award #1618542; and the Office of Naval Research (ONR)
award #N000141712787.

References[1] P. A. Abdulla, M. F. Atig, Y. Chen, L. Holík, A. Rezine, P. Rümmer, and J. Stenman.
String constraints for verification. In CAV, 2014.
[2] T. C. Burn, C. L. Ong, and S. J. Ramsay. Higher-order constrained horn clauses
for verification. PACMPL, 2(POPL), 2018.
[3] K. Hashimoto and H. Unno. Refinement type inference via horn constraint
optimization. In SAS, 2015.
[4] M. Hofmann and W. Chen. Abstract interpretation from Büchi automata. In
CSL-LICS, 2014.
[5] L. Holík, P. Janku, A. W. Lin, P. Rümmer, and T. Vojnar. String constraints withconcatenation and transducers solved efficiently. PACMPL, 2(POPL), 2018.
[6] R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: verifying functional programs
using abstract interpreters. In CAV, 2011.
[7] N. Kobayashi. Types and higher-order recursion schemes for verification ofhigher-order programs. In POPL, 2009.
[8] N. Kobayashi and C. L. Ong. A type system equivalent to the modal mu-calculus
model checking of higher-order recursion schemes. In LICS, 2009.
[9] N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for
higher-order model checking. In PLDI, 2011.
[10] N. Kobayashi, É. Lozes, and F. Bruse. On the relationship between higher-orderrecursion schemes and higher-order fixpoint logic. In POPL, 2017.
[11] N. Kobayashi, T. Tsukada, and K. Watanabe. Higher-order program verification
via HFL model checking. In ESOP, 2018.
[12] E. Koskinen and T. Terauchi. Local temporal reasoning. In CSL-LICS, 2014.
[13] T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination
verification for higher-order functional programs. In ESOP, 2014.
[14] T. Kuwahara, R. Sato, H. Unno, and N. Kobayashi. Predicate abstraction and
CEGAR for disproving termination of higher-order functional programs. In CAV,2015.
[15] M. Lange, É. Lozes, and M. V. Guzmán. Model-checking process equivalences.
Theor. Comput. Sci., 560, 2014.
[16] A. Murase, T. Terauchi, N. Kobayashi, R. Sato, and H. Unno. Temporal verificationof higher-order functional programs. In POPL, 2016.
[17] Y. Nanjo, H. Unno, E. Koskinen, and T. Terauchi. A fixpoint logic and dependent
effects for temporal property verification. Extended version, available fromhttp://www.cs.tsukuba.ac.jp/~uhiro/.
[18] C. L. Ong. On model-checking trees generated by higher-order recursion schemes.
In LICS, 2006.
[19] C. L. Ong and S. J. Ramsay. Verifying higher-order functional programs withpattern-matching algebraic data types. In POPL, 2011.
[20] P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, 2008.
[21] C. Skalka, S. F. Smith, and D. V. Horn. Types and trace effects of higher orderprograms. J. Funct. Program., 18(2), 2008.
[22] C. Sprenger and M. Dam. On the structure of inductive reasoning: Circular andtree-shaped proofs in the µ -calculus. In FOSSACS, 2003.
[23] T. Terauchi. Dependent types from counterexamples. In POPL, 2010.
[24] H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP,
2009.
[25] H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In POPL, 2013.
[26] H. Unno, Y. Satake, and T. Terauchi. Relatively complete refinement type systemfor verification of higher-order non-deterministic programs. PACMPL, 2(POPL),
2018.
[27] M. Y. Vardi. Verification of concurrent programs: The automata-theoretic framework. Ann. Pure Appl. Logic, 51(1-2), 1991.
[28] N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. P. Jones. Refinement types
for haskell. In ICFP, 2014.
[29] M. Viswanathan and R. Viswanathan. A higher order modal fixed point logic. In
CONCUR, 2004.
[30] H. Xi and F. Pfenning. Dependent types in practical programming. In POPL,
1999.
[31] H. Zhu and S. Jagannathan. Compositional and lightweight dependent type
inference for ML. In VMCAI, 2013.
[32] H. Zhu, A. V. Nori, and S. Jagannathan. Learning refinement types. In ICFP, 2015.