Local Temporal Reasoning
Eric Koskinen ∗ †Tachio Terauchi ‡New York University

Japan Advanced Institute of Science and Technology

Abstract
We present the first method for reasoning about temporal logic
properties of higher-order, infinite-data programs. By distinguishing between the finite traces and infinite traces in the specification,
we obtain rules that permit us to reason about the temporal behaviorof program parts via a type-and-effect system, which is then able
to compose these facts together to prove the overall target propertyof the program. The type system alone is strong enough to derive
many temporal safety properties using refinement types and temporal effects. We also show how existing techniques can be usedas oracles to provide liveness information (e.g. termination) aboutprogram parts and that the type-and-effect system can combine thisinformation with temporal safety information to derive nontrivial
temporal properties. Our work has application toward verificationof higher-order software, as well as modular strategies for procedural programs.
Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification—Model checking; Correctness proofs; Reliability; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs;
F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—Program analysis; F.3.3 [Logics and Meanings
of Programs]: Studies of Program Constructs—Type structure
General Terms Algorithms, Languages, Theory, Verification
Keywords Higher-order programs, formal verification, temporal
logic, program analysis, model checking

1. Introduction
Programming languages that use higher-order functionality(e.g. Java, C#, F#, Haskell, Ocaml, Perl, Python, Ruby) have become commonplace. Higher-order language features such as map,
grep, Google’s Map/Reduce, are used widely and applauded fortheir simplicity and modularity.
∗ Supported in part by the CMACS NSF Expeditions in Computing award

0926166.
† Supported in part by the Japan Society for the Promotion of Science(JSPS).
‡ Supported in part by MEXT Kakenhi 26330082 and 25280023.

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 afee. Request permissions from permissions@acm.org.
CSL-LICS 2014, July 14–18, 2014, Vienna, Austria.
Copyright © 2014 ACM 978-1-4503-2886-9. . . $15.00.
http://dx.doi.org/10.1145/2603088.2603138

Meanwhile, in the past couple of decades, algorithms and tools
have emerged that have enabled automatic verification of someindustrial software systems. Symbolic analysis techniques suchas abstraction refinement [7] and interpolation [24] have givenrise to interprocedural program analysis tools for safety [2, 5],
while termination argument refinement [25] has led to tools for
liveness [8, 13]. Further research has led to tools and algorithms
for verifying properties expressed in temporal logic: more elaborate
specifications that combine safety and liveness [1, 4, 9–12].
The verification techniques discussed thus far have been mostly
limited to imperative first-order software and cannot be applied tohigher-order programming languages. In recent years, researchers
have developed some techniques for verifying higher-order programs. Some showed how to verifying temporal properties ofhigher-order programs when the domain of data is finite (i.e.
boolean). Others have also developed methods of verifying purely
safety properties [16, 19, 26, 29] or purely termination [21, 22] ofhigher-order programs with infinite data (e.g. integers) . Despite
the efforts discussed above, at present there are no methods forverifying safety/liveness properties (i.e. temporal logic formulae)of programs written in higher-order languages.
We present the first technique for verifying temporal logic properties of higher-order, infinite-data programs. The crux of our work
is to decompose the problem, not only by dividing the program up
into individual expressions via a type-and-effect system, but also,
for every expression, to track the behavior of finite traces separate
from the behavior of infinite traces. Our type rules permit verification oracles (including the type system itself) to reason about
the conditional safety and liveness (i.e. temporal) behavior of program parts, and compose these facts together to prove the overalltarget property of the program. Moreover, we show that existing
tools can be used as oracles to introduce liveness proofs into thetype system’s effects. While it is a commonly held belief that typesystems cannot be used for liveness properties, we show how theycan, nonetheless, be used to carry some liveness information andsoundly combine reasoning about program parts together to proveoverall safety and liveness.
By way of an example, consider a function application e v,
where we are attempting to prove an overall temporal property“tick U boom,” which means that some event tick will occur
repeatedly until the event boom occurs, and boom is inevitable.
With the type-and-effect system described in this paper we can, forexample, reason about the safety behaviorboomΓ ⊢ e ∶ τ ÐÐ→ τ ′ & tick*that is due to the reduction of e (repeating event tick) and the latent
behavior (event boom) that arises when e is applied to a value v ∶ τ ,and then separately reason about the termination of (the reductionof) e via an oracle:Γ ⊢ e v ∶ τ ′ & terminatesWe are using shorthand in these judgments’ effects, whereas formally our type system distinguishes the behavior of finite tracesfrom the behavior of infinite traces. The type-and-effect system inthis paper combines all of this information together via refinement
types, and temporal connectives (intersection, union, concatenation) to obtain an overall goal judgmentΓ ⊢ e v ∶ τ ′ & tick U boom
while carefully accounting for possibly divergent evaluations. Ourformalism permits oracles of arbitrary temporal expressive power.
Our use of termination in the example above is a special case.
Contributions. To our knowledge, this work marks the first
method for reasoning about temporal logic properties of higherorder programs that have infinite data. The above is a limited example. We believe our work provides the theoretical foundation
toward several areas of practical significance. To this end, we havedevised general rules so there are many instantiations and applications of them, including:
1. Instantiation to a wide variety of specification logics. We areable to support any logic that is closed under intersection,
union, and composition (over finite and infinite traces) suchas Büchi specifications. We sometimes use LTL as a shorthandfor Büchi [15].
2. Instantiation to arbitrary type environments. Often the type system alone is strong enough to derive safety properties. For example, when using refinement types in the absence of a termination oracle, our rules can be thought of as a novel extension
to dependent types, where temporal behaviors are carried as effects.
3. Instantiation of oracles to any fragment of program expressions
or any subset of the specification logic.
4. Instantiation to a modular reasoning system for temporal behaviors of first-order procedural programs.
We have devised our methodology to be based on local reasoning,
employing a type system. This stands in contrast to many existing verification works for higher-order programs that operate by
extracting a transition system and then performing standard model
checking techniques. Such existing techniques suffer from the inability to refine the abstraction during the verification process and,moreover, require input programs to be given in CPS form.
Limitations. It is a commonly held belief that (ordinary) typesystems cannot be used to derive liveness properties. In this paper, we do not allow the type system to derive (non-trivial) liveness properties by itself. However, when liveness information is
introduced by an oracle (e.g. a termination oracle), our type system is able to soundly combine this liveness information withsafety/liveness information from other oracles or the type system itself. To maintain soundness, we also have to be careful when typing
recursive functions, as we will discuss in the next section. Finally,note that the temporal behavior of a program is directly related toits evaluation order. For the purposes of this paper, we assume astrict evaluation order.
Organization. We first give a high-level description of our
methodology in Section 2. After preliminaries in Section 3, we
present our type and effect system in Section 4. We prove typesoundness (Theorem 4.1). We then examine a variety of examples,
discussed in Section 5, that span a range of temporal behaviors,
compositions and oracle power. We conclude with a discussion ofrelated work in Section 6.

2. Overview
Consider the following higher-order program, written in an MLlike syntax:
Example 1.

1 let rec zoom

= ev[zoom]; zoom ()2 and shrink f = ev[shrink];
3
if ( f () = 0 ) then4zoom ()
5else
6shrink (λ . (f ()) - 1)
7 and main() = ev[main];
89

let t = *pos inshrink (λ . t)

For the moment, think of the boxed expressions as skip. The function zoom calls it self recursively, looping forever. Next, shrink is
a recursive function and it takes, as an argument, a function f fromunit to int. If applying f returns 0, zoom is called. Otherwise,
shrink is called recursively with a new partially-defined argument.
Finally, main initiates with the expression shrink (λ . t) where t
is bound to a nondeterministically chosen positive integer (denoted*pos ).
For this example, we may want to prove the Linear Temporal
Logic (LTL) property: Φ = main ∧ X(shrink U zoom). (Weare abusing notation here and using LTL as shorthand for a Büchi
specification over finite and infinite executions, but we will discussthat shortly.) This property consists of the temporal operators X
and U as well as atomic propositions that are events, denoted in
the event font. Events are emitted by the ev[event] expression. For
simplicity, in the above example we correlate events with function
calls, indicating that the function with the corresponding name has
been called (this correlation is also a suitable definition of events inthe context of practical examples). The property Φ specifies that themain function will be called first (event main) and then in the next
step, the shrink function will be called (event shrink) repeatedly
Until zoom is called (event zoom). U is the strong until operator,
which specifies that its second argument must hold after finitely
many steps.
Intuitively, we know that Φ holds of the above example. The
property Φ is a trace-based property and specifies that every (terminating or nonterminating) execution of this program must generate
event sequences of the form:
main, (shrink)∗ , zoom, ...
where there are finitely many instances of shrink. The property
holds because, when shrink is called with a function that returns
a positive integer, shrink will eventually call zoom.
Proving that this property holds of this program is challenging. There are several obstacles: First it consists of both safety
and liveness aspects, in the form of reachability and termination.
Second, there is nondeterministic input. Third, the state space isinfinite. Finally, this is a higher-order program. There are several
recent related works, but all of them have restrictions that makethem unsuitable to this example. Some works are restricted to finite
data [18], others can reason over infinite data but are restricted tosafety [29] or termination [21] properties, and still others can reason about infinite-state systems but are restricted to first-order input
programs [10].
Compositional reasoning. The key idea of this paper is to decompose the problem of verifying that the entire program satisfies
Φ into pieces in two ways. The first decomposition is not surprising: we divide the program up into its individual expressions so that
we can determine which events arise from a given expression. For
example, the behavior of a function application e v is determinedby separately considering the behavior of the value v as it is re-duced, the behavior of the function expression e as it is reduced
and, finally, the latent behavior that arises when e is applied to v.
The second form of decomposition is that, for every expression,
we track the event behavior of finite traces separate from the event
behavior of infinite traces. That is, for an expression e we will
have two specifications: Ξ for the finite part and Π for the infinite
part. The event behavior of e is the union of these specifications.
Büchi automata provide a convenient such specification languagethat can be characterized separately over finite and infinite runs.
(Büchi automata are also known to be closed under concatenation
across the two partitions [30], which we will see to be importantin Section 3.) The informed reader will note two commonly held
beliefs. First, liveness is generally not composable: one cannot, ingeneral, find a witness to non-liveness with a finite prefix of a trace.
Related is the second belief that per-expression reasoning, as seenin type systems, cannot be used for liveness. However, as we will
see here, type systems can be used to carry temporal safety andliveness specifications for expressions. This fact, combined with
our separation of finite traces from infinite traces, allows us tosoundly combine reasoning about program parts together to proveoverall safety and liveness.
Our technique is best illustrated through the running example.
After the main event fires and t is bound, we need to show that the
body of main, shrink (λ . t), satisfies shrink U zoom. In this paper, we characterize the temporal behavior of program expressions
via a type-and-effect system that distinguishes between finite andinfinite event traces. Syntactically, judgments are of the form:

Our type-and-effect system combines these facts (whose origins
we will next discuss) together to obtain a final judgment, using a
few rules such as function application (App), the combination rule
(Comb), and the subtyping rule (Sub):Γ ⊢ e ∶ τ & (Ξ, Π)

Safety via the type system. We can use our type-and-effect system to deduce that the function shrink has the latent (safety) effectshrink W zoom. This arises as a fixpoint solution to the typing
context in the judgments over the body of shrink. Assume that wehave a typing environment Γ that already contains a judgment:

which denotes that, under a typing context Γ, we deduce that
expression e has a (refinement) type τ , that finite event traces of
e satisfy Ξ, and that infinite event traces of e satisfy Π.
Our type system permits us to decompose our reasoning about
Example 1 into separate components:
1. The latent temporal behavior arising from shrink when it isapplied to an argument:
J1

shrink W zoomΓ ⊢ shrink ∶ (unit → int) ÐÐÐÐÐÐ→ unit & ε

The above judgment J1 says that shrink is a function which
consumes a function and returns unit (i.e., “()”). shrink itself
is a function value and, as such, it generates no effects, denoted ε. However, when shrink is applied, the latent behavior“shrink W zoom” occurs, indicating that event shrink occurs
until event zoom (but not that zoom will necessarily inevitably
occur). Formally, as we will discuss later in the paper, the latenteffects are also represented as a pair (Ξ, Π) of finite and infinite
traces (e.g., as finite and Büchi automaton). But, we are abbreviating it in LTL by encoding terminating runs as self-loops, as
is commonly done.
2. The conditions under which shrink terminates:
J2

F¬shrinkΓ ⊢ shrink ∶ (unit → {i ∣ i ≥ 0}) ÐÐÐÐ→ unit & ε

We use refinement (dependent) types [32] to say that the argument of shrink is a function that returns an integer above 0.
In this judgment J2 , the latent effect is F¬shrink, indicatingthat eventually an event will occur that is not shrink. For convenience, we will sometimes abbreviate such termination judgments as “Γ ⊢ e ∶ τ & terminates”.
Notice that in the above judgment we have used a refinement
type system to place the conditions on (the function passedto) shrink under which shrink will terminate: that the passed
function is returning a nonnegative number.

J1

J2... (λ . t) ...
⋮App... (λ . t) ...
⋮

App
Comb

⋮
Sub
Γ, t ∶ {i ∣ i ≥ 0} ⊢ shrink (λ . t) ∶ unit & shrink U zoom
This final judgment indicates that the expression (shrink λ . t)
has unit type and will exhibit a finite sequence of shrink events,
followed by a zoom event.
Our type-and-effect system, formalized in Section 4, consistsof several other rules that combine temporal information about expressions, taking care to account for possibly divergent computation. To be able to combine rich information across different oracles, we adopt and extend the refinement type system that has garnered popularity in the verification of functional programs [6, 16,
19, 26, 29, 31]. There are typing rules for all the usual higher-orderfeatures such as subtyping, intersection, etc—however, they will
now also carry the temporal effect of each (sub)expression.
In the above example, our work combined a derivation J1 ,which is a safety proof with a derivation J2 which is a termination
proof. But one is inclined to wonder: where do these pieces comefrom in the first place? We will now describe how these subproofs
are obtained, respectively.

G zoomΓ(zoom) = unit ÐÐÐ→ unit & εindicating that when zoom is applied to unit an arbitrarily longsequence of zoom events may occur. We also know that an application of shrink will generate event shrink. (We assume that every
named function begins with a special event statement of the same
name, but this has been omitted for readability. For example, thebody of shrink in Example 1 is “ev[shrink]; if ...”).
Depending on which branch is taken in shrink, either shrink willrecur, generating event shrink or else the expression zoom () will
generate event G zoom. Since we do not know a priori whether
f () = 0 returns true or false, a valid typing context will say thatshrink f satisfies shrink∨G zoom. This disjunction of event atomic
propositions is valid, however, it only asserts the event currently
generated. If we look for a fixpoint of
α = shrink ∧ X(G zoom ∨ α)
there is a stronger solution:
Γ, zoom ∶ ... ⊢ shrink f ∶ unit & shrink W (G zoom)
Note that type systems typically do not distinguish fixpoints (e.g.
greatest versus least) and, as such, we cannot conclude anything
about the infinite traces. However, we can combine a judgementof shrink W (G zoom) over the finite traces, with an oracle
judgement that G(shrink ∨ zoom) holds over the infinite traces,
to obtain that shrink W (G zoom) holds over all traces1 .
Liveness via a termination oracle. Type systems themselves
cannot generate liveness information. However, we show how they
1 We conjecture that there is a way to organize type systems so that infinite-

trace behaviors of expressions can arise from fixpoint equations, but weleave this to future work.

P
a
e

∶∶=
∶∶∈
∶∶=
∣

P ∪ {F x̄ = e} ∣ ∅Σx ∣ c ∣ F ∣ ev[a] ∣ let x = e1 in e2 ∣ x y
x op y ∣ if x then e1 else e2 ∣ λx.eΓ ⊢s c ∶ sty(c)Γ ⊢s x ∶ B1Γ ⊢s y ∶ B2sty(op) = B1 → B2 → B3
Γ ⊢s x op y ∶ B3

Figure 1: The syntax of the simple functional language.

Γ ⊢s F ∶ Γ(F) Γ ⊢s x ∶ Γ(x)can be used to carry liveness (or safety) information obtained froman outside source. This is accomplished via an oracle rule:Θ▸e∶τ &Φ
Oracle∆, Θ ⊢ e ∶ τ & Φ(Note that an oracle ▸ must satisfy the Oracle property in Definition 4.1.) This rule is very general and it allows us to incorporate
information from external techniques into our type-and-effect system. Let us look again at the body of shrink. If f is a function that,when applied to (), returns 0, then zoom will be invoked. Otherwise, shrink is called recursively with a partial function definition(λ . (f ())−1). Intuitively we know that this recursive function terminates provided that it is applied to a function f that, when applied
to (), returns a positive integer. In recent work [21] we describe atechnique for proving termination of higher-order programs. We
can adapt this technique to prove a temporal property (F¬shrink)that is similar to termination, under the condition that f() is nonnegative. With this proof in hand, we can use the oracle rule toconclude thatΓ, x∶s ⊢s e ∶ s′
Γ ⊢s λx.e ∶ s → s′ Γ ⊢s ev[a] ∶ unitΓ ⊢s e1 ∶ s Γ, x∶s ⊢s e2 ∶ s′
Γ ⊢s let x = e1 in e2 ∶ s′
Γ ⊢s x ∶ s → s′ Γ ⊢s y ∶ s
Γ ⊢s x y ∶ s′
Γ ⊢s x ∶ bool Γ ⊢s e1 ∶ s Γ ⊢s e2 ∶ s
Γ ⊢s if x then e1 else e2 ∶ s∀F x̄ = e ∈ P.Γ ⊢s λx̄.e ∶ Γ(F)Γ ⊢s ⋆
Figure 2: Simple type system type checking rules.

F¬shrinkΓ ⊢ shrink ∶ (unit → {i ∣ i ≥ 0}) ÐÐÐÐ→ unit & ε
Of course in general, the oracle rule can be used to introduce moreelaborate temporal specifications. We will see such examples in
Section 5.
The example in this section provided a small illustration of
how our work combines temporal reasoning over separate program
pieces together to prove overall temporal properties. In Section 5
we present a variety of examples that illustrate many ways that ourwork can be instantiated. In addition to verification of higher-orderprograms, our work also suggests a local technique for verificationof first-order interprocedural programs that would escape previous
restrictions on the logic [1]. We now turn to a formal presentationof our work.

For simplicity, we restrict branch conditions, operator arguments and the expressions in function applications to variables. But
note that a non-variable form can be encoded by using let (e.g.
e1 e2 can be encoded as let x = e1 in let y = e2 in x y). For convenience, we use the non-variable forms when the encoding is clear
from the context.
As usual, applications associate to the left so that e0 e1 e2 =(e0 e1 ) e2 . We write e1 ; e2 for let x = e1 in e2 such that x ∉fv(e2 ). Without loss of generality, we assume that bound variables
are distinct. We say that an expression is closed if it contains nofree variables.
We assume that the program is simply typed. For an expression
e in the program, write sty(e) for its simple type. A simple type, s,
is defined by the following grammar.
Bs

3. Preliminaries
We focus on a small functional language shown in Figure 1. A program, P , is a finite set of mutually recursive function definitions.
F x̄ = e uniquely defines a function named F with the formal parameters x̄ and the closed expression e as the body. Function names
may appear free in a function body. The notation x̄ denotes a possibly empty sequence. Note that nested recursive function definitions
can be supported via λ lifting [17].
Expressions, e, comprises constants c, function names F, variables x, lambda abstractions λx.e, constant operations x op y,function applications x y, event raises ev[a], conditional branches
if x then e2 else e3 , and let expressions let x = e1 in e2 . In
ev[a], a ∈ Σ is an event symbol. We assume that the set of event
symbols Σ contains a special event symbol step whose role is explained below. The constants include the boolean constants trueand false, the unit constant (), and the integer constants. The operator op include boolean and integer operators such as +, −, ≤, aswell as the operator ∗int that returns a non-deterministic integer(for simplicity, we often write ∗int for ∗int ). We write fv(e) for
the free variables of e.

∶∶=
∶∶=

int ∣ bool ∣ unit
B ∣ s1 → s2

Figure 2 defines the simple typing judgement ⊢s . A program P issimply typed if Γ ⊢s ⋆. (The program is implicit and is omitted in
the type judgement rules.)3.1 Semantics
We define the call-by-value semantics of the language via bigstep evaluation rules. We define terminating evaluation by theusual inductive rules (⇓P ), and define non-terminating runs by coinductive rules (⇑P ), following the previous work on co-inductive
big-step [14, 23]. Non-terminating runs need be provided as well as
the usual terminating ones because we are concerned with possibly
infinite sequences of events generated by the program.
The terminating judgement e ⇓P v & ̟ expresses that theexpression e evaluates to the value v producing the finite sequenceof events ̟ ∈ Σ∗ . A value is either a constant or a closed λx.e
(i.e., fv(e) ⊆ {x}). The non-terminating judgement e ⇑P  & π
expresses that e diverges and produces the infinite sequence of
events π ∈ Σω . Because of non-determinism, an expression canhave multiple terminating and non-terminating evaluations. We

T ERMINATING RUNSe[v/x] ⇓P v ′ & ̟(λx.e) v ⇓P v ′ & step ⋅ ̟

st-AppJopK(c1 , c2 ) = c
st-Op
st-Valc1 op c2 ⇓P c & εv ⇓P v & ε
F x̄ = e ∈ P
st-Ev
st-FunF ⇓P λx̄.e & ε
ev[a] ⇓P () & a
e1 ⇓P v & ̟1′e2 [v/x] ⇓P v & ̟2

let x = e1 in e2 ⇓P v ′ & ̟1 ⋅ ̟2

st-Lete1 ⇓P v & ̟
st-If1
if true then e1 else e2 ⇓P v & ̟
e2 ⇓P v & ̟
st-If2
if false then e1 else e2 ⇓P v & ̟
N ON - TERMINATING RUNSe[v/x] ⇑P  & π
snt-App(λx.e) v ⇑P  & step ⋅ π
e1 ⇑P  & π
snt-Let1
let x = e1 in e2 ⇑P  & π
e1 ⇓P v, ̟ e2 [v/x] ⇑P  & π
snt-Let2
let x = e1 in e2 ⇑P  & ̟ ⋅ π
e1 ⇑P  & π
snt-If1
if true then e1 else e2 ⇑P  & π
e2 ⇑P  & π
snt-If2
if false then e1 else e2 ⇑P  & π
Figure 3: Semantics of the simple functional language

denote concatenation of finite event sequences ̟1 and ̟2 by̟1 ⋅ ̟2 , and the concatenation of an finite event sequence ̟ toan infinite event sequence π by ̟ ⋅ π.
Figure 3 shows the evaluation rules. We describe the key rules.
The rule st-Ev evaluates ev[a] to a unit value, producing the event
a. The rule st-App evaluates a function application (λx.e) v. The
rule handles the case where the function call (i.e,. the evaluationof e[v/x]) terminates. The special event step is used to prevent
hidden computation. The rule snt-App is similar to st-App, but forthe case the call diverges. In st-Op, JopK denotes the semantics ofthe operator op. For example, J+K(i, j) = i + j for any i, j ∈ Z, andJ∗int K(i, j) = k for any i, j, k ∈ Z.
Remark: Hidden Computation. In temporal verification of
first-order as well as higher-order programs there is some degreeof engineering choice that needs to be made as to what constitutes
a subsequent state. Related is the choice of the atomic proposition language and what aspect of the state are represented by that
language. Imagine, for example, the imperative program: “x:=1;
increment(x); x:=-1;” The property F(x < 0) holds unless,of course, increment(x) diverges. It depends greatly on whatis defined to be (i) the “state” of the program automaton and (ii)

Ξ
Π
Φ
B

∶∶⊆
∶∶⊆
∶∶=
∶∶=

Σ∗
Σω
(Ξ, Π)
int ∣ bool ∣ unit

τ, σ

∶∶=

{u∶B ∣ θ} ∣ x∶σ Ð→τΦFigure 4: Type syntax
the process of computing the subsequent such state. Trouble arises
when it is possible for ii to execute infinitely many steps.
We think that this is an important point and so, in this paper, wehave given a semantics for the λ-calculus that ensures that there
are no infinite, invisible computations. We do this by inserting
step events, as described above. We argue that future temporal
verification techniques and tools for both first- and higher-ordershould be developed with this in mind. In the context of first-orderprograms, a state is typically defined to be the valuation of all
program variables. This precludes the observation that there canbe infinite computation over registers. We urge future semantics
for first-order programs to incorporate a strategy similar to ours inorder to ensure there is no hidden computation. There is, however,a caveat: user specifications may be impacted. A specification suchas Fp holds regardless of how many step events occur before p. A
specification such as Gp must be written with the possibility of step
events in mind. In most cases, the intention of a Gp specification isreally G(step ∨ p).
◻
Returning to the language semantics, the rule snt-App is also
used to evaluate function applications:e[v/x] ⇑P  & π
snt-App(λx.e) v ⇑P  & step ⋅ πThis rule handles the case when the function call diverges (i.e., theevaluation of e[v/x] diverges).
Example 2. Let P be the following four-function program:F g = ev[a]; if ∗int then g 0 else F (H g)
G x = ev[b]; 1
H g x = ev[c]; g x
I () = F G; F G
Let â = step ⋅ a, b̂ = step ⋅ b, and ĉ = step ⋅ c. Let A be the regular
language â∗ ⋅ ĉ∗ ⋅ b̂. Then, I () ⇓P v, ̟ if and only if ̟ ∈ Ξ andv = 1, and I () ⇑P , π if and only if π ∈ Π whereΞ = {̟ ⋅ ̟′ ∣ ̟ ∈ A ∪ {ε} ∧ ̟′ ∈ A}
Π = {, ̟ ⋅ âω ∣ ̟ ∈ A ∪ {ε}}We often omit the program P from the definitions when the
program is clear from the context. For example, we simply write ⇓and ⇑ instead of ⇓P and ⇑P .

4. Type System
We now formalize the type and effect system. Intuitively, our typeand effect system is an orchestrating language that glues together
information from the temporal property verifier oracles (termination checker, safety checker, etc.). As we described in Section 2, inorder to be able to communicate rich information across the different oracles, we adopt and extend the refinement (dependent) typesystem that has garnered recent popularity [6, 16, 19, 26, 29, 31].
Figure 4 defines the syntax of types. Per previous work on
refinement type systems, types include refinement base types{u∶B ∣ θ} that refines the base-type B by the refinement predicate
θ which is a formula in some first-order logic theory on base-type(Ξ1 , Π1 ) ∪ (Ξ2 , Π2 ) = (Ξ1 ∪ Ξ2 , Π1 ∪ Π2 )(Ξ1 , Π1 ) ∩ (Ξ2 , Π2 ) = (Ξ1 ∩ Ξ2 , Π1 ∩ Π2 )(Ξ1 , Π1 ) ⋅ (Ξ2 , Π2 ) = (Ξ1 ⋅ Ξ2 , Π1 ∪ (Ξ1 ⋅ Π2 ))(Ξ1 , Π1 ) ⊆ (Ξ2 , Π2 ) ⇔ Ξ1 ⊆ Ξ2 ∧ Π1 ⊆ Π2
Figure 5: Trace set operations.

u ∉ fv(JΓKbase ) ⊧ JΓKbase ∧ θ1 ⇒ θ2
Γ ⊢ {u∶B ∣ θ1 } ≤ {u∶B ∣ θ2 }JΓKbase is the FOL formula denoting the assumptions about thebase-type variables in Γ, and is defined as follows.
JεKbase = ⊺JΓ, x∶{u∶B ∣ θ}Kbase = JΓKbase ∧ θ[x/u]JΓ, θKbase = JΓKbase ∧ θJΓ, x∶τ Kbase = JΓKbase τ not refinement base type
We use the meta variable ∆ for type environment containing
only the function names, and Θ for the type environment containing
only the variables (both base-type and function-type variables) andthe formulas. Note that any type environment Γ can be split into thefunction name part and the variable part so that Γ = ∆, Θ.
4.2 Variable-to-value SubstitutionΓ ⊢ σ2 ≤ σ1

Γ, x ∶ σ2 ⊢ τ1 ≤ τ2
Φ1

Φ1 ⊆ Φ2

Φ2

Γ ⊢ x∶σ1 Ð→ τ1 ≤ x∶σ2 Ð→ τ2
Figure 8: Subtyping rules.

variables. We sometimes abbreviate {u∶B ∣ θ} as B when θ is atautology (e.g., {u∶B ∣ ⊺} = B). Intuitively, {u∶B ∣ θ} denotes thetype of some value u of the base type B satisfying the formula θ.
Φ
The type x ∶ σ Ð→ τ is a dependent function type, consistingof the argument type σ and the return type τ and the latent effectΦ. We extend the dependent function type from previous work byΦadding trace sets as a latent effect. Intuitively, x ∶ σ Ð→ τ denotes
the type of a function that returns a value of the type τ [y/x] andgenerates the events represented by the effect Φ when applied to anargument y of the type σ. As usual, → associates to the right. The
system is parametrized by the class of trace sets that are usable as
the effects.
An effect is a pair comprising a set of finite traces Ξ (theterminating part) and a set of infinite traces Π (the non-terminatingpart). We define operations on effects component-wise as shown in
Figure 5. Here, Ξ1 ⋅ Ξ2 denotes the concatenation of the traces inΞ1 to those in Ξ2 and is defined {̟1 ⋅ ̟2 ∣ ̟1 ∈ Ξ1 ∧ ̟2 ∈ Ξ2 }.
Similarly, a concatenation of a set of finite traces Ξ to a set of
infinite traces Π is defined as Ξ ⋅ Π = {̟ ⋅ π ∣ ̟ ∈ Ξ ∧ π ∈ Π}.
The type system may be used by instantiating the effects withany class of trace sets that are closed under the operations. In theexamples in this paper, we use a pair of finite state automaton andBüchi automaton (i.e., regular and ω-regular trace sets) which havethe required closure property [30]. We use LTL as a shorthand fortrace sets by interpreting a finite trace as the infinite trace that selfloops at the last event (e.g.,  = ∅, ⊺ = Σ∗ , and aUb = a∗ ⋅ b ⋅ Σ∗ ,for finite traces).
ΦThe type {x∶B ∣ θ} binds x in θ. Likewise, x ∶ σ Ð→ τ binds
x in τ (but not in σ). That is, fv({x∶B ∣ θ}) = fv(θ) ∖ {x}, andΦ
fv(x∶σ Ð→ τ ) = fv(σ) ∪ (fv(τ ) ∖ {x}). Types are equivalent up
to renaming of bound variables. We say that a type is closed if it
contains no free variables.
4.1

Type Environment

A type environment Γ is a sequence of variable binding x ∶ τ ,function name binding F ∶ τ , and a FOL formula θ. The formulas
θ are used to express the branch conditions (cf. [26, 29]). We often
treat Γ as a set and write x ∶ τ ∈ Γ, θ ∈ Γ, etc. to access its elements.
We write dom(Γ) for the variables and function names that arebound in Γ, that is, dom(Γ) = {κ ∣ κ ∶ τ ∈ Γ}. (Here, κ ranges
over variables and function names.) We assume that the (base-type)variables appearing free in the types and the formulas in Γ are indom(Γ), that is, (⋃θ∈Γ fv(θ) ∪ ⋃κ∶τ ∈Γ fv(τ )) ⊆ dom(Γ).

We use the meta variable ρ to denote substitutions from variables
to values (ρ does not map function names). (Recall that values areclosed.) We define ρ(e), ρ(θ), and ρ(τ ) in the obvious way. We
define ρ(Γ) to be the environment with each θ ∈ Γ replaced byρ(θ) and each κ ∶ τ ∈ Γ replaced by κ ∶ ρ(τ ). We let ρ↾base
denote the restriction of ρ to base type variables, and ρ↾fn denote
the restriction of ρ to function type variables. Note that, because theformulas and the types only have base-type variables, substitution
over the formulas can be restricted to base-type variables (i.e.,ρ(θ) = ρ↾base (θ) and ρ(τ ) = ρ↾base (τ )).
4.3 Semantics of Type and EffectWe define the semantics of type and effect for the purpose ofdefining the notion of valid oracles that can be used in the typesystem and for formalizing the soundness of the type system. Informally, the type and effect semantics JΘ ⊢ τ & ΦKP is the setof expressions of the program P whose evaluation causes (finite
and infinite) sequences of events in Φ, and if terminates, results
in a value of the type τ , when the free variables in the expression are substituted the values of the types Θ. Figure 6 formallydefines JΘ ⊢ τ & ΦKP . Here, ρ ⊧P Θ denotes that 1.) dom(ρ) =dom(Θ), 2.) ⊧ ρ↾base (JΘKbase ), and 3.) ∀x ∈ dom(ρ↾fn ).ρ(x) ∈Jρ(Θ(x))KP .
Note that the definition uses the auxiliary notion Jτ K which
represents the set of values of the type. As with the evaluation
relations, we omit the subscript P and write JΘ ⊢ τ & ΦK, Jτ K, andρ ⊧ Θ when the program is clear from the context.
4.4 Oracle
We formalize oracle as follows.
Definition 4.1 (Oracle). An oracle ▸P is a 4-ary relation thatsatisfies Θ ▸P e ∶ τ & Φ ⇒ e ∈ JΘ ⊢ τ & ΦKP , for any expression
e of P .
That is, an oracle is simply defined to be an entity that derives
semantically correct judgements for the program’s expressions. In
fact, by the type soundness theorem (Theorem 4.1), our type systemitself is a valid oracle. As before, we write Θ ▸ e ∶ τ & Φ forΘ ▸P e ∶ τ & Φ when P is clear from the context.
4.5 Typing Rules
Figure 7 shows the typing rules. A typing judgement for expressions is of the form Γ ⊢ e ∶ τ &Φ expressing that the under the environment Γ, e has type τ with the effect Φ. We write Γ ⊢ e ∶ τ when
there exists some Φ such that Γ ⊢ e ∶ τ & Φ. The type judgements
are implicitly parameterized by the program being typed (used in
the rule Program, and in Oracle for Θ ▸ e ∶ τ & Φ).
We implicitly assert that a type assigned to an expression conforms to the expression’s simple type. More formally, the simpletype shape of τ is the simple type stsh(τ ) defined such thatΦ
stsh(x∶σ Ð→ τ ) = stsh(σ) → stsh(τ ), and stsh({u∶B ∣ θ}) = B.

e ∈ JΘ ⊢ τ & (Ξ, Π)KP⇔

∀ρ.ρ ⊧P Θ ⇒(∀v, ̟.ρ(e) ⇓P v & ̟ ⇒ v ∈ Jρ(τ )KP ∧ ̟ ∈ Ξ)∧(∀π.ρ(e) ⇑P  & π ⇒ π ∈ Π)c ∈ J{u∶B ∣ θ}KPΦ
λx.e ∈ Jx∶τ Ð
→ σKP

⇔
⇔

c ∈ B∧ ⊧ θ[c/u]e ∈ Jx∶τ ⊢ σ & ΦKP

Figure 6: Semantics of type and effect.

Θ▸e∶τ &Φ
Oracle∆, Θ ⊢ e ∶ τ & ΦΓ ⊢ e ∶ τ1 & Φ1 Γ ⊢ τ1 ≤ τ2
Γ ⊢ e ∶ τ & Φ1 Γ ⊢ e ∶ τ & Φ2Comb
Γ ⊢ e ∶ τ & Φ1 ∩ Φ2
Γ ⊢ e ∶ τ2 & Φ2sty(x) = B
c∈B
VaB
Const
Γ ⊢ c ∶ {u∶B ∣ u = c} & ({ε}, ∅)Γ ⊢ x ∶ {u∶B ∣ u = x} & ({ε}, ∅)Φ1 ⊆ Φ2Sub

sty(x) ∈→VaFΓ ⊢ x ∶ Γ(x) & ({ε}, ∅)Φ1Φ2

Γ ⊢ x ∶ τ1 Γ ⊢ y ∶ τ2 ty(op) = x1 ∶τ1 Ð→ x2 ∶τ2 Ð→ τ3
OpFun
Γ ⊢ F ∶ er (Γ(F)) & ({ε}, ∅)Γ ⊢ x op y ∶ τ3 [x/x1 ][y/x2 ] & ({ε}, ∅)Γ, x ∶ τ1 ⊢ e ∶ τ2 & Φ

Φ

Lam

Φ

→ τ2 & ({ε}, ∅)Γ ⊢ λx.e ∶ x∶τ1 Ð→ τ2 Γ ⊢ y ∶ τ1
Γ ⊢ x ∶ z∶τ1 ÐAppΓ ⊢ x y ∶ τ2 [y/z] & ({step}, ∅) ⋅ ΦΓ ⊢ e ∶ τ & Φ ⊧ JΓKbase ⇒ Γ, x = true ⊢ e1 ∶ τ & Φ1 Γ, x = false ⊢ e2 ∶ τ & Φ2
UnreachIfΓ ⊢ if x then e1 else e2 ∶ τ & Φ1 ∪ Φ2
Γ ⊢ e ∶ τ & (∅, ∅)Γ ⊢ e1 ∶ τ1 & Φ1
Γ, x ∶ τ1 ⊢ e2 ∶ τ2 & Φ2
∀F x̄ = e ∈ P.Γ ⊢ λx̄.e ∶ Γ(F)ProgramEventLetΓ ⊢ let x = e1 in e2 ∶ τ2 & Φ1 ⋅ Φ2
Γ ⊢ ev[a] ∶ unit & ({a}, ∅)Γ⊢⋆Figure 7: Typing rules.
Then, we assert that any type τ assigned to e in a type derivation
satisfies sty(e) = stsh(τ ).
We describe each rule. Oracle allows information derived by
an external oracle to be used in the typing derivation. For example,
consider the function below.

er ({u∶B ∣ θ}) = {u∶B ∣ θ}(Ξ,Π)(Ξ,Σω )er (x∶σ ÐÐÐ→ τ ) = x∶σ ÐÐÐÐ→ er (τ )Figure 9: er (τ ).

f0 x = ev[a]; if x = 0 then () else f0 (x − 1)
A termination verifier for functional programs [21] may be used as
an oracle to derive ▸ f0 ∶ τf0 & (∅, ∅) where(Σ∗ ,∅)

τf0 = x∶{u∶int ∣ u ≥ 0} ÐÐÐÐ→ unit
With this, Oracle can derive that f0 ∶ τf0 ⊢ f0 ∶ τf0 & (∅, ∅).
Note that τf0 states that, given a non-negative integer argument, f0
has no non-terminating event traces (i.e., it terminates), but may
have arbitrary terminating event traces (i.e., the termination oracle
says nothing beyond the fact that the function terminates on nonnegative inputs).
Comb combines information from multiple derivations. Whileinnocuous, the rule is essential for incorporating the facts derived
by an oracle or combining the facts from multiple oracles. For
example, as we show below, App and Sub can be used to derivethat
f0 ∶τf0 , x∶{u∶int ∣ u ≥ 0} ⊢ f0 x ∶ unit & (Σ∗ , ∅)in the example above. That is, the call to f0 with a non-negative
integer argument terminates. Then, a safety oracle may be used toderive via Oracle (alternatively, the type system can derive such asafety judgement by itself):
f0 ∶τf0 , x∶{u∶int ∣ u ≥ 0} ⊢ f0 x ∶ unit & ({step, a}∗ , Σω )which says that the function call only generates either step or a
event, if it terminates. Note that this judgement gives no information about the non-termination behavior. Then, Comb may combine the two judgements to derive:f0 ∶τf0 , x∶{u∶int ∣ u ≥ 0} ⊢ f0 x ∶ unit & ({step, a}∗ , ∅)which says that the function call only generates terminating event
traces consisting of step and a.
Sub is the subsumption rule for subtypes and sub-effects. The
subtyping rules are defined in Figure 8. The rule is an extension of
the one used in the previous work on refinement type systems [6,16, 19, 26, 29, 31] with the usual rule for sub-effecting that allow alarger effect to be used in place of a smaller effect.
Const, VaB, and VaF for typing constants and variables are
straightforward extension of those from the previous work on refinement type systems. Here, → denotes the set of function-type
simple types. Looking up a variable generates no non-terminating
effects (i.e., ∅) because the operation is guaranteed to terminate,
whereas it generates an empty terminating event sequence (i.e.,{ε}).
Fun looks up the type of a recursive function name in the typeenvironment. The rule is similar to VaF, except that the type in
the conclusion is er (Γ(F)) instead of Γ(F). Informally, er (τ )“erases” the non-terminating parts of the top-level effects of τ byreplacing them with Σω . This prevents the type system from deriving non-trivial facts about non-terminating runs by itself (i.e.,
without the help of an oracle), and is needed to ensure the typesystem’s soundness. For example, suppose er (Γ(F)) in the conclusion of Fun was replaced by Γ(F). Then, for the program{. . . , loop x = loop x}, we would be able to derive Γ ⊢ ⋆ where(Σ∗ ,∅)

Γ(loop) = x∶int ÐÐÐÐ→ unit, which says that a call to loop generates no infinite event traces, that is, it terminates. This is obviously incorrect as any call to loop diverges. The erasure prevents
such unsound non-termination effects from occurring. We formallydefine er (τ ) in Figure 9.
Op types constant operator applications. Here, ty(op) is thesound constant operator type of op. Formally, a sound constantoperator type of op is defined to be a closed type of the form({ε},∅)({ε},∅)

x1 ∶B1 ÐÐÐÐ→ x1 ∶B2 ÐÐÐÐ→ {u∶B3 ∣ θ}that satisfy the following:● op is a binary operator from the arguments of the type B1 andB2 to the return value of the type B3 .
● For constants c1 and c2 of the type B1 and B2 and c3 =JopK(c1 , c2 ), ⊧ θ[c1 /x1 ][c2 /x2 ][c3 /u].
({ε},∅)({ε},∅)

would like to prove that the call to H with any integer argument terminates. The property can be expressed as the type(Σ∗ ,∅)

τH = x∶int ÐÐÐÐ→ unit, and we try to derive that H ∶ τH ⊢ ⋆.
But, this cannot be done without Oracle because any occurrenceof H in the derivation will have its type’s top-most non-terminating
effect “erased”. (Trivially, soundness holds even if the Oracle rule
is removed from the type system.)

5. Examples
In this section we illustrate how our technique operates through avariety of instantiations on examples. Note there are no existing
techniques to prove that the following properties hold over theirrespective programs. For illustrative purposes, some examples are
first order however, of course, the power of our technique is that it
applies to higher order programs. In this section we have made all
events explicit.
In the R EDUCE example in Figure 10, we rely on a termination
oracle to tell us that explore terminates when it’s given a certain
type of R:(step+ ,)Γ, R ∶ {i ∶ int ∣ true} ÐÐÐÐ→ {j ∶ int ∣ j < i}⊢ explore x R ∶ unit & (⊺, )
We also obtain safety information from the type system:

For example, x ∶ int ÐÐÐÐ→ y∶int ÐÐÐÐ→ {u∶int ∣ u = x + y}is a sound type for the integer addition operator +Lam types function definitions, and App types function applications. The rules are extensions of the ones in the previous workon refinement type systems with the usual type-and-effect approachof recording and discharging the latent effect. As remarked in Section 3, the step event guard is used to prevent non-productive nonterminating runs.
If types conditional branches. Per previous work on refinement
type systems, each branch is typed with the assumption about thebranch condition added to the type environment (i.e., x = true
and x = false). Unreach allows the type system to derive that e
generates no effects in an unreachable context (i.e., when JΓKbase
is unsatisfiable).
Let types let bindings. Note that the effect Φ1 of e1 is appended
to the effect Φ2 of e2 . Event types event raising operations and isself-explanatory. Continuing the function f0 example from above,
we may use Let and Event to derive that

Via the Sub rule, we can rewrite the combination (Comb) of these
two rules and conclude that the body of main has effect F(done).
Note that the termination oracle here need only be used to show that
explore is not called infinitely often (whole program termination
reasoning is not needed).
The RUMBLE example illustrates modular reasoning. Here weagain use a termination oracle to tell us that rumble terminates regardless of input, but we use it to refine the safety information differently. Our type system can conclude that the innermost application in main has (finitely many) step events:f0 ∶τf0 , x∶{u∶int ∣ u ≥ 0} ⊢ f0 x; ev[b] ∶ unit & (Ξ0 , ∅)

Γ ⊢ rumble b a ∶ ... & ((step ∣ rumble)+ , ).

where Ξ0 = {step, a}∗ ⋅ {b}. That is, f0 x; ev[b] only generates
finite sequences of step and a that end in b, which is the property(step ∨ a)Ub in LTL.
Finally, Program types the program P (implicit in the rules)
by asserting that each of the recursive functions have types of their
fixpoints. We state the soundness of the type system.

(We have omitted the refinement typing, which is not relevant here.)We then use the App, Oracle and Comb rules again to obtain

Theorem 4.1 (Soundness). Suppose ∆ ⊢ ⋆, dom(Θ) = fv(e), and∆, Θ ⊢ e ∶ τ & Φ. Then, e ∈ JΘ ⊢ τ & ΦK
Proof. Please see our technical report [20] for detail.

◻

The following is immediate from Oracle, and states that thetype system is complete relative to the oracle.
Theorem 4.2 (Relative Completeness). Suppose Θ ▸ e ∶ τ & Φ.
Then, ∆, Θ ⊢ e ∶ τ & Φ.
We note that, without Oracle, the type system cannot prove
non-trivial liveness properties (i.e., properties about non-terminatingruns) in presence of recursive functions. For example, let P ={H y = if y ≤ 0 then () else H (y − 1)} and suppose that we(step+ ,)Γ, R ∶ {i ∶ int ∣ true} ÐÐÐÐ→ {j ∶ int ∣ j < i}⊢ explore x R ∶ unit & ((explore ∣ step)∗ ⋅ done, ⊺)Γ ⊢ rumble b a ∶ ... & ((step ∣ rumble)+ , ⊺)We use the Comb rule to combine this with information from thetermination oracle to obtainΓ ⊢ rumble a (rumble b a) ∶ ... & ((step ∣ rumble)+ , ).
Finally, we consider the application of print to obtainΓ ⊢ main... ∶ ... & ((step ∣ rumble)+ ⋅ print, )which entails F(print). A benefit of our type system is illustrated
here: information from an oracle can be reused.
E VENTUALLY G LOBALLY demonstrates nesting of G within F.
To prove this example, we combine a few facts:
1. A termination oracle tells us that bar terminates.
2. We can indicate that bar always returns a non-positive number
with the dependent typing:((bar∣step)+ ,⊺)Γ ⊢ bar ∶ int ÐÐÐÐÐÐÐ→ {j ∶ int ∣ j ≤ 0} & ...
3. The type-and-effect system can conclude, with the help of anontermination oracle that foo x does not terminate when x ≤ 0
and that its infinite behavior will be (foo ∣ step)ω which is a
fixpoint of α = foo ∧ Xα:
Γ, x ∶ {j ∶ int ∣ j ≤ 0} ⊢ foo x ∶ ... & (, (foo ∣ step)ω )R EDUCE
let rec done =ev[done]and reduce x R =if x ≤ 0 then x
else R x
let rec explore x R =ev[explore] ;let y = reduce x R in
if y ≤ 0 then done ()else explore y R
let main() =let t = * in
explore t (λx. x - 2)
Φ = F(done)

RUMBLE
let rec print int x =ev[print] ; ...
and rumble x y =ev[rumble] ;if x < y thenif * thenrumble (x+1) yelse rumble x (y-1)
else xE VENTUALLY G LOBAL
let rec halt =ev[halt]
and bar x = ev[bar] ;if x > 0 then bar (x-2)
else xlet main() =let a = * inlet b = * inprint (rumble a(rumble b a))
Φ = F(print)

let main () =let t = * in
if * then foo 0
else foo (bar t)

and foo x = ev[foo] ;if (x ≤ 0) then foo x
else halt ()Φ = FG(foo ∨ step)

A LTERNATE I NEVITABILITY
let app f x i = f x (λ t. t - i)let ha1 = ev[ha1]
let ha2 = ev[ha2]let rec walk x f = ev[walk] ;if x = 0 then x else walk (f x) f
and run x f = ev[run] ;if x = 0 then x
else run (f (f x)) f
and life x =if * thenev[p];
if x<0 then ha1 (app walk x 1)
else ha2 (app run x 1)
else life x
let main() = life *Ξ = G(p ⇒ X(walkUha1 ∨ runUha2))

Figure 10: Example programs and corresponding properties (abbreviated in LTL).
We combine all of this information together to show that the foo
call sites in main satisfy F(G(foo ∨ step)).
For A LTERNATE I NEVITABILITY, ultimately we need to showthat the finite traces of life x satisfies G(p ⇒ X(walkUha1 ∨runUha2)). We elide detail related to step events. We begin with
the inner if/else in life. In the then branch, app applies the function
walk on argument x and on a function that subtracts by one. An
oracle can show that this terminates:

One solution is G(p ⇒ X(walkUha1 ∨ runUha2)). Somethingcritical here was that we had complete knowledge of all instanceswhere p was generated. Because our type-and-effect system canmaintain precise descriptions of the event traces, we can build thisup syntactically over the body of life.

goal of proving an overall (exogenous) specification, by composing
together pieces of reasoning.
We are not the first to suggest a type-and-effect system for verifying temporal properties. Skalka et al. [27, 28] describe a typeand-effect system where event traces are effects, similar to oursystem. However, unlike our system, they use the type-and-effectsystem only to infer an over-approximation of the program’s actual event traces, which is then checked against the target temporal
property by an external model checker.2 Their approach precludes
the possibility of verifying non-trivial liveness properties, because a
type-and-effect system alone is inherently “safety”, and having an
up-front type-and-effect abstraction can result in losing the information needed for liveness reasoning. By contrast, our type-andeffect system allows the use of temporal property verifiers inside
the type derivation as oracles, enabling compositional verificationof non-trivial temporal properties.
A different approach to using a type system for temporal property verification has been proposed by Kobayashi and Ong [18]. In
their approach, the type system is used internally to define a parity
game (i.e. a “move” in the game is defined as a typability relation),and the verification problem is reduced to the problem of finding
a winning strategy to the game. Our approach is conceptually thedual of theirs, and allows verifiers to be used as oracles inside thetype system. Also, unlike our approach, their approach is limited to
the verification of finite data programs (given in CPS), and it may
be difficult to extend the approach to infinite data programs.

6. Related work

7. Conclusion

To the best of our knowledge, our work is the first technique thatis able to prove temporal properties of higher-order, infinite-data
programs. In Sections 1 and 2 we summarized previous efforts thatare restricted in one way or another (e.g. only finite-data, safetyonly, termination-only, or works that are restricted to first-orderprograms). We now discuss some other related works.
In our work we strive to achieve exogenous verification in that
we are attempting to verify an overall external behavior of a program, as opposed to endogenous verification (e.g. Floyd/Hoare
Logic), which is more directly connected to system internals suchas program location. However, we use an endogenous type-andeffect system, combined with generalizing composed effects. In
their work, Barringer et al. [3] extend temporal logic with a composition operator. Their work, however, is geared toward compositional user-provided (endogenous) specifications rather than our

We have introduced the first technique that enables us to verify temporal properties of higher-order, infinite-data programs. Our typeand-effect system accomplishes this by decomposing the program,not only into expressions, but also based on the behavior of each
expression’s finite versus infinite event behaviors. The type systemitself is strong enough to derive temporal safety properties which
can be combined with liveness information from oracles. We believe this work will serve as a theoretical foundation toward automatic verification of not only higher-order programs, but also provides a new route to more compositional verification of first-orderprograms.

Γ ⊢ walk ∶(⊺,)x ∶ int Ð→ f ∶ (i ∶ int Ð→ {j ∶ int ∣ j < i}) ÐÐÐ→ int
Similar for run. Combining this information with a safety judgmentthat walk generates walk∗ , and using the App rule to append theha1 event, we have summarized the effects of the then branch. We
do the same for the else branch, and then with the semi-colon rule,
we obtain (p ⇒ X(walkUha1 ∨ runUha2)) for the then branchof the outer if/else expression. The else branch is another call to life
x, so we look for a fixpoint toα = α ∨ (p ⇒ X(walkUha1 ∨ runUha2))

2 For this reason, they use BPA as the concrete model of effects, whereas

we keep the effect representation intentionally abstract.

References[1] A LUR , R., AND C HAUDHURI , S. Temporal reasoning for procedural
programs. In Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’10)(2010), vol. 5944, pp. 45–60.
[2] BALL , T., AND R AJAMANI , S. K. Automatically validating temporal safety properties of interfaces. In Proceedings of the 8th International SPIN Workshop on Model Checking Software (2001), vol. 2057,
pp. 103–122.
[3] BARRINGER , H., K UIPER , R., AND P NUELI , A. Now you may
compose temporal logic specifications. In Proceedings of the 16th
Annual ACM Symposium on Theory of Computing (STOC ’84) (1984),
pp. 51–63.
[4] B EYENE , T., P OPEEA , C., AND RYBALCHENKO , A. Solving existentially quantified horn clauses. In Proceedings of the 25th International
Conference on Computer Aided Verification (CAV’11) (2013).
[5] B EYER , D., H ENZINGER , T. A., J HALA , R., AND M AJUMDAR , R.
The software model checker blast. STTT 9, 5-6 (2007), 505–525.
[6] B HARGAVAN , K., F OURNET, C., AND G ORDON , A. D. Modular
verification of security protocol code by typing. In The 37th Annual
ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL’10) (2010), pp. 445–456.
[7] C LARKE , E. M., G RUMBERG , O., J HA , S., L U , Y., AND V EITH ,H. Counterexample-guided abstraction refinement. In Proceedingsof the 12th International Conference on Computer Aided Verification(CAV’00) (2000), vol. 1855, pp. 154–169.
[8] C OOK , B., G OTSMAN , A., P ODELSKI , A., RYBALCHENKO , A.,
AND VARDI , M. Y. Proving that programs eventually do something
good. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’07) (2007),
pp. 265–276.
[9] C OOK , B., AND KOSKINEN , E. Making prophecies with decisionpredicates. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11) (2011),
ACM, pp. 399–410.
[10] C OOK , B., AND KOSKINEN , E. Reasoning about nondeterminism
in programs. In Proceedings of the 34th ACM SIGPLAN Conference
on Programming Language Design and Implementation (PLDI’13)(2013), ACM.
[11] C OOK , B., KOSKINEN , E., AND VARDI , M. Temporal verification asa program analysis task [extended version]. Formal Methods in System
Design (2012).
[12] C OOK , B., KOSKINEN , E., AND VARDI , M. Y. Temporal property
verification as a program analysis task. In Proceedings of the 23rd
International Conference on Computer Aided Verification (CAV’11)(2011), vol. 6806, pp. 333–348.
[13] C OOK , B., P ODELSKI , A., AND RYBALCHENKO , A. Termination
proofs for systems code. In Proceedings of the ACM SIGPLAN 2006
Conference on Programming Language Design and Implementation(PLDI’06) (2006), pp. 415–426.
[14] C OUSOT, P., AND C OUSOT, R. Inductive definitions, semantics
and abstract interpretation. In Proceedings of the 19th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1992), R. Sethi, Ed., ACM Press, pp. 83–94.
[15] G ASTIN , P., AND O DDOUX , D. Fast LTL to Büchi automata translation. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV’01) (2001), pp. 53–65.

[16] J HALA , R., M AJUMDAR , R., AND RYBALCHENKO , A. HMC: Verifying functional programs using abstract interpreters. In Proceedingsof the 23rd International Conference on Computer Aided Verification(CAV’11) (2011).
[17] J OHNSSON , T. Lambda lifting: Transforming programs to recursive
equations. In FPCA (1985), pp. 190–203.
[18] KOBAYASHI , N., AND O NG , C.-H. L. A type system equivalent
to the modal mu-calculus model checking of higher-order recursion
schemes. In Proceedings of the 24th Annual IEEE Symposium on
Logic in Computer Science (LICS’09) (2009), pp. 179–188.
[19] KOBAYASHI , N., S ATO , R., AND U NNO , H. Predicate abstraction
and cegar for higher-order model checking. In Proceedings of the
32nd ACM SIGPLAN Conference on Programming Language Design
and Implementation (PLDI’11) (2011), pp. 222–233.
[20] KOSKINEN , E., AND T ERAUCHI , T. Local temporal reasoning. Tech.
Rep. 966, New York University, 2014.
[21] K UWAHARA , T., T ERAUCHI , T., U NNO , H., AND KOBAYASHI , N.
Automatic termination verification for higher-order functional programs. In Proceedings of the 22nd European Symposium on Programming (ESOP’14) (2014), vol. 7792, pp. 1–20.
[22] L EDESMA -G ARZA , R., AND RYBALCHENKO , A. Binary reachability
analysis of higher order functional programs. In Proceedings of the
19th International Symposium on Static Analysis (SAS’12) (2012),
vol. 7460, pp. 388–404.
[23] L EROY, X., AND G RALL , H. Coinductive big-step operational semantics. Inf. Comput. 207, 2 (2009), 284–304.
[24] M C M ILLAN , K. L. Lazy abstraction with interpolants. In CAV’06(2006), T. Ball and R. B. Jones, Eds., vol. 4144, pp. 123–136.
[25] P ODELSKI , A., AND RYBALCHENKO , A. A complete method for thesynthesis of linear ranking functions. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract
Interpretation (VMCAI’04) (2004), vol. 2937, Springer, pp. 239–251.
[26] RONDON , P. M., K AWAGUCHI , M., AND J HALA , R. Liquid types.
In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI’08) (2008), ACM,
pp. 159–169.
[27] S KALKA , C., AND S MITH , S. F. History effects and verification.
In Proceedings of Programming Languages and Systems: Second
Asian Symposium, (APLAS 2004) (2004), W.-N. Chin, Ed., vol. 3302,
Springer, pp. 107–128.
[28] S KALKA , C., S MITH , S. F., AND H ORN , D. V. Types and trace
effects of higher order programs. J. Funct. Program. 18, 2 (2008),
179–249.
[29] T ERAUCHI , T. Dependent types from counterexamples. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages (POPL’10) (2010), ACM, pp. 119–130.
[30] T HOMAS , W. Handbook of theoretical computer science (vol. b). MIT
Press, Cambridge, MA, USA, 1990, ch. Automata on Infinite Objects,
pp. 133–191.
[31] U NNO , H., T ERAUCHI , T., AND KOBAYASHI , N. Automating relatively complete verification of higher-order functional programs. In
Proceedings of the 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’13) (2013), pp. 75–86.
[32] X I , H., AND P FENNING , F. Dependent types in practical programming. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’99) (1999),
pp. 214–227.

A. Proof of Theorem 4.1(3) ∆, Θ ⊢ e ∶ τ & (Ξ, Π)We add to the type system an “the-all-knowing oracle” rule that canderive arbitrary semantically true judgements:

Then, e ∈ JΘ ⊢ er (τ ) & (Ξ, Σω )K.
Proof. First, note that the statement is equivalent to the following.

e ∈ JΘ ⊢ τ & ΦK
All∆, Θ ⊢ e ∶ τ & Φ(a) Suppose (1), (2), (3), ρ ⊧ Θ, and ρ(e) ⇓ v & ̟. Then, ̟ ∈ Ξ
and v ∈ Jρ(er (τ ))K.

We state a few lemmas regarding subtyping.
Lemma A.1 (≤ Transitivity). Suppose Γ ⊢ τ1 ≤ τ2 and Γ ⊢ τ2 ≤
τ3 . Then, Γ ⊢ τ1 ≤ τ3 .
Lemma A.2 (≤ Substitution). Suppose ∆, Θ ⊢ τ ≤ σ, and ρ ⊧ Θ.
Then, ∆ ⊢ ρ(τ ) ≤ ρ(σ).
Lemma A.3. Suppose Γ, x ∶ τ ⊢ σ ′ ≤ σ and Γ ⊢ τ ′ ≤ τ . Then,Γ, x∶τ ′ ⊢ σ ′ ≤ σ.
Lemma A.4. Suppose Γ, x ∶ τ ⊢ e ∶ τ & Φ and Γ ⊢ τ ′ ≤ τ . Then,Γ, x∶τ ′ ⊢ e ∶ τ & Φ.
Lemma A.5 (≤ Semantic Correspondence I). Suppose ∆, Θ ⊢ τ ≤τ ′ and ρ ⊧ Θ. Then, Jρ(τ )K ⊆ Jρ(τ ′ )K.
Proof. We prove by induction on the structure of τ .
Case τ = {u∶B ∣ θ}
By Lemma A.2, ∆ ⊢ ρ(τ ) ≤ ρ(τ ′ ). By Lemma A.1 andinspection of the subtyping rules, it must be the case that τ ′ ={u∶B ∣ θ′ } and ⊧ ρ(θ) ⇒ ρ(θ′ ). Therefore, Jρ(τ )K ⊆ Jρ(τ ′ )K.
ΦCase τ = x∶σ1 Ð→ σ2
By Lemma A.2, ∆ ⊢ ρ(τ ) ≤ ρ(τ ′ ). By Lemma A.1 andinspection of the subtyping rules, it must be the case that τ ′ = x∶Φ′

σ1′ Ð→ σ2′ , ∆ ⊢ ρ(σ1′ ) ≤ ρ(σ1 ), ∆, x∶ρ(σ1′ ) ⊢ ρ(σ2 ) ≤ ρ(σ2′ ),and Φ ⊆ Φ′ .
Let λx.e ∈ Jρ(τ )K. By definition, e ∈ Jx∶ρ(σ1 ) ⊢ ρ(σ2 ) & ΦK.
It suffices to show that e ∈ Jx∶ρ(σ1′ ) ⊢ ρ(σ2′ ) & Φ′ K (because
then λx.e ∈ Jρ(τ ′ )K). Suppose v ∈ Jρ(σ1′ )K. Then, by induction
hypothesis, v ∈ Jρ(σ1 )K. Therefore, if e[v/x] ⇓ v ′ & ̟ thenv ′ ∈ Jρ(σ2 )[v/x]K. By induction hypothesis, the latter implies
that v ′ ∈ Jρ(σ2′ )[v/x]K. Therefore, because Φ ⊆ Φ′ , it follows
that e ∈ Jx∶ρ(σ1′ ) ⊢ ρ(σ2′ ) & Φ′ K.
◻
Lemma A.6 (≤ Semantic Correspondence II). Suppose ∆, Θ ⊢τ ≤ τ ′ and Φ ⊆ Φ′ . Then, JΘ ⊢ τ & ΦK ⊆ JΘ ⊢ τ ′ & Φ′ K.

By Lemma A.7, ∆ ⊢ ρ(e) ∶ ρ(τ ) & (Ξ, Π), and so by Lemma A.8,
∆ ⊢ v ∶ ρ(τ ) and ̟ ∈ Ξ. Therefore, (a) is implied by the following.
(b) Suppose (1), ρ ⊧ Θ, and ∆ ⊢ v ∶ ρ(τ ). Then, v ∈ Jρ(er (τ ))K.
We prove (b) by induction on the structure of τ .
Case τ = {u∶B ∣ θ}
We have that ρ(er (τ )) = ρ(τ ) = {u∶B ∣ ρ(θ)}. By the definition of values, v = c for some constant c. Then, by Const,
Sub, and Lemma A.1 and the definition of sound constant type,⊧ u = c ⇒ ρ(θ). Therefore, c ∈ Jρ(θ)K.
(Ξ′ ,Π′ )Case τ = x∶σ ′ ÐÐÐÐ→ τ ′(Ξ′ ,Σω )We have that ρ(er (τ )) = x∶ρ(σ ′ ) ÐÐÐÐ→ ρ(er (τ ′ )). It must
be case that v = λx.e′ for some e′ and x. By inspection of thetyping rules, either All, Oracle, or Lam must have been applied
at v.
Case All or Oracle
By Sub and Lemma A.1, it must be the case that v ∈Jε ⊢ τ ′ & ΦK such that ∆ ⊢ τ ′ ≤ ρ(τ ).
We have that v ∈ Jτ ′ K. Therefore, by Lemma A.5, v ∈Jρ(τ )K. It is easy to see that ∆ ⊢ ρ(τ ) ≤ ρ(er (τ )).
Therefore, by Lemma A.5 again, v ∈ Jρ(er (τ ))K.
Case Lam
By Sub and Lemma A.1, it must be the case that ∆, x ∶ σ ′′ ⊢e′ ∶ τ ′′ & (Ξ′′ , Π′′ ) where● ∆ ⊢ ρ(σ ′ ) ≤ σ ′′● ∆, x∶ρ(σ ′ ) ⊢ τ ′′ ≤ ρ(τ ′ )● (Ξ′′ , Π′′ ) ⊆ (Ξ′ , Π′ )By Lemma A.4 and Sub, we have ∆, x ∶ ρ(σ ′ ) ⊢ e′ ∶ρ(er (τ ′ )) & (Ξ′ , Σω ). Therefore, by induction hypothesis(on ρ(er (τ ′ ))), we have thate′ ∈ Jx∶ρ(σ ′ ) ⊢ ρ(er (τ ′ )) & (Ξ′ , Σω )KTherefore,(Ξ′ ,Σω )λx.e′ ∈ Jx∶ρ(σ ′ ) ÐÐÐÐ→ ρ(er (τ ′ ))K

Proof. Suppose ρ ⊧ Θ, ρ(e) ⇓ v & ̟, and v ∈ Jρ(τ )K. Then, by
Lemma A.5, v ∈ Jρ(τ ′ )K. Therefore, the statement follows.
◻
Lemma A.7 (Substitution). Suppose ∆, Θ ⊢ e ∶ τ & Φ and ρ ⊧ Θ.
Then, ∆ ⊢ ρ(e) ∶ ρ(τ ) & Φ.
Proof. By induction on the derivation of ∆, Θ ⊢ e ∶ τ & Φ.

◻

Lemma A.8 (Preservation). Suppose(1) ∆ ⊢ ⋆,(2) dom(Θ) = fv(e), andTheorem 4.1: Suppose● ∆ ⊢ ⋆,
● dom(Θ) = fv(e), and● ∆, Θ ⊢ e ∶ τ & Φ

Proof. We prove by induction on the derivation of ∆, Θ ⊢ e ∶ τ &Φ.

Then, ∆ ⊢ v ∶ τ and ̟ ∈ Ξ

Lemma A.9 (Soundness Part I : Erasure). Suppose

We are now ready to prove the soundness theorem.

Then, e ∈ JΘ ⊢ τ & ΦK.

● ∆ ⊢ ⋆,● ∆ ⊢ e ∶ τ & (Ξ, Π),● e is closed, and● e⇓ v&̟

Proof. By induction on the derivation of e ⇓ v & ̟.

◻

◻

Case the last rule is Oracle
Immediate from Definition 4.1 and Oracle.
Case the last rule is Comb
It must be the case that Φ = Φ1 ∩ Φ2 where∆, Θ ⊢ e ∶ τ & Φ1 ∆, Θ ⊢ e ∶ τ & Φ2∆, Θ ⊢ e ∶ τ & Φ1 ∩ Φ2
By induction hypothesis, we have that● e ∈ JΘ ⊢ τ & Φ1 K
● e ∈ JΘ ⊢ τ & Φ2 K
Therefore, e ∈ JΘ ⊢ τ & Φ1 ∩ Φ2 K.
Case the last rule is Sub
We have

Case the last rule is Lam
Φ′
We have e = λx.e′ and τ = x∶σ ′ Ð→ τ ′ such that∆, Θ, x ∶ σ ′ ⊢ e′ ∶ τ ′ & (Ξ, Π)(Ξ,Π)∆, Θ ⊢ λx.e′ ∶ x∶σ ′ ÐÐÐ→ τ ′ & ({ε}, ∅)∆, Θ ⊢ e ∶ τ ′ & Φ′ ∆, Θ ⊢ τ ′ ≤ τ∆, Θ ⊢ e ∶ τ & Φ

Φ′ ⊆ Φ

By induction hypothesis, we have thate ∈ JΘ ⊢ τ ′ & Φ′ K
Therefore, by Lemma A.6, e ∈ JΘ ⊢ τ & ΦK.
Case the last rule is Const
We have e = c andc∈B∆, Θ ⊢ c ∶ {u∶B ∣ u = c} & ({ε}, ∅)Suppose ρ ⊧ Θ and v ∈ Jρ(σ ′ )K. Then, ρ ∪ {x ↦ v} ⊧ Θ, x∶σ ′ .
Therefore, the following holds from the induction hypothesise′ ∈ JΘ, x ∶ σ ′ ⊢ τ ′ & (Ξ, Π)K.
● If ρ(e′ )[v/x] ⇓ v ′ & ̟ then v ′ ∈ ρ(τ ′ )[v/x] and ̟ ∈ Ξ.
● If ρ(e′ )[v/x] ⇑  & π then π ∈ Π.
Therefore, by st-Val,(Ξ,Π)λx.e′ ∈ JΘ ⊢ x∶σ ′ ÐÐÐ→ τ ′ & ({ε}, ∅)K
Case the last rule is App
We have e = x y and Φ = ({step}, ∅) ⋅ (Ξ, Π) where(Ξ,Π)

Suppose ρ ⊧ Θ. Then, because c ∈ B,
ρ(c) = c ∈ J{u∶B ∣ u = c}K = Jρ({u∶B ∣ u = c})K
Therefore, by st-Val,∆, Θ ⊢ x ∶ z∶τ1 ÐÐÐ→ τ & Φ1 ∆, Θ ⊢ y ∶ τ1 & Φ2∆, Θ ⊢ x y ∶ τ [y/z] & ({step}, ∅) ⋅ (Ξ, Π)
By induction hypothesis, we have thatc ∈ JΘ ⊢ {u∶B ∣ u = c} & ({ε}, ∅)K
Case the last rules is VaB
We have e = x and(Ξ,Π)● x ∈ JΘ ⊢ z∶τ1 ÐÐÐ→ τ & Φ1 K
● y ∈ JΘ ⊢ τ1 & Φ2 K(Ξ,Π)

sty(x) = B∆, Θ ⊢ x ∶ {u∶B ∣ u = x} & ({ε}, ∅)Suppose ρ ⊧ Θ. Then, because sty(x) ∈ B, we haveρ(x) ∈ Jρ({u∶B ∣ u = x})K
Therefore, by st-Val, we havex ∈ JΘ ⊢ {u∶B ∣ u = x} & ({ε}, ∅)K
Case the last rule is VaF
We have e = x andsty(x) ∈→∆, Θ ⊢ x ∶ Θ(x) & ({ε}, ∅)Suppose ρ ⊧ Θ. Then, because sty(x) ∈→,ρ(x) ∈ Jρ(Θ(x))K
Therefore, by st-Val, x ∈ JΘ ⊢ Θ(x) & ({ε}, ∅)K.
Case the last rule is Fun
Immediate by Lemma A.9 and st-Fun.
Case the last rule is Op
We have e = x op y andΦ1Φ2ty(op) = x1 ∶τ1 Ð→ x2 ∶τ2 Ð→ τ3∆, Θ ⊢ x ∶ τ1 & Φ′1 ∆, Θ ⊢ y ∶ τ2 & Φ′2∆, Θ ⊢ x op y ∶ τ3 [x/x1 ][y/x2 ] & ({ε}, ∅)By the definition of the sound constant operator type, τ1 ={u∶B1 ∣ ⊺} and τ2 = {u∶B2 ∣ ⊺}, and τ3 = {u∶B3 ∣ θ} for some
B1 , B2 ,B3 , and θ.
Suppose ρ ⊧ Θ. By simple typing of x and y (or by induction
hypothesis), we have ρ(x) ∈ B1 and ρ(y) ∈ B2 . By thedefinition of sound constant operator type, if ρ(x) op ρ(y) ⇓c & ε, then c ∈ B3 and ⊧ θ[ρ(x)/x1 ][ρ(y)/y2 ][c/u]. Because
fv(θ) ⊆ {u, x1 , x2 }, it follows thatc ∈ Jρ({u∶B3 ∣ θ}[x/x1 ][y/x2 ])K
Therefore, by st-Op, x op y ∈ JΘ ⊢ τ3 [x/x1 ][y/x2 ] & ({ε}, ∅)K.

Suppose ρ ⊧ Θ. Then, ρ(x) ∈ Jz∶ρ(τ1 ) ÐÐÐ→ ρ(τ )K andρ(y) ∈ Jρ(τ1 )K. Let ρ(x) = λz.e′ . Then,e′ ∈ Jz∶ρ(τ1 ) ⊢ ρ(τ ) & (Ξ, Π)K
Therefore, the following holds.
● If e′ [ρ(y)/z] ⇓ v & ̟ then v ∈ ρ(τ )[ρ(y)/z] and ̟ ∈ Ξ.
● If e′ [ρ(y)/z] ⇑  & π then π ∈ Π.
Therefore, by st-App, snt-App, and the definition of trace set
concatenation, it follows thatx y ∈ JΘ ⊢ τ [y/z] & ({step}, ∅) ⋅ Φ′ K
Case the last rule is If
We have e = if x then e1 else e2 and Φ = Φ1 ∪ Φ2 where∆, Θ, x = true ⊢ e1 ∶ τ & (Ξ1 , Π1 )∆, Θ, x = false ⊢ e2 ∶ τ & (Ξ2 , Π2 )∆, Θ ⊢ if x then e1 else e2 ∶ τ & (Ξ1 , Π1 ) ∪ (Ξ2 , Π2 )By induction hypothesis, we have that● e1 ∈ JΘ, x = true ⊢ τ & Φ1 K
● e2 ∈ JΘ, x = false ⊢ τ & Φ2 K
Suppose ρ ⊧ Θ. Then, by simple typing of x, either ρ(x) = trueor ρ(x) = false. Suppose ρ(x) = true. (The case ρ(x) = false
is analogous.) Then, ρ ⊧ Θ, x = true. Therefore, the following
holds from e1 ∈ JΘ, x = true ⊢ τ & Φ1 K.
● If ρ(e1 ) ⇓ v & ̟ then v ∈ ρ(τ )[ρ(y)/z] and ̟ ∈ Ξ1 .
● If ρ(e1 ) ⇑  & π then π ∈ Ξ1 .
Therefore, by st-If1, st-If2, snt-If1, and snt-If2,
if x then e1 else e2 ∈ JΘ ⊢ τ & (Ξ1 , Π1 ) ∪ (Ξ2 , Π2 )KCase the last rule is UnreachWe have∆, Θ ⊢ e ∶ τ & Φ ⊧ J∆, ΘKbase ⇒ ∆, Θ ⊢ e ∶ τ & (∅, ∅)It must be the case that ⊧ JΘKbase ⇒ . Therefore, for all ρ,¬ρ ⊧ Θ. Therefore, e ∈ JΘ ⊢ τ & (∅, ∅)K holds vacuously.
Case the last rule is Let
Analogous to Lam and App.

Case the last rule is Event
We have e = ev[a] where∆, Θ ⊢ ev[a] ∶ unit & ({a}, ∅)Suppose ρ ⊧ Θ. Then, ρ(ev[a]) = ev[a] and by st-Ev,
ev[a] ⇓ () & a. Therefore, by Const and Sub, ev[a] ∈JΘ ⊢ unit & ({a}, ∅)K.
◻