Propositional Dynamic Logic forHigher-Order Functional Programs
Yuki Satake and Hiroshi Unno
University of Tsukuba{satake,uhiro}@logic.cs.tsukuba.ac.jp

Abstract. We present an extension of propositional dynamic logic called
HOT-PDL for specifying temporal properties of higher-order functional
programs. The semantics of HOT-PDL is defined over Higher-Order
Traces (HOTs) that model execution traces of higher-order programs. A
HOT is a sequence of events such as function calls and returns, equippedwith two kinds of pointers inspired by the notion of justification pointersfrom game semantics: one for capturing the correspondence between calland return events, and the other for capturing higher-order control flow
involving a function that is passed to or returned by a higher-order function. To allow traversal of the new kinds of pointers, HOT-PDL extends
PDL with new path expressions. The extension enables HOT-PDL to
specify interesting properties of higher-order programs, including stackbased access control properties and those definable using dependent refinement types. We show that HOT-PDL model checking of higher-orderfunctional programs over bounded integers is decidable via a reduction
to modal µ-calculus model checking of higher-order recursion schemes.

1

Introduction

Temporal verification of higher-order programs has been an emerging research
topic [12, 14, 18, 22–24, 26, 27, 31, 34]. The specification languages used there are(ω-)regular word languages (that subsume LTL) [12, 18, 26] and modal µ-calculus(that subsumes CTL) [14, 24, 31], which are interpreted over sequences or trees
consisting of events. (Extended) dependent refinement types are also used to
specify temporal [23, 27] and branching properties [34]. These specification languages, however, cannot suﬃciently express specifications of control flow involving (higher-order) functions. For example, let us consider the following simple
higher-order program Dtw (in OCaml syntax):
let tw f x = f (f x) in let inc x = x + 1 in let r = * in tw inc r
Here, ∗ denotes a non-deterministic integer, and the higher-order function tw :(int → int) → int → int applies its function argument f : int → int to theinteger argument x twice. For example, for r = 0, the program Dtw exhibits thefollowing call-by-value reduction sequence (with the redexes underlined).
tw inc 0 −→ (λx.inc (inc x)) 0 −→ inc (inc 0) −→∗ inc 1 −→∗ 2

Example properties of the program Dtw that cannot be expressed by the previous
specification languages are:Prop.1 If the function returned by a partial application of tw to some function(e.g., λx.inc (inc x) in the above sequence) is called with some integer n,
the function argument passed to tw (i.e., inc) is eventually called with n.
Prop.2 If the function returned by a partial application of tw to some function
is never called, then the function argument passed to tw is never called.
To remedy the limitation, we introduce a notion of Higher-Order Trace(HOT) that captures the control flow of higher-order programs and proposea dynamic logic over HOTs called Higher-Order Trace Propositional Dynamic
Logic (HOT-PDL) for specifying temporal properties of higher-order programs.
Intuitively, a HOT models a program execution trace which is a possibly
infinite sequence of events such as function calls and returns with information
about actual arguments and return values. Furthermore, HOTs are equippedwith two kinds of pointers to enable precise specification of control flow: onefor capturing the correspondence between call and return events, and the otherfor capturing higher-order control flow involving a function that is passed to or
returned by a higher-order function. The two kinds of pointers are inspired by
the notion of justification pointers from the game semantics of PCF [1, 2, 19, 20].
For the higher-order program Dtw , for r = 0, we get the following HOT Gtw :1
CC
CR

CC

CR

RC

CR

CR

call (tw, •) ret (tw, •) call (• , 0)call (• , 0) · · · ret (• , 1)call (• , 1) · · · ret (• , 2) ret(•, 2)

Here, • represents some function value, call(f, v) represents a call event of thefunction f with the argument v, and ret(f, v) represents a return event of thefunction f with the return value v. This trace corresponds to the previous reduction sequence: the call events call(tw, •), call(•, 0), call(•, 0), and call(•, 1) that
occur in the trace in this order correspond respectively to the redexes tw inc,(λx.inc (inc x)) 0, inc 0, and inc 1. The three important points here are that(1) the call events have pointers labeled with CR to the corresponding return
events ret(tw, •), ret(•, 2), ret(•, 1), and ret(•, 2), (2) the call event call(tw, •)has two pointers labeled with CC, where • represents the function argument fof tw and the pointed call events call(•, 0) and call(•, 1) represent the two calls
to f in tw, and (3) the return event ret(tw, •) has a pointer labeled with RC,
where • represents the partially-applied function λx.inc (inc x) and the pointed
call event call(•, 0) represents the call to the function.
To allow traversal of the pointers, HOT-PDL extends propositional dynamic
logic with new path expressions (see Section 3 for details). The extension enables
1

The symbol · · · indicates the omission of a subsequence. The two omitted subseCR

CR

quences are call(inc, 0) ret(inc, 1) and call(inc, 1) ret(inc, 2) in this order.

HOT-PDL to specify interesting properties of higher-order programs, including
stack-based access control properties and those definable using dependent refinement types. Here, stack-based access control is a security mechanism implemented in runtimes like JVM for ensuring secure execution of programs thathave components with diﬀerent levels of trust: the mechanism ensures that asecurity-critical function (e.g., file access) is invoked only if all the (immediate
and indirect) callers in the current call stack are trusted, or one of the callers isa privileged function and its callees are all trusted. We introduce a new variantof stack-based access control properties for higher-order programs, formalized in
HOT-PDL from the point of view of interactions among callers and callees.
Compared to the previous specification languages with respect to the expressiveness, HOT-PDL subsumes (ω-)regular languages because PDL interpreted
over words is already as expressive as them [15]. Temporal logics over nested
words [6] such as CaRet [5] and NWTL [4] can capture the correspondence between call and return events (i.e., pointers labeled with CR) but cannot capture
higher-order control flow (i.e., pointers labeled with CC and RC). Branchingproperties (expressible in, e.g., CTL), however, are out of the scope of the present
paper, and such an extension of HOT-PDL remains an interesting future direction. Dependent refinement types are often used to specify properties of higherorder programs for partial- and total-correctness verification [29, 33, 39, 40]. For
example, the following properties of the program Dtw are expressible:
Prop.3 The function yielded by applying tw to a strictly increasing function isstrictly increasing.
Prop.4 The function yielded by applying tw to a terminating function is terminating.
This paper shows that HOT-PDL can encode such dependent refinement types.
We also study HOT-PDL model checking: given a higher-order program D
over bounded integers and a HOT-PDL formula ϕ, the problem is to decide
whether ϕ is satisfied by all the execution traces of D modeled as HOTs. We
show the decidability of HOT-PDL model checking via a reduction to modalµ-calculus model checking of higher-order recursion schemes [21, 28].
The rest of the paper is organized as follows. Section 2 formalizes HOTsand explains how to use them to model execution traces of higher-order functional programs. Section 3 defines the syntax and the semantics of HOT-PDL
and Section 4 shows how to encode stack-based access control properties anddependent refinement types in HOT-PDL. Section 5 discusses HOT-PDL model
checking. We compare HOT-PDL with related work in Section 6 and conclude
the paper with remarks on future work in Section 7. Omitted proofs are givenin the extended version of this paper [30].

2Higher-Order Traces

This section defines the notion of Higher-Order Trace (HOT), which is used tomodel execution traces of higher-order programs. To this end, we first define(Σ, Γ )-labeled directed graphs and DAGs.

Definition 1 ((Σ, Γ )-labeled directed graphs). Let Σ be a finite set of nodelabels and Γ be a finite set of edge labels. A (Σ, Γ )-labeled directed graph isdefined as a triple (V, λ, ν), where V is a countable set of nodes, λ : V → Σ is anode labeling function, and ν : V × V → 2Γ is an edge labeling function. We calla (Σ, Γ )-labeled directed graph that has no directed cycle (Σ, Γ )-labeled DAG.
Note that an edge may have multiple labels. For nodes u, u′ ∈ V , ν(u, u′ ) = ∅means that there is no edge from u to u′ . We use σ and γ as meta-variables
ranging respectively over Σ and Γ . We write Vσ for the set {u ∈ ∪V | σ = λ(u)}of all the nodes labeled with σ. We also write VΣ for the set σ∈Σ Vσ . For∗u, u′ ∈ V , we write u ≺γ u′ if γ ∈ ν(u, u′ ). A binary relation ≺+γ (resp. ≺γ )denotes the transitive (resp. reflexive and transitive) closure of ≺γ .
Definition 2 (HOTs). A HOT is a (Σ, Γ )-DAG, G = (V, λ, ν) that satisfies:
TA
1. V ̸= ∅, Γ = {N, CR, CC, RC}, Σ = Σcall ⊎ Σret , and Σcall = Σcall⊎ ΣcallA ), and ≺RC ⊆ (VΣA ).
2. ≺CR ⊆ (VΣcall × VΣret ), ≺CC ⊆ (VΣcall × VΣcall× VΣcallret
3. The elements of V are linearly ordered by ≺N
4. If u ≺CR u′ and u ≺CR u′′ , then u′ = u′′ .
5. For all u′ ∈ VΣret , there uniquely exists u ∈ VΣcall such that u ≺CR u′ holds.
′
A , there uniquely exists u ∈ V such that u ≺CC u
6. For all u′ ∈ VΣcallor′u ≺RC u holds.

Intuitively, Σcall (resp. Σret ) represents a set of call (resp. return) events.
AT) represents a set of call events of top-level functions (resp.
(resp. ΣcallΣcall
functions that are returned by or passed to (higher-order) functions). u ≺N u′means that u′ is the next event of u in the trace. u ≺CR u′ indicates that u′ isthe return event corresponding to the call event u. u ≺CC u′ represents that u′ isa call event of the function argument passed at the call event u. u ≺RC u′ meansthat u′ is a call event of the partially-applied function returned at the return
event u. We call the minimum node of a HOT G with respect to ≺N the root node,denoted by 0G . For HOTs G1 and G2 , we say G1 is a prefix of G2 and write G1 ⪯G2 , if G1 is a sub-graph of G2 such that 0G1 = 0G2 . Note that the HOT Gtw in
Section 1, where N-labeled edges are omitted, satisfies the above conditions, withTA
{call(tw, •), call(inc, 0), call(inc, 1)} ⊆ Σcall, {call(•, 0), call(•, 1)} ⊆ Σcall,and {ret(tw, •), ret(inc, 1), ret(inc, 2), ret(•, 1), ret(•, 2)} ⊆ Σret .
2.1

Trace Semantics for Higher-Order Functional Programs

We now formalize our target language L, which is an ML-like typed call-by-value
higher-order functional language. The syntax is defined by(programs) D ::= {f1 7→ λx.e1 , . . . , fm 7→ λx.em }(expressions) e ::= x | f | λx.e | e1 e2 | n | op(e1 , e2 ) | ifz e1 e2 e3(values) v ::= f | λx.e | n(types) τ ::= int | τ1 → τ2
Here, x and f are meta-variables ranging respectively over term variables andnames of top-level functions. The meta-variable n ranges over the set of boundedDomains(configurations) C ::= (I, E[e])(eval. contexts) E ::= {[ ] | E e | v E | op(E, e) |}op(v, E) | ifz E e1 e2 | ret(h, i, E)
i

i

m
1
vm
(interfaces) I ::= h1 7→
v1 , . . . , hm 7→(handles) h ::= n | f | ⌊h⌋i | ⌈h⌉i(events) α ::= call(h1 , i, h2 ) | ret(h1 , i, h2 )Derivation Rulesϵ(I, E[(λx.e) v]) −→ (I, E[[v/x]e]) (App)n = [[op]](n1 , n2 )i(h 7→ v) ∈ Ii, n){ α = call(h,}i+1I ′ = I h 7→ v

(Op)(I, E[h n]) −→ (I ′ , E[ret(h, i, v n)])(I, E[ifz 0 e1 e2 ]) −→ (I, E[e1 ]) (IfZ)

v is a functioni(h 7→ v ′ ) ∈ {I
α = call(h, i,}⌊h⌋i )ϵ(I, E[op(n1 , n2 )]) −→ (I, E[n])ϵn ̸= 0(I, E[ifz n e1 e2 ]) −→ (I, E[e2 ])
ϵ

C=
⇒C
ϖ1

C −−→ CC =⇒ Cϖ ·ϖ2
C ==1==⇒C′

C −→ C ′(IfN)(Refl)′′ ϖ2′′(Tran)C ==⇒ ⊥

(I, E[h v]) −→ (I ′ , E[ret(h, i, v ′ ⌊h⌋i )])α(CFun)

α = ret(h, i, n)(RInt)(I, E[ret(h, i, n)]) −→ (I, E[n])v is a function { α = ret(h,} i, ⌈h⌉i )I ′ = I ⌈h⌉i 7→ v
0

C =
⇒⊥
ϖ·π

0

α

′

′ π

ϖ

I ′ = I h 7→ v ′ , ⌊h⌋i 7→ v
i+1

ϵ(CInt)

α(Tranω)(I, E[ret(h, i, v)]) −→ (I ′ , E[⌈h⌉i ])αϖ(RFun)

πFig. 1. Labeled Transition Relations (=⇒) and (=⇒ ) for L

integers Zb = {nmin , · · · , nmax } ⊂ Z. For simplicity of presentation, L has thetype int of bounded integers as the only base type. op represents binary operators such as +, −, ×, =, and >. The binary relations = and > return an
integer that encodes a boolean value (e.g., 1 for true and 0 for false). A program D maps each top-level function name fi to its definition λx.ei . We write
dom(D) for {f1 , . . . , fm }. We assume that D has the main function main of thetype int → int. The functions in D can be mutually recursive. Expressions
e comprise variables x, function names f , lambda abstractions λx.e, function
applications e1 e2 , bounded integers n, binary operations op(v1 , v2 ), and conditional branches ifz e1 e2 e3 . We assume that expressions are simply-typed.
As usual, the simple type system guarantees that an evaluation of a typed expression never causes a runtime type mismatch like 1 + λx.x. An expression
ifz e1 e2 e3 evaluates to e2 (resp. e3 ) if e1 evaluates to 0 (resp. a non-zero
integer). For example, the program Dtw in Section 1 is defined in L as follows:△

Dtw = {tw 7→ λf.λx.f (f x), inc 7→ λx.x + 1, main 7→ λr.tw inc r}






0

tw 7→ etw ,

△
0
I1 =
inc 7→ λx.x + 1,




0
main 7→ λr.tw inc r{}△
1
I2 = I1 main 7→ λr.tw inc r(I1 , main 0)call(main,0,0)−−−−−−−−→ (I2 , Emain [(λr.tw inc r) 0])−→ (I2 , Emain [tw inc 0])

{
}
△
1
0
I3 = I2 tw 7→ etw , ⌊tw⌋0 7→ inccall(tw,0,⌊tw⌋ )0−−−−−−−−−−→ (I3 , Etw [(λf.λx.f (f x)) ⌊tw⌋0 ])−→ (I3 , Etw [λx. ⌊tw⌋0 (⌊tw⌋0 x)]){}△0
I4 = I3 ⌈tw⌉0 7→ e′tw{}△
1
I5 = I4 ⌈tw⌉0 7→ e′twret(tw,0,⌈tw⌉0 )−−−−−−−−−→ (I4 , Emain [⌈tw⌉0 0])call(⌈tw⌉ ,0,0)0−−−−−−−−−→ (I5 , E⌈tw⌉0 [(λx. ⌊tw⌋0 (⌊tw⌋0 x)) 0])−→ (I5 , E⌈tw⌉0 [⌊tw⌋0 (⌊tw⌋0 0)]){}△1
I6 = I5 ⌊tw⌋0 7→ inc{}△
1
I7 = I6 inc 7→ λx.x + 1

call(⌊tw⌋0 ,0,0)−−−−−−−−−→ (I6 , E⌊tw⌋0 [inc 0])call(inc,0,0)−−−−−−−−→ (I7 , Einc [(λx.x + 1) 0])=⇒ (I7 , Einc [1])ret(inc,0,1)·ret(⌊tw⌋0 ,0,1)================⇒ (I7 , E⌈tw⌉0 [⌊tw⌋0call(⌊tw⌋0 ,1,1)−−−−−−−−−→ (I8 , E⌊tw⌋′0 [inc 1])

1])

}
{
△
2
I8 = I7 ⌊tw⌋0 7→ inc{}△
2
I9 = I8 inc 7→ λx.x + 1

call(inc,1,1)−−−−−−−−→ (I9 , Einc′ [(λx.x + 1) 1])=⇒ (I9 , Einc′ [2])ret(inc,1,2)·ret(⌊tw⌋0 ,1,2)·ret(⌈tw⌉0 ,0,2)·ret(main,0,2)==================================⇒ (I9 , 2)etw△

= λf.λx.f (f x)△

Emain = ret(main, 0, [ ])
△

△

e′tw

= λx. ⌊tw⌋0 (⌊tw⌋0 x)

Etw= Emain [ret(tw, 0, [ ]) 0]△△E⌈tw⌉0 = Emain [ret(⌈tw⌉0 , 0, [ ])]E⌊tw⌋0 = E⌈tw⌉0 [⌊tw⌋0 ret(⌊tw⌋0 , 0, [ ])]EincE⌊tw⌋′0 = E⌈tw⌉0 [ret(⌊tw⌋0 , 1, [ ])]△△= E⌊tw⌋0 [ret(inc, 0, [ ])]△Einc′ = E⌊tw⌋′0 [ret(inc, 1, [ ])]Fig. 2. Example Trace of Dtw

We now introduce a trace semantics of the language L, which will be usedin Section 5 to define our model checking problems of higher-order programs.
In the trace semantics, a program execution trace is represented by a sequenceof function call and return events without an explicit representation of pointers
but with enough information to construct them. We will explain how to model
traces of L as HOTs by presenting a translation.
The trace semantics[[D]] of the language
L is defined}}{ as [[D]]fin ∪ [[D]]inf
{
ϖ

π

⇒⊥
⇒ C and [[D]]inf = π (I, main n) =where [[D]]fin = ϖ (I, main n) =are respectively the sets of finite and infinite execution traces obtained by evaluating main n for some integer n using trace-labeled multi-step reduction reϖπlations=⇒ and =
⇒ , whichare presented in Figure 1, under the program I =}{0
f 7→ v (f 7→ v) ∈ D annotated with the number of calls to each function oc-curred so far (i.e., initialized to 0). There, we use ϖ (resp. π) as a meta-variableranging over finite sequences α1 · · · αm (resp. infinite sequences α1 · α2 · · · ) of
events αi . We write ϵ for the empty sequence, ϖ1 · ϖ2 for the concatenation of
the sequences ϖ1 and ϖ2 , and |ϖ| for the length of ϖ. An event α is either ofthe form call(h1 , i, h2 ) or ret(h1 , i, h2 ), where a handle h represents a top-level
function or a runtime value exchanged among functions. An event call(h1 , i, h2 )represents the (i + 1)th call to the function h1 with the argument h2 . On theother hand, an event ret(h1 , i, h2 ) represents the return of the (i + 1)th call to
the function h1 with the return value h2 . We thus equip call and return eventsof h1 with the information about (1) the number i of the calls to h1 occurredso far and (2) the runtime value h2 passed to or returned by h1 , so that we canconstruct pointers (see Definition 3 for details). Note here that handles h arealso equipped with meta-information necessary for constructing pointers. Morespecifically, h is any of the following: a bounded integer n, a top-level function
name f ∈ dom(D), the special identifier ⌊h⌋i for the function argument of the(i + 1)th call to the higher-order function h, or the special identifier ⌈h⌉i for thepartially-applied function returned by the (i+1)th call to h. We thus use handles
to track for each function value where it is constructed and how many times it
is called. We shall assume that the syntax of expressions e and values v is also
extended with handles h. As we have seen, the finite traces [[D]]fin of a program
D are collected using the terminating trace-labeled multi-step reduction relationϖ=⇒ on configurations. A configuration (I, E[e]) is a pair of an interface I and an
expression E[e] consisting of an evaluation context E and a sub-expression eunder evaluation. A special evaluation context ret(h, i, E) represents the calling
context of the (i + 1)th call to h{that waits for the return} value computed by E.
i

i

1
m
An interface I is defined to be h1 7→
v1 , . . . , hm 7→
vm that maps each function handle hj to its definition vj , where ij records the number of calls to theϖfunction hj occurred so far. In the derivation{}rules for −→, [[op]] represents theiinteger function denoted by op, and I h 7→ v represents the interface obtained

from I by adding (or replacing existing assignment to h with) the assignmentih 7→ v. In the rule CInt (resp. RInt) for function calls (resp. returns) with an
integer n, the reduction relation is labeled with call(h, i, n) (resp. ret(h, i, n)).
By contrast, in the rule CFun (resp. RFun) for function calls (resp. returns)
with a function value v, the special identifier ⌊h⌋i (resp. ⌈h⌉i ) for v is used in
the label call(h, i, ⌊h⌋i ) (resp. ret(h, i, ⌈h⌉i )) of the reduction relation, and v in
the expression is replaced by the identifier. For example, as shown in Figure 2,
the following finite trace ϖtw is generated from the program Dtw :call(main, 0, 0) · call(tw, 0, ⌊tw⌋0 ) · ret(tw, 0, ⌈tw⌉0 ) · call(⌈tw⌉0 , 0, 0)·call(⌊tw⌋0 , 0, 0) · call(inc, 0, 0) · ret(inc, 0, 1) · ret(⌊tw⌋0 , 0, 1) · call(⌊tw⌋0 , 1, 1)·call(inc, 1, 1) · ret(inc, 1, 2) · ret(⌊tw⌋0 , 1, 2) · ret(⌈tw⌉0 , 0, 2) · ret(main, 0, 2)
Similarly, the infinite traces [[D]]inf of a program D are collected using the nonπ
terminating trace-labeled reduction relation C =⇒ ⊥ on configurations. Intuπ
itively, C =⇒ ⊥ means that an execution from the configuration C diverges,

producing an infinite event sequence π. In the rule Tranω, the double horizontal line represents that the rule is interpreted co-inductively.
T
We now define the translation from traces [[D]]fin to HOTs with Σcall=
A{call(f, n), call(f, •) | f ∈ dom(D), n ∈ Zb }, Σcall = {call(•, n), call(•, •) | n ∈ Zb },and Σret = {ret(f, n), ret(f, •), ret(•, n), ret(•, •) | f ∈ dom(D), n ∈ Zb }. We
TAshall write Σ(D) for Σcall∪ Σcall∪ Σret . Note that Σ(D) is finite becausedom(D) and Zb are finite. We write |α| for the element of Σ(D) obtained fromthe event α by dropping the second argument and replacing ⌊h⌋i and ⌈h⌉i by •.
For example, we get |call(tw, 0, ⌊tw⌋0 )| = call(tw, •).
Definition 3 (Finite Traces to HOTs). Given a finite trace ϖ = α1 · · · αm ∈[[D]]fin with m > 0, the corresponding HOT Gϖ = (Vϖ , λϖ , νϖ ) is defined by:– Vϖ = {1, . . . , m},– λϖ = {j 7→ |αj | | j ∈ Vϖ }, and– νϖ is the smallest relation that satisfies: for any j1 , j2 ∈ Vϖ ,• j1 ≺N j2 if j2 = j1 + 1,
• j1 ≺CR j2 if ∃h, h′ , h′′ , i. αj1 = call(h, i, h′ ) ∧ αj2 = ret(h, i, h′′ ),• j1 ≺CC j2 if ∃h, h′ , h′′ , i, i′ . αj1 = call(h′ , i, h) ∧ αj2 = call(h, i′ , h′′ ),• j1 ≺RC j2 if ∃h, h′ , h′′ , i, i′ . αj1 = ret(h′ , i, h) ∧ αj2 = call(h, i′ , h′′ ).
For example, the HOT Gtw in Section 1 is translated from the finite trace
ϖtw defined above (with the call and return events of main omitted).
For an infinite trace π = α1 · α2 · · · ∈ [[D]]inf , the HOT Gπ = (Vπ , λπ , νπ ) isdefined similarly for Vπ = {j ∈ N | j ≥ 1} and λπ = {j 7→ |αj | | j ∈ Vπ }.

3

Propositional Dynamic Logic over Higher-Order Traces

This section presents HOT-PDL, a propositional dynamic logic (PDL) definedover HOTs (see [16] for a general exposition of PDL). HOT-PDL extends pathexpressions of PDL with →ret and →call for traversing edges of HOTs labeledrespectively with CR and CC/RC. The syntax is defined by:(formulas) ϕ ::= p | ϕ1 ∧ ϕ2 | ¬ϕ | [π] ϕ(path expressions) π ::= → | →call | →ret | {ϕ}? | π1 · π2 | π1 + π2 | π ∗Here, p is a meta-variable ranging over atomic propositions AP. Let ⊤ and ⊥denote tautology and contradiction, respectively. Path expressions π are definedusing a syntax based on regular expressions: we have concatenation π1 · π2 ,alternation π1 + π2 , and Kleene star π ∗ . We write π + for π · π ∗ . Path expressions→, →ret , and →call are for traversing edges labeled with N, CR, and CC or
RC, respectively. A path expression {ϕ}? is for testing if ϕ holds at the current
node. A formula [π] ϕ means that ϕ always holds if one moves along any path
represented by the path expression π. The dual formula ⟨π⟩ ϕ is defined by¬ [π] ¬ϕ and means that there is a path represented by π such that ϕ holds if
one moves along the path. ⟨π⟩ and [π] have the same priority as ¬.

11

7
CR

CR

6

10

8
F

3
2

CR
F

5

12
F

13

9

CR

CR

F

F

4

CR

14

F

1

CR

1 : call(main, 0), 2 : call(tw, •), 3 : ret(tw, •), 4 : call(•, 0), 5 : call(•, 0),
6 : call(inc, 0), 7 : ret(inc, 1), 8 : ret(•, 1), 9 : call(•, 1), 10 : call(inc, 1),
11 : ret(inc, 2), 12 : ret(•, 2), 13 : ret(•, 2), 14 : ret(main, 2)
Fig. 3. The pairs of nodes in Gtw related by CR or ↗F

We now define the semantics of HOT-PDL. For a given HOT G = (V, λ, ν)with Σ = AP, λ(u) represents the atomic proposition satisfied at the nodeu ∈ V . We define the semantics [[ϕ]]G of a formula ϕ as the set of all nodes u ∈ V
where ϕ is satisfied, and the semantics [[π]]G of a path expression π as the set of
all pairs (u1 , u2 ) ∈ V × V such that one can move along π from u1 to u2 .
[[p]]G = {u ∈ V | p = λ(u)}′[[ϕ1 ∧ ϕ2 ]]G = [[ϕ1 ]]G ∩ [[ϕ2 ]]G′[[¬ϕ]]G = V \ [[ϕ]]G′[[[π] ϕ]]G = {u ∈ V | ∀u . ((u, u ) ∈ [[π]]G ⇒ u ∈ [[ϕ]]G )}[[→]]G = ≺N[[→ret ]]G = ≺CR[[→call ]]G = ≺CC ∪ ≺RC[[{ϕ}?]]G = {(u, u) ∈ V × V | u ∈ [[ϕ]]G }[[π1 · π2 ]]G = {(u1 , u3 ) ∈ V × V | ∃u2 ∈ V.∪(u1 , u2 ) ∈ [[π1 ]]G ∧ (u2 , u3 ) ∈ [[π2 ]]G }m[[π1 + π2 ]]G = [[π1 ]]G ∪ [[π2 ]]G[[π ∗ ]]G = m≥0 [[π]]G
Here, for a binary relation R, Rm denotes the m-th power of R. Note that thissemantics can interpret a given HOT-PDL formula over both finite and infinite
HOTs. [[p]]G consists of all nodes labeled by p. [[[π] ϕ]]G contains all nodes fromwhich we always reach to a node in [[ϕ]]G if we take a path represented by π. [[→]]G ,[[→ret ]]G , and [[→call ]]G contain the pairs of nodes linked by an edge labeled by N,
CR, and CC or RC, respectively. We write G |= ϕ if 0G ∈ [[ϕ]]G . For example, let
us consider the HOT Gtw and AP = Σ(Dtw ). Then, [[⟨→⟩ ret(tw, •)]]Gtw consistsof the node labeled by call(tw, •). [[⟨→ret ⟩ ret(•, 2)]]Gtw consists of a node labeledby call(•, 0) and the node labeled by call(•, 1). [[⟨→call ⟩ call(•, 0)]]Gtw consistsof the two nodes respectively labeled by call(tw, •) and ret(tw, •). The example
properties of Dtw discussed in Section 1 can be expressed as follows:∧
Prop.1: [→∗ ] x∈Zb ((call(tw, •) ∧ ⟨→ret · →call ⟩ call(•, x)) ⇒ ⟨→call ⟩ call(•, x))
Prop.2: [→∗ ] ((call(tw, •) ∧ ¬ ⟨→ret · →call ⟩ ⊤) ⇒ ¬ ⟨→call ⟩ ⊤)

CC

11

CC

7
CR

3

5

CR

RC

2

CR

4
H

8

6

13

9

H
CR

10

12
H

CR

14
CR

1

CR

1 : call(main, 0), 2 : call(tw, •), 3 : ret(tw, •), 4 : call(•, 0), 5 : call(•, 0),
6 : call(inc, 0), 7 : ret(inc, 1), 8 : ret(•, 1), 9 : call(•, 1), 10 : call(inc, 1),
11 : ret(inc, 2), 12 : ret(•, 2), 13 : ret(•, 2), 14 : ret(main, 2)
Fig. 4. The pairs of nodes in Gtw related by CR, CC, RC, or ↗H

Here,

∧

x∈Zb ϕ abbreviates [nmin /x] ϕ ∧ · · · ∧ [nmax /x] ϕ.

In Section 4, we show further examples that express interesting propertiesof higher-order programs, including stack based access control properties andthose definable using dependent refinement types. We here prepare notations
Tused there. First, we
the symbols Σcall{∨, ΣTret}, and Σcall to denote the∨ overload ∨Σcall ?, respectively. We write
path expressions { Σcall }?, { Σret }?, and→F for the path expression →ret · →, which is used to move from a call event to
the next event of the caller (by skipping to the next event of the corresponding
return event). We also write ↗F for the path expression Σcall · → · →∗F ·Σcall ,which is used to move from a call event to any call event invoked by the callee.
Figure 3 illustrates the pairs of nodes in Gtw related by ↗F . To capture control
flow of higher-order programs, where function callers and callees may exchange
functions as values, we need to use CC- and RC-labeled edges. For example, an
event raised by the function argument farg of a higher-order function f could
be regarded as an event of the caller g of f , because farg is constructed byg. Similarly, an event raised by the (partially-applied) function fret returned
by a function f could be regarded as an event of f . To formalize the idea, weintroduce variants →H and ↗H of →F and ↗F with higher-order control flow
taken into consideration: →H denotes (→ret · →) + (→call · →) and ↗F denotes
T
T
Σcall
· → · →∗H ·Σcall. Note that the source and the target of ↗H are restricted
to call events of top-level functions. Figure 4 illustrates the pairs of nodes in Gtw
related by ↗H , where nodes labeled with events of the same function (in thesense discussed above) are arranged in the same horizontal line.

4

Applications of HOT-PDL

We show how to encode dependent refinement types and stack-based access
control properties using HOT-PDL.
4.1

Dependent Refinement Types

HOT-PDL can specify pre- and post-conditions of higher-order functions, byencoding dependent refinement types τ for partial [29, 33, 40] and total [23, 27, 34,
36, 39] correctness verification, defined as: τ ::= {ν | ψ} | (x : τ1 ) → τ2Q . Here, Q
is either ∀ or ∃. An integer refinement type {ν | ψ} is the type of bounded integers
ν that satisfy the refinement formula ψ over bounded integers. A dependentfunction type (x : τ1 ) → τ2∀ is the type of functions that, for any argument x
conforming to the type τ1 , if terminating, return a value conforming to the type
τ2 . By contrast, (x : τ1 ) → τ2∃ is the type of functions that, for any argument
x conforming to τ1 , always terminate and return a value conforming to τ2 . For
example, Prop.3 and Prop.4 of Dtw are expressed by the following types of tw:()∀∀∀
Prop.3: (f : (x : int) → {ν | ν > x} ) → (x : int) → {ν | ν > x}()∀
Prop.4: (f : (x : int) → int∃ ) → (x : int) → int∃
We here write int for {ν | ⊤}. These types can be encoded in HOT-PDL as:()
Prop.3: call(tw, •) ⇒ ([→call ] incr(•)) ∧ [→ret ] (ret(tw, •) ⇒ [→call ] incr(•))
Prop.4: call(tw, •) ⇒ ([→call ] term(•)) ∧ [→ret ] ret(tw, •) ⇒ [→call ] term(•)∧∧
Here, incr(g)∧ = x∈Zb call(g, x) ⇒ [→ret ] y∈Zb (ret(g, y) ⇒ y > x) andterm(g) = x∈Zb (call(g, x) ⇒ ⟨→ret ⟩ ⊤) for g ∈ {•} ∪ {f | f ∈ dom(D)}. We
now define a translation F from types to HOT-PDL formulas as follows:)∧ (F (g, (x : τ1 ) → τ2Q ) =call(g, x) ⇒ Farg (x, τ1 ) ∧ Fret (g, τ2Q )x∈|τ1 ||(x : τ1 ) → τ2Q | = {•}Farg (•, τ ) = [→call ] F (•, τ )Fret (g, τ ∀ ) = [→ret ]∧| {x | ψ} | = Zb{⊤
Farg (n, {x | ψ}) =⊥(if |= [n/x]ψ)(if ̸|= [n/x]ψ)(ret(g, x) ⇒ F (x, τ ))x∈|τ |

Fret (g, τ ∃ ) = (⟨→ret ⟩ ⊤) ∧ Fret (g, τ ∀ )4.2

Stack-Based Access Control Properties

As briefly summarized in Section 1, stack-based access control [13] ensures thata security-critical function (e.g., file access) is invoked only if all the (immediate
and indirect) callers in the current call stack are trusted, or one of the callers

is a privileged function and its callees are all trusted. We here use HOT-PDL
to specify stack-based access control properties for higher-order programs. Let
Critical, Trusted, and Priv be HOT-PDL formulas that tell whether the current node is labeled with a call event of security-critical, trusted, and privileged
functions, respectively. We assume that Critical, Priv, and ¬Trusted do not
overlap each other, and a function in Priv can be directly called only from afunction in Trusted. Then, one may think we can express the specification as:⟨⟩¬ ↗∗F · {¬Trusted}? · (↗F · {¬Priv}?)+ Critical
Here, the path expression ↗F introduced in Section 3 is used to traverse the callstack bottom-up. The above formula says that an invalid call stack never occurs,
where a call stack is called invalid if it contains a call to an untrusted function(represented by the part ↗∗F {¬Trusted}?), followed by a call to a critical function (represented by Critical), with no intervening call to a privileged function(represented by (↗F · {¬Priv}?)+ ).
This definition, however, is not suﬃcient for our higher-order language. Let
us consider the following program Dpa , which involves a partial application:
let untrusted () = λu.critical u
let main () = untrusted () ()Here, untrusted ̸∈ Trusted and critical ∈ Critical. Intuitively, Dpa should
be regarded as unsafe because critical in the body of untrusted is called.
However, Dpa satisfies the specification above (under the assumption that anonymous functions are in Trusted), because the partial application untrusted ()never causes a call to critical but just returns the anonymous (and trusted)function λu.critical u. The following higher-order program Dho is yet anotherunsafe example that satisfies the specification:
let privileged f = f ()let trusted f = if test () then privileged f else ()let untrusted () = trusted (λx.crash (); critical ())
let main () = untrusted ()Here, privileged ∈ Priv, trusted ∈ Trusted, untrusted ̸∈ Trusted, andcritical ∈ Critical. Note that critical in the body of untrusted is called
as follows: the anonymous function λx.crash (); critical () is first passed totrusted and then to privileged (if test () returns true), and is finally calledby privileged, causing a call to critical.
To remedy the limitation, we introduce a new refined variant of stack-based
access control properties for higher-order programs, formalized in HOT-PDL
from the point of view of interactions among callers and callees as follows:⟨⟩¬ ↗∗H · {¬Trusted}? · (↗H · {¬Priv}?)+ Critical
Note that this is obtained from the previous version by just replacing ↗F with
↗H , which takes into account which function constructed each function valueexchanged among functions. The refined version rejects the unsafe Dpa and Dho
as intended: Dpa (resp. Dho ) is rejected because the call event of λu.critical u(resp. λx.crash (); critical ()) is regarded as an event of untrusted.
Fournet et al. [13] have studied variants of stack-based access control properties for a call-by-value higher-order language. We conclude this section by comparing ours with one of theirs called “stack inspection with frame capture”.2
The ideas behind the two are similar but what follows illustrates the diﬀerence:
let untrusted f = crash (); f ()let trusted x = untrusted (λx.if test () then critical () else ())
let main () = trusted ()This program satisfies ours but violates theirs. Note that ours allows a function
originally constructed by a trusted function to invoke a critical function even
if the function is passed around by an untrusted function. By contrast, in theirdefinition, a trusted function value gets “contaminated” (i.e., disabled to invoke
a critical function) once it is passed to or returned by an untrusted function.
In some cases, their conservative policy is useful, but we believe ours would be
more semantically robust (e.g., even works well with the CPS transformation).

5

HOT-PDL Model Checking

In this section, we define HOT-PDL model checking problems for higher-orderfunctional programs over bounded integers and sketch a proof of the decidability.
Definition 4 (HOT-PDL model checking). Given a program D and a HOTPDL formula ϕ with AP = Σ(D), HOT-PDL model checking is the problem ofdeciding whether Gϖ |= ϕ and Gπ |= ϕ for all ϖ ∈ [[D]]fin and π ∈ [[D]]inf .
Theorem 1 (Decidability). HOT-PDL model checking is decidable.
We show this by a reduction to modal µ-calculus (µ-ML) model checkingof higher-order recursion schemes (HORSs), which is known decidable [21, 28].
A HORS is a grammar for generating a (possibly infinite) ranked tree, and
HORSs are essentially simply-typed lambda calculus with general recursion, tree
constructors, and finite data domains such as booleans and bounded integers.
In the reduction, we encode the set of HOTs that are generated from the given
program D as a single tree (generated by a HORS). For example, Figure 5 showssuch a tree that encodes the HOTs of Dtw .3 There, a node labeled with end represents the termination of the program. Note that the branching at the root nodeis due to the input to the function main. The subtree with the root node labeledwith call(main, 0) is obtained from the HOT Gtw by appending a special nodelabeled with end, adding, for each edge with the label γ ∈ {N, CR, CC, RC},2

We do not compare with the other variants in [13] because they are too syntactic tobe preserved by simple program transformations like inlining.
3
There, for simplicity, we illustrate an unranked tree and omit the label of branchingnodes. In the formalization, we express an unranked tree as a binary tree using a
special node label br of the arity 2 representing a binary branching.

a new node labeledwith γ, and expanding the resulting DAG
call(main, 0)call(main, nmax )call(main, nmin )into a tree. Thus, theedge labels of Gtw arecall(tw, ·)turned into node labels of the tree.
It is also worth
end
CR
CC
CC
mentioning here thatN
we are allowed to exret(tw, ·) ret(tw, ·) call(·, 0) call(·, 1)
pand DAGs into trees
because the truth valueof a HOT-PDL forN RC end
mula is not aﬀectedcall(·, 0)
by node-sharing in
the given HOT. This
nice property is lost
if we extend the pathexpressions of HOTFig. 5. A tree encoding the HOTs generated from Dtw
PDL, for example, withintersections. Thus, thedecidability of model checking for extensions of HOT-PDL is an open problem.
We next explain our translation from a HOT-PDL formula into a µ-ML
formula interpreted over trees that encode HOTs. Our translation is based on
an existing one for ordinary PDL [11]. The syntax of µ-ML is defined as follows:
φ ::= X | p | ¬φ | φ ∧ φ | □φ | νX.φ | µX.φ
Here, X represents a propositional variable and p represents an atomic proposition. A formula □φ means that φ holds for any child of the current node. A
formula µX.φ (resp. νX.φ) represents the least (resp. greatest) fixpoint of thefunction λX.φ. Here, we assume X occurs only positively in φ. For example, the
HOT-PDL formulas [→] p, [→ret ] p, and [→call ] p are respectively translated toµ-ML formulas: □(νX.(N ⇒ □p) ∧ (br ⇒ □X)), □(νX.(CR ⇒ □p) ∧ (br ⇒□X)), and □(νX.((CC ∨ RC) ⇒ □p) ∧ (br ⇒ □X)), where the greatest fixpoints are used to skip the branching nodes labeled with br (that may repeat
infinitely).
Finally, we explain how to obtain a HORS for generating a tree that encodes
the set of HOTs generated from the given program D. We here need to simulate
pointer traversals of HOT-PDL by using purely functional features of HORSs because µ-ML does not support pointers. Intuitively, we obtain the desired HORS
from D by embedding an event monitor and an event handler. Whenever themonitor detects a function call or return event during the execution of D, thehandler creates a new node labeled with the event or ignores the event until acertain event is detected by the monitor, depending on the current mode of thehandler. The handler has the following three modes:

mN : The handler always creates and links two new nodes uN and uα labeledrespectively with N and the event α observed. The handler then continues
as follows, depending on the form of the event α:call(g, n): Spawns a new handler with the mode mret . Then, the two handlers of the modes mN and mret continue to create subtrees of uα .
call(g, •): Spawns two new handlers with the modes mret and mcall . The
three handlers of mN , mret , and mcall continue to create subtrees of uα .
ret(g, n): The handler of the mode mN continues to create a subtree of uα .
ret(g, •): Spawns a new handler with the mode mcall . Then, the two handlers of the modes mN and mcall continue to create subtrees of uα .
mret : The handler ignores all events but the return event corresponding to thecall event that caused the spawn of the handler. If not ignored, the handler
creates and links new nodes uCR and uα labeled with CR and the event α.
The handler changes its mode to mN and continues creating a subtree of uα .
mcall : The handler ignores all events but the call event of the function passed toor returned by the call or return event that caused the spawn of the handler.
If not ignored, the handler creates and links new nodes u and uα labeledrespectively with CC or RC and the event α, duplicates itself, and changes
the mode of the original to mN . The handler of the mode mN (resp. mcall )continues to create a subtree of uα (resp. the parent of u).
For simplicity of the construction, we assume that D is in the ContinuationPassing Style (CPS). This does not lose generality because we can enforce thisform by the CPS transformation. Because CPS explicates the order of function
call and return events, it simplifies event monitoring, handling, and tracking of
the current mode of the monitors, which often changes as monitoring proceeds.

6

Related Work

HOT-PDL can specify temporal trace properties of higher-order programs. An
extension for specifying branching properties, however, remains a future work.
There have been proposed logics and formal languages on richer structures
than words. Regular languages of nested words, or equivalently, Visibly Pushdown Languages (VPLs) have been introduced by Alur and Madhusudan [7]. An(ω-)nested word is a (possibly infinite) word with additional well-nested pointers from call events to the corresponding return events. Compared to temporal
logics CaRet [5] and NWTL [4] over (ω-)nested words, HOT-PDL is definedover HOTs that have richer structures. Recall that a HOT is equipped with
two kinds of pointers: one kind with the label CR, which is the same as thepointers of nested words, and the other kind with the label CC or RC, which
is newly introduced to capture higher-order control flow. Bollig et al. proposed
nested traces as a generalization of nested words for modeling traces of concurrent (first-order) recursive programs, and presented temporal logics over nested
traces [8]. Nested traces, however, cannot model traces of higher-order programs.
We expect a combination of our work with theirs enables us to specify temporal
trace properties of concurrent and higher-order recursive programs. Cyriac etal. have recently introduced an extension of PDL defined over traces of order2 collapsible pushdown systems (CPDS) [3]. Interestingly, their traces are also
equipped with two kinds of pointers: one kind of pointers captures the correspondence between ordinary push and pop stack operations, and the other captures
the correspondence between order-2 push and pop operations for second-orderstacks. Our work deals with higher-order programs that correspond to order-nCPDS for arbitrary n.
Finally, we compare HOT-PDL with existing logics defined over words. It
is well known that LTL is less expressive than ω-regular languages [38]. To
remedy the limitation of LTL, Wolper introduced ETL [38] that allows users
to define new temporal operators using right-linear grammars. Henriksen andThiagarajan proposed DLTL [17] that generalizes the until operator of LTL using
regular expressions. Leucker and Sánchez proposed RLTL [25] that combines LTL
and regular expressions. Vardi and Giacomo have introduced Linear Dynamic
Logic (LDL), a variant of PDL interpreted over infinite words [15, 35]. LDLf ,a variant of PDL interpreted over finite words, has also been studied in [15].
ETL, DLTL, RLTL, and LDL are as expressive as ω-regular languages. Notethat HOT-PDL subsumes (ω-)regular languages because LDL and LDLf canbe naturally embedded in HOT-PDL. (ω-)VPLs strictly subsume (ω-)regular
languages. Though CaRet [5] and NWTL [4] are defined over nested words, they
do not capture the full class of VPLs [10]. To remedy the limitation, VLTL [10]combines LTL and VRE [9] in the style of RLTL, where VRE is a generalizationof regular expressions for VPLs. VLDL [37] extends LDL by replacing the pathexpressions with VPLs over finite words. VLTL and VLDL exactly characterize
ω-VPLs. Because VPLs and HOT-PDL are incomparable, it remains future work
to extend HOT-PDL to subsume (ω-)VPLs.

7

Conclusion and Future Work

We have presented HOT-PDL, an extension of PDL defined over HOTs thatmodel execution traces of call-by-value and higher-order programs. HOT-PDL
enables a precise specification of temporal trace properties of higher-order programs and consequently provides a foundation for specification in various application domains including stack-based access control and dependent refinement
types. We have also studied HOT-PDL model checking and presented a reduction
method to modal µ-calculus model checking of higher-order recursion schemes.
To further widen the scope of our approach, it is worth investigating how
to adapt HOTs and HOT-PDL to call-by-name and/or eﬀectful languages. To
this end, it is natural to incorporate more ideas from achievements of gamesemantics [1, 20, 32] and extend HOTs with new kinds of events and pointers for
capturing call-by-name and/or eﬀectful computations.
Acknowledgments We would like to thank anonymous referees for their useful comments. This work was supported by JSPS KAKENHI Grant Numbers
15H05706, 16H05856, 17H01720, and 17H01723.

References
1. Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information
and Computation 163, 409–470 (2000)
2. Abramsky, S., McCusker, G.: Call-by-value games. In: CSL ’98. LNCS, vol. 1414,
pp. 1–17. Springer (1998)
3. Aiswarya, C., Gastin, P., Saivasan, P.: Nested words for order-2 pushdown systems.
arXiv:1609.06290 (2016)
4. Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: Firstorder and temporal logics for nested words. Logical Methods in Computer Science
Volume 4, Issue 4 (2008)
5. Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls andreturns. In: TACAS ’04. pp. 467–481. Springer (2004)
6. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC ’04. pp. 202–211. ACM (2004)
7. Alur, R., Madhusudan, P.: Adding nesting structure to words. Journal of the ACM
56(3), 16:1–16:43 (2009)
8. Bollig, B., Cyriac, A., Gastin, P., Zeitoun, M.: Temporal logics for concurrent
recursive programs: Satisfiability and model checking. Journal of Applied Logic
12(4), 395 – 416 (2014)
9. Bozzelli, L., Sánchez, C.: Visibly rational expressions. In: FSTTCS ’12. LIPIcs,
vol. 18, pp. 211–223. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2012)
10. Bozzelli, L., Sánchez, C.: Visibly linear temporal logic. In: IJCAR ’14. LNCS,
vol. 8562, pp. 418–433. Springer (2014)
11. Carreiro, F., Venema, Y.: PDL inside the µ-calculus: A syntactic and an automatatheoretic characterization. Advances in Modal Logic 10, 74–93 (2014)12. Disney, T., Flanagan, C., McCarthy, J.: Temporal higher-order contracts. In: ICFP
’11. pp. 176–188. ACM (2011)
13. Fournet, C., Gordon, A.D.: Stack inspection: Theory and variants. In: POPL ’02.
pp. 307–318. ACM (2002)
14. Fujima, K., Ito, S., Kobayashi, N.: Practical alternating parity tree automata model
checking of higher-order recursion schemes. In: APLAS ’13. LNCS, vol. 8301, pp.
17–32. Springer (2013)
15. Giacomo, G.D., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on
finite traces. In: IJCAI ’13. pp. 854–860. AAAI Press (2013)
16. Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press (2000)
17. Henriksen, J.G., Thiagarajan, P.: Dynamic linear time temporal logic. Annals ofPure and Applied Logic 96(1), 187 – 207 (1999)
18. Hofmann, M., Chen, W.: Abstract interpretation from Büchi automata. In: CSLLICS ’14. pp. 51:1–51:10. ACM (2014)19. Honda, K., Yoshida, N.: Game theoretic analysis of call-by-value computation. In:
ICALP ’97. LNCS, vol. 1256, pp. 225–236. Springer (1997)
20. Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF: I, II, and III. Information and Computation 163, 285–408 (2000)
21. Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus
model checking of higher-order recursion schemes. In: LICS ’09. pp. 179–188. IEEE
(2009)
22. Kobayashi, N., Tsukada, T., Watanabe, K.: Higher-order program verification via
HFL model checking. In: ESOP ’18. pp. 711–738. Springer (2018)23. Koskinen, E., Terauchi, T.: Local temporal reasoning. In: CSL-LICS ’14. pp. 59:1–
59:10. ACM (2014)
24. Lester, M.M., Neatherway, R.P., Ong, C.H.L., Ramsay, S.J.: Model checking
liveness properties of higher-order functional programs. URL http://mjolnir.
comlab.ox.ac.uk/papers/thors.pdf (2011)
25. Leucker, M., Sánchez, C.: Regular linear temporal logic. In: ICTAC ’07. pp. 291–
305. Springer (2007)
26. Murase, A., Terauchi, T., Kobayashi, N., Sato, R., Unno, H.: Temporal verificationof higher-order functional programs. In: POPL ’16. pp. 57–68. ACM (2016)
27. Nanjo, Y., Unno, H., Koskinen, E., Terauchi, T.: A fixpoint logic and dependenteﬀects for temporal property verification. In: LICS ’18. ACM (2018)
28. Ong, C.H.L.: On model-checking trees generated by higher-order recursion
schemes. In: LICS ’06. pp. 81–90. IEEE (2006)
29. Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI ’08. pp. 159–169.
ACM (2008)
30. Satake, Y., Unno, H.: Propositional dynamic logic for higher-order functional programs. Extended version, available from http://www.cs.tsukuba.ac.jp/~uhiro/(2018)
31. Suzuki, R., Fujima, K., Kobayashi, N., Tsukada, T.: Streett automata model checking of higher-order recursion schemes. In: FSCD ’17. LIPIcs, vol. 84, pp. 32:1–32:18.
Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2017)32. Tzevelekos, N.: Nominal game semantics. Ph.D. thesis, University of Oxford (2008)
33. Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: PPDP
’09. pp. 277–288. ACM (2009)
34. Unno, H., Satake, Y., Terauchi, T.: Relatively complete refinement type systemfor verification of higher-order non-deterministic programs. Proc. ACM Program.
Lang. 2(POPL), 12:1–12:29 (Dec 2017)35. Vardi, M.Y.: The rise and fall of LTL. GandALF (2011)
36. Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton Jones, S.L.: Refinement
types for Haskell. In: ICFP ’14. pp. 269–282. ACM (2014)
37. Weinert, A., Zimmermann, M.: Visibly linear dynamic logic. In: FSTTCS ’16.
LIPIcs, vol. 65, pp. 28:1–28:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik(2016)
38. Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1),72–99 (1983)
39. Xi, H.: Dependent types for program termination verification. In: LICS ’01. pp.
231–242. IEEE (2001)
40. Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL ’99.
pp. 214–227. ACM (1999)