日本ソフトウェア科学会第 38 回大会 (2021 年度) 講演論文集

Data-Driven Reﬁnement Type Optimization
Yu Gu, Hiroshi Unno, and Takeshi Tsukada

This paper presents a data-driven reﬁnement type optimization method for higher-order functional programs
that manipulate algebraic data types. Reﬁnement type optimization is an extension of reﬁnement type inference to multi-objective optimization of criteria such as the strength/weakness of predicates to be inferred,
thereby allowing user control of types inferred, especially for modular veriﬁcation. Following the previous
work by Hashimoto and Unno, we reduce reﬁnement type optimization to constraint optimization. Their
constraint optimization method, however, does not scale to complex constraints over non-numerical domains
because it is based on Farkas’ Lemma that is limited to numerical domains and non-linear constraint solving
that is of high computational complexity. This paper addresses the scalability issue by proposing a novel
data-driven constraint optimization method based on counterexample guided inductive synthesis.

1 Introduction
Reﬁnement types [1, 3, 7, 9, 13, 14, 17] are dependent types equipped with predicates that can express value-dependent behaviors of programs. They
have been applied to veriﬁcation of higher-orderfunctional programs. To automate veriﬁcation, researchers have proposed a variety of reﬁnement
type inference methods based on software model
checking [6, 12, 13, 15, 18] and abstract interpretation techniques [5, 8].
These inference methods try to infer some reﬁnement types that are suﬃcient to conclude that thegiven program satisﬁes a desired property such as
assertion safety. This design is reasonable for theveriﬁcation purpose because reﬁnement type systems (with a decidable underlying theory) do notsatisfy the principal typing property, and such typing (if any) is computationally hard to infer. Therefore, types inferred by these methods are often too∗ データ駆動リファインメント型最適化.

This is an unrefereed paper. Copyrights belong to
the Author(s).
Yu Gu, Hiroshi Unno, 筑波大学大学院情報理工学位プ
ログラム, Dept. of Computer Science, University ofTsukuba.
Takeshi Tsukada, 千葉大学大学院理学研究院, Dept. ofMathematics and Informatics, Chiba University.

speciﬁc to the given assertions and of limited applicability, in particular to modular veriﬁcation of(a) higher-order functions that take functions asarguments and similarly (b) open programs that
depend on other modules whose deﬁnitions are notavailable at the time of inference.
To regain user control over types to be inferred,
we follow and extend an approach called reﬁnement
type optimization advocated by [4]. Our framework
allows users to control type inference via (1) reﬁnement type templates with predicate variables,
which act as placeholders for reﬁnement predicatesto be inferred, (2) a subset of predicate substitutions, which along with the templates restricts
the search space, and (3) a preference order on
predicate substitutions, which expresses (possibly
multi-objective) optimization criteria such as thestrength/weakness of predicates.
We reduce the problem of ﬁnding a maximallypreferred (i.e., Pareto optimal) reﬁnement typewith respect to the user-speciﬁed order into a
constraint optimization problem we call Optimizing predicate Constraint Satisfaction Problem(Opt-pCSP) where the set of constraints belong to
the class of pCSP [10, 16] that extends the wellknown class of Constraint Horn Clauses (CHCs) [2]with head-disjunctions.
This paper presents a novel data-driven con-

straint optimization method for Opt-pCSP basedon CounterExample Guided Inductive Synthesis(CEGIS) [11] and synthesis based on stratiﬁed families of templates [16]. Our method iteratively reﬁnes the current solution of the given pCSP C until a Pareto optimal one is found. To this end,
we solve a series C0 , C1 , C2 , . . . where C0 = C andeach Ci+1 (i ≥ 0) is obtained from C by adding
a constraint that speciﬁes that any solution of
Ci+1 strictly improves the solution found for Ci ,with respect to the preference order. To express
Ci+1 (i ≥ 0), we extend and use pCSP with nonemptiness constraints.
Our data-driven method remedies the scalability issue of the previous constraint optimization
method based on Farkas’ Lemma and non-linear
constraint solving [4]: it does not scale to complex constraints over non-numerical domains because Farkas’ Lemma is limited to numerical domains and non-linear constraint solving is of highcomputational complexity.
The rest of the paper is organized as follows. Section 2 brieﬂy reviews an existing reﬁnement typesystem and Section 3 formalizes reﬁnement type optimization. Section 4 formalizes Opt-pCSP and discusses reduction from reﬁnement type optimization
to Opt-pCSP. In Section 5, we present our datadriven method for solving Opt-pCSP. We conclude
the paper in Section 6.

2 Reﬁnement Type System
This section brieﬂy reviews an existing reﬁnement type system [13]. The syntax of reﬁnement
types and formulas of the ﬁrst-order quantiﬁer-freetheory of algebraic data types is deﬁned as follows:
σ ::= {x : δ | ψ}
(reﬁnement type
| x:σ→σtemplates)Π ::= ∅
(type environment| Π, x : σ
templates)t ::= x(terms)| K(t1 , . . . , tar(K) )| K#i
a ::= P (et) | t1 = t2 | IsK (t) (atoms)
ψ ::= a | > | ⊥(formulas)| ¬ψ | ψ1 ∧ ψ2
| ψ1 ∨ ψ 2 | ψ1 ⇒ ψ2
Here, x (resp. P ) is a meta-variable ranging overterm (resp. predicate) variables. We use ϕ asa meta-variable ranging over pure formulas which
are formulas without predicate variables. We write
ftv (ϕ) (resp. fpv (ϕ)) for the set of free term (resp.
predicate) variables in ϕ. We use p as a metavariable ranging over predicates that are deﬁnable
as λe
x.ϕ where ftv (ϕ) ⊆ {ex}. We use τ (resp. Γ)
as a meta-variable ranging over reﬁnement types(resp. reﬁnement type environments) which are reﬁnement type templates (resp. reﬁnement type environment templates) without predicate variables.
We write ty(t) for the type of the term t. δ isa meta-variable ranging over (monomorphic) algebraic data types (ADTs). K represents a constructor with ty(K ) = δ1 × · · · × δar(K) → δ forsome ADTs δ, δ1 , . . . , δar(K) , where ar(K) represents the arity of K. K#i represents the i-th selector of the constructor K and ty(K#i(et )) = δi if
ty(K ) = δ1 × · · · × δar(K) → δ and ty(ti ) = δi foreach i. K#i(t) is deﬁned as ti if t is equivalent toK(et) for some et and undeﬁned otherwise. IsK (t)represents the tester for the constructor K: IsK (t)is deﬁned as > if t is equivalent to K(et) for some etand ⊥ otherwise.
We here omit the syntax of program expressions e and the inference rules for typing judgmentsΓ ` e : τ and subtyping judgments Γ ` τ1 <: τ2(see [13] for the deﬁnitions). Intuitively, ` τ1 <: τ2means that any program expression e that has thetype τ1 also has the type τ2 . In other words, τ1 islogically stronger than τ2 and τ1 can express more
precise program behaviors. The following deﬁnitions elaborate on the logical strength of reﬁnement
types:
Deﬁnition 1 (Maximum Speciﬁcation). The
maximum speciﬁcation of a closed program expression e is the strongest reﬁnement type τ :` e : τ ∧ (∀τ ′ . ` e : τ ′ ⇒ ` τ <: τ ′ )Deﬁnition 2 (Maximal Speciﬁcation). A maximum speciﬁcation of a closed program expression
e is a maximally-strong reﬁnement type τ :` e : τ ∧ (∀τ ′ . ` e : τ ′ ∧ τ ′ 6= τ ⇒ 6` τ ′ <: τ )The maximum speciﬁcation (if any) is the mostaccurate representation of the program’s behaviors.
However, it is usually not expressible as a reﬁnement type equipped with predicates of a decidable
underlying theory. This paper thus moves focus
to maximal speciﬁcations. Note that they also do
not exist unless we use appropriate reﬁnement type
templates. The next section introduces reﬁnement

type optimization that allows users to control reﬁnement type inference to obtain (but not limitedto) a maximal speciﬁcation.

3 Reﬁnement Type Optimization
This section formalizes reﬁnement type inference
and generalizes it to reﬁnement type optimization [4].
We ﬁrst deﬁne some auxiliary notions. A predicate type environment ∆ is a map from predicatesvariables to their types. We write dom(∆) for thedomain of ∆. We write σ∆ (resp. Π∆ ) if fpv (σ∆ ) ⊆dom(∆) (resp. ∀(x : σ) ∈ Π∆ . fpv (σ) ⊆ dom(∆)).
A predicate substitution θ is a map from predicate
variables to (deﬁnable) predicates. We write Θ∆ forthe set of predicate substitutions conforming to ∆.
We omit ∆ and write Θ if it is clear from the context. We write θΓ (resp. θσ) for the application ofθ to Γ (resp. σ). We write θ↾∆ to denote the restriction of the domain of θ to dom(∆). We write θ ≡ θ′
if θ is logically equivalent to θ′ : dom(θ) = dom(θ′ )and ∀P ∈ dom(θ). |= θ(P ) ⇔ θ′ (P ).
Deﬁnition 3 (Reﬁnement Type Inference).
Let e be a program expression. Let Π∆ and σ∆ betemplates of a reﬁnement type environment and areﬁnement type, respectively. A reﬁnement type inference problem (e, Π∆ , σ∆ ) is the problem of ﬁnding a predicate substitution θ ∈ Θ∆ such thatθΠ∆ ` e : θσ∆ .
Deﬁnition 4 (Reﬁnement Type Optimization). Let e be a program expression. Let Π∆ andσ∆ be templates of a reﬁnement type environment
and a reﬁnement type, respectively. Let S∆ and∆ be a subset of Θ∆ and a partial order on predicate substitutions in Θ∆ , respectively. A reﬁnement
type optimization problem (e, Π∆ , σ∆ , S∆ , ∆ ) is
the problem of ﬁnding a predicate substitution θsuch that:• θ ∈ S∆ ,• θΠ∆ ` e : θσ∆ , and• ∀θ′ ∈ S∆ .θ′ Π∆ ` e : θ′ σ∆ ∧ θ′ 6≡ θ ⇒ θ′ 6∆ θ.
Here, θ′ 6∆ θ means that either θ ≺∆ θ′ holdsor θ and θ′ are incomparable in ≺∆ . Note that
θ1 ≺∆ θ2 intuitively means that θ1 is more preferred than θ2 and the goal of reﬁnement type optimization is to ﬁnd (if any) a maximally preferredθ (i.e., a minimal θ with respect to ∆ ).

4 Reduction from Reﬁnement Type
Optimization to Opt-pCSP
This section formalizes Optimizing predicate
Constraint Satisfaction Problem (Opt-pCSP) andpresents a reduction from reﬁnement type optimization to Opt-pCSP.
First of all, we follow [10, 16] and deﬁne a predicate Constraint Satisfaction Problem (pCSP) C to
be a ﬁnite set of clauses! of themform
!
l
_
_
ϕ∨
Pi (xei ) ∨¬Pi (xei )
i=1

i=l+1

where 0 ≤ ℓ ≤ m. We write C∆ if fpv (C) ⊆ dom(∆).
We call a predicate substitution θ a solution for CV
if fpv (C) ⊆ dom(θ) and |= θ(C).
Deﬁnition 5 (pCSP Satisﬁability). The predicate satisﬁability problem of a pCSP C is the problem of ﬁnding a solution for C.
The language pCSP generalizes over existing languages of constraints. A pCSP C that satisﬁes ℓ ≤ 1
for all clauses in C is called Constraint Horn Clauses(CHCs) in the literature.
We now deﬁne Optimizing predicate Constraint
Satisfaction Problem (Opt-pCSP).
Deﬁnition 6 (Opt-pCSP). Let C∆ be a pCSP. Let∆ be a partial order on predicate substitutions inΘ∆ and S∆ be a subset of Θ∆ . An Opt-pCSP(C∆ , ∆ , S∆ ) is the problem of ﬁnding a solution
θ of C∆ such that:• θ ∈ S∆ andV• ∀θ′ ∈ S∆ . |= θ′ (C∆ ) ∧ θ 6≡ θ′ ⇒ θ′ 6∆ θ.
The goal of Opt-pCSP is to ﬁnd a maximally preferred θ (i.e., a minimal θ with respect to ∆ ).
We now present the reduction from reﬁnement
type optimization to Opt-pCSP.†1 A reﬁnement
type inference problem can be reduced to a pCSP
by reusing an existing reﬁnement type inference
method [13]: More speciﬁcally, the procedure Gen
deﬁned in [13] inputs a reﬁnement type inference
problem (e, Π∆ , σ∆ ) and outputs a pCSP C∆′ forsome ∆′ such that dom(∆) ⊆ dom(∆′ ). The
constraint generation algorithm Gen satisﬁes the†1 If the shape of reﬁnement predicates in reﬁnement
type templates is restricted to the form P (et), thereduction results in only CHCs optimization problems instead of Opt-pCSP. In other words, ouradoption of Opt-pCSP here allows us to support
expressive templates of reﬁnement types.

soundness and the completeness as stated by thefollowing lemmas (see [13] for the proofs):
Lemma 1. A solution of the pCSP C∆′ =Gen(e, Π∆ , σ∆ ) is a solution of the reﬁnement type
inference problem (e, Π∆ , σ∆ ).
Lemma 2. A solution of the reﬁnement type inference problem (e, Π∆ , σ∆ ) can be extended to asolution of pCSP C∆′ = Gen(e, Π∆ , σ∆ ).
The following theorem shows the soundness of
our reduction from reﬁnement type optimization to
Opt-pCSP:
Theorem 1 (Soundness of Reduction). Suppose that C∆′ = Gen(e, Π∆ , σ∆ ). A solution of the
Opt-pCSP (C∆′ , ext(∆ , ∆′ ), ext(S∆ , ∆′ )) is a solution of the reﬁnement type optimization problem(e, Π∆ , σ∆ , S∆ , ∆ ), where ext(∆ , ∆′ ) is the extension {(θ, θ′ ) ∈ Θ∆′ × Θ∆′ | θ↾∆ ∆ θ′ ↾∆ } of ∆to ∆′ and ext(S∆ , ∆′ ) is the extension {θ ∈ Θ∆′ |θ↾∆ ∈ S∆ } of S∆ to ∆′ .
Proof. Let ∆′ and S∆′ respectively be ext(∆, ∆′ ) and ext(S∆ , ∆′ ). Let θ be a solution of the
Opt-pCSP (C∆′ , ∆′ , S∆′ ). By Deﬁnition 6, θ is asolution of C∆′ such that θ ∈ S∆′ and ∀θ′ ∈ S∆′ . |=V ′
θ (C∆′ ) ∧ θ 6≡ θ′ ⇒ θ′ 6∆′ θ. By Lemma 1, we
obtain that θ↾∆ is a solution of the reﬁnement type
inference problem (e, Π∆ , σ∆ ). By Deﬁnition 3, wehave θ↾∆ Π∆ ` e : θ↾∆ σ∆ . We next prove:(∀θ′ ∈ S∆ .θ′ Π∆ ` e : θ′ σ∆ ∧θ′ 6≡ θ↾∆ ⇒ θ′ 6∆ θ↾∆ ).
We assume that θ′ Π∆ ` e : θ′ σ∆ ∧ θ′ 6≡ θ↾∆ .
By Lemma 2, there is θ′′ such that dom(θ′′ ) =V ′′dom(∆′ ), |=θ (C∆′ ), and θ′ ≡ θ′′ ↾∆ . Thus′′
θ 6≡ θ holds since θ′ 6≡ θ↾∆ and θ′ ≡ θ′′ ↾∆ .
We then have θ′′ 6∆′ θ. By the deﬁnition of∆′ = ext(∆ , ∆′ ), we get θ′ 6∆ θ↾∆ . Thus θ↾∆
is a solution of the reﬁnement type optimization
problem (e, Π∆ , σ∆ , S∆ , ∆ ).

variable P ∈ fpv (C) to its kind; either • or ∃which respectively represent ordinary and nonempty predicate variables.
Here, non-empty predicates are predicates that are
not equivalent to ⊥.
Deﬁnition 7 (pnCSP Satisﬁability). The predicate satisﬁability problem of a pnCSP (C, K) is the
problem of ﬁnding a solution θ of C such that for
all P ∈ fpv (C), |= ∃ex.θ(P )(ex) if K(P ) = ∃.
Algorithm 1: Optimize
Input: An Opt-pCSP (C∆ , ∆ , S∆ )Output: Unknown means that it isunknown whether a solution
exists, Unsat means that there is
no solution, Sat(θ) means that θ isa possibly non-minimal solution
w.r.t. ∆ , MinSat(θ) means that
θ is a minimal solution w.r.t. ∆ .
1 Function Optimize (C∆ , ∆ , S∆ ) =2K∆ ← {P 7→ • | P ∈ fpv (C∆ )};3match Solve(C∆ , K∆ , S∆ ) with4
| Unsat → return Unsat;
5| Unknown → return Unknown;
6| Sat(θ) →7
while > do
′
′
8
(C∆
′ , K∆′ ) ← Improve⪯∆ (θ);′
9match Solve(C∆ ∪ C∆
′ , K∆ ∪′′K∆′ , ext(S∆ , ∆ ∪ ∆ )) with
10
| Unsat →11
return MinSat(θ)
12| Unknown →13
return Sat(θ)
14| Sat(θ′ ) →15θ ← θ′ ↾∆
16
end
17
end
18
end
19 end5 Data-Driven Approach to Opt-pCSP
This section presents a data-driven constraint optimization method for Opt-pCSP. As discussed in
Section 1, we solve a series of pCSP extended with
non-emptiness constraints. We call the extended
class pnCSP. Formally, a pnCSP (C, K) consists of• a ﬁnite set C of pCSP clauses over predicate
variables and• a kind function K that maps each predicate

We now explain our constraint optimization
method for Opt-pCSP shown in Algorithm 1. Optimize iteratively improves the current solution θof the pCSP C∆ until a minimal one with respectto ∆ is found. The sub-procedure Improve⪯∆ ,which is parameterized by ∆ , inputs the current′′
solution θ and outputs a pnCSP (C∆′ , K∆′ ) that

is used to constrain that any solution strictly improves the current solution θ with respect to ∆ .
The sub-procedure Solve is for solving a pnCSP(C∆ , K∆ , S∆ ). We deﬁne Solve by extending an
existing data-driven constraint solving method [16]with non-emptiness constraints and algebraic datatypes (ADTs). Solve is based on CounterExample
Guided Inductive Synthesis (CEGIS), which iteratively accumulates example instances E of the original constraints (C∆ , K∆ , S∆ ) through the following
two phases for each iteration:• Synthesis Phase: ﬁnd a candidate solution
θ that satisﬁes all the examples in E;• Validation Phase: check whether the candidate θ also satisﬁes the original constraints(C∆ , K∆ , S∆ ), and if so, return θ as a genuine
solution, and otherwise repeat the procedureby adding the found counterexamples to E.
In the synthesis phase, the previous constraint solving method uses a predicate synthesizer based on
stratiﬁed families of templates. The synthesizer
can be extended to support non-emptiness constraints and ADTs by designing appropriate families of templates. Figure 1 presents stratiﬁed families of templates TP• (nd , depth) and TP∃ (depth) respectively for ordinary and non-empty predicate
variables over ADTs. The parameters nd anddepth of TP• (nd , depth) are used to control the maximum number of disjuncts and the maximum depthof selector applications. The parameter depth ofTP∃ (depth) is used to control the maximum depthof constructor applications.

6 Conclusion
We have presented a sound reduction from reﬁnement type optimization to a new expressive class ofconstraint optimization problems called Opt-pCSP,
which is necessary to support expressive templatesof reﬁnement types. Furthermore, we have proposed a novel data-driven constraint optimization
method for Opt-pCSP over algebraic data types,
which remedies the scalability issue of the previous
constraint optimization method based on Farkas’
Lemma and non-linear constraint solving.
References[ 1 ] Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A. D., and Maﬀeis, S.: Reﬁnement Types

Stratiﬁed Template Family for Ordinary Predicate
Variables:TP• (nd , depth) ≜let T = {x1 , . . . , xar(P ) } in
let {ϕ1 , . . . , ϕm } = quals(depth, T ) in
W
Vm
λe
x. nd
i=1
j=1 ((ci,j > 0 ⇒ ϕj ) ∧ (ci,j < 0 ⇒ ¬ϕj ))
sel(
(t) ≜

1 ≤ i ≤ ar(K), δ = ty(t),K#i(t)ty(K ) = δ1 → · · · → δar(K) → δ)

quals(0, T ) ≜{t)( 1 = t2 | t1 , t2 ∈ T , t1 6= t2 } ∪t ∈ T , ty(t) = δ,IsK (t)ty(K ) = δ1 → · · · → δar(K) → δ
quals(depth, T ) ≜//depth ≥ 1
Squals(depth − 1, T ∪ t∈T sel (t))
Stratiﬁed Template Family for Non-Empty Predicate Variables:TP∃ (depth) ≜let {p1 , . . . , pm } = genp P (depth) in
W
λe
x. m
x)
i=1 bi ∧ pi (econs(1,  T ) ≜


t1 ,


t
,
.
.
.
,
t
∈
T
,
1
ar(K)

 

.

.
K
ty(t
)
=
δ
for
each
i,
i
i
.








tar(K) ty(K ) = δ1 → · · · → δar(K) → δcons(depth, T ) ≜//depth ≥ 2
Scons(depth − 1, T ∪ t∈T cons(t))
genp P (depth) ≜{y1 , . . . , yar(P ) } = {x1 , . . . , xar(P ) },








t1 ∈ {y1 } ∪ cons(depth, ∅),







Var(P )
λe
t2 ∈ {y2 } ∪ cons(depth, {y1 }), 
x. i=1.
..
yi = t i










t
∈
{y
}
∪


ar(P )
ar(P )

cons(depth, {y , . . . , y}) 1Fig. 1ar(P )−1

Stratiﬁed Families of Templates

for Secure Implementations, ACM Transactions
on Programming Languages and Systems, Vol. 33,
No. 2(2011), pp. 8:1–8:45.
[ 2 ] Bjørner, N., Gurﬁnkel, A., McMillan, K. L., andRybalchenko, A.: Horn Clause Solvers for Program
Veriﬁcation, Fields of Logic and Computation II:
Essays Dedicated to Yuri Gurevich on the Occasionof His 75th Birthday, LNCS, Vol. 9300, Springer,
2015, pp. 24–51.
[ 3 ] Flanagan, C.: Hybrid type checking, POPL ’06,
ACM, 2006, pp. 245–256.

[ 4 ] Hashimoto, K. and Unno, H.: Reﬁnement Type
Inference via Horn Constraint Optimization, SAS’15, LNCS, Vol. 9291, Springer, 2015, pp. 199–216.
[ 5 ] Jhala, R., Majumdar, R., and Rybalchenko, A.:Reﬁnement Type Inference via Abstract Interpretation, arXiv:1004.2884v1, 2010.
[ 6 ] Kobayashi, N., Sato, R., and Unno, H.: Predicate abstraction and CEGAR for higher-ordermodel checking, PLDI ’11, ACM, 2011, pp. 222–
233.
[ 7 ] Nanjo, Y., Unno, H., Koskinen, E., and Terauchi, T.: A Fixpoint Logic and Dependent Effects for Temporal Property Veriﬁcation, LICS ’18,
ACM, July 2018, pp. 759–768.
[ 8 ] Pavlinovic, Z., Su, Y., and Wies, T.: Data
Flow Reﬁnement Type Inference, Proceedings of
the ACM on Programming Languages, Vol. 5,
No. POPL(2021).
[ 9 ] Rondon, P., Kawaguchi, M., and Jhala, R.: Liquid Types, PLDI ’08, ACM, 2008, pp. 159–169.
[10] Satake, Y., Unno, H., and Yanagi, H.: Probabilistic Inference for Predicate Constraint Satisfaction, AAAI ’20, Vol. 34, No. 02(2020), pp. 1644–
1651.
[11] Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., and Saraswat, V.: Combinatorial Sketching for Finite Programs, ASPLOS XII, ACM, 2006,
pp. 404–415.
[12] Terauchi, T.: Dependent types from counterexamples, POPL ’10, ACM, 2010, pp. 119–130.
[13] Unno, H. and Kobayashi, N.: Dependent Type
Inference with Interpolants, PPDP ’09, ACM, 2009,
pp. 277–288.
[14] Unno, H., Satake, Y., and Terauchi, T.: Relatively Complete Reﬁnement Type System for Veriﬁcation of Higher-order Non-deterministic Programs,
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL(2017), pp. 12:1–12:29.
[15] Unno, H., Terauchi, T., and Kobayashi, N.:
Automating Relatively Complete Veriﬁcation ofHigher-order Functional Programs, POPL ’13,
ACM, 2013, pp. 75–86.
[16] Unno, H., Terauchi, T., and Koskinen, E.:
Constraint-based Relational Veriﬁcation, CAV ’21,
Springer, 2021.
[17] Xi, H. and Pfenning, F.: Dependent types inpractical programming, POPL ’99, ACM, 1999,
pp. 214–227.
[18] Zhu, H., Nori, A. V., and Jagannathan, S.:
Learning Reﬁnement Types, ICFP ’15, ACM, 2015,
pp. 400–411.