Relatively Complete
Refinement Type System for
Verification of Higher-Order
Non-deterministic Programs
Hiroshi Unno (University of Tsukuba)
Yuki Satake (University of Tsukuba)
Tachio Terauchi (Waseda University)
POPL'18, Los Angeles, United States1

Background• Recent advances in (semi-)automated methods forverifying higher-order functional programs• safety [Rondon+ ’08; U. & Kobayashi ’08,’09; Terauchi ’10;

Ong & Ramsay ’11; Jhala+ ’11; Kobayashi+ ’11; U.+ ’13; …]• termination [Sereni & Jones ’05; Giesl+ ’11; Kuwahara+ ’14; Vazou+ ’14]

• non-termination [Kuwahara+ ’15; Hashimoto & U. ’15]
• temporal properties [Koskinen & Terauchi ’14; Murase+ ’16]

• Different techniques are used to verify
the different classes of properties, and are
hard to combine in a unified framework• dependent refinement types,• predicate abstraction for higher-order model checking,• program transformation for (binary) reachability analysis,…
POPL'18, Los Angeles, United States2

Our Contributions• Novel dependent refinement type system that can:• uniformly express and verify universal and existential
branching properties of call-by-value, higher-order,and non-deterministic programs:• (cond.) safety, non-safety, termination, and non-termination• seamlessly combine universal and existential reasoning• e.g., Prove non-safety via termination• e.g., Prove non-termination via safety• e.g., Prove termination and non-termination simultaneously• Meta-theoretic properties of the type system:• Closure of types under complement• Soundness• Relative completeness

POPL'18, Los Angeles, United States3

Our Contributions• Novel dependent refinement type system that can:• uniformly express and verify universal and existential
branching properties of call-by-value, higher-order,and non-deterministic programs:• (cond.) safety, non-safety, termination, and non-termination• seamlessly combine universal and existential reasoning• e.g., Prove non-safety via termination• e.g., Prove non-termination via safety• e.g., Prove termination and non-termination simultaneously• Meta-theoretic properties of the type system:• Closure of types under complement• Soundness• Relative completeness

POPL'18, Los Angeles, United States4

Dependent Refinement Types 𝝉𝝉• 𝒙𝒙 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 | 𝒙𝒙 ≥ 𝟎𝟎

Non-negative integers

predicates onprogram values• 𝒙𝒙 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 → {𝒓𝒓 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 | 𝒓𝒓 ≥ 𝒙𝒙}

Functions that take an integer 𝒙𝒙 and(if terminated) return 𝒓𝒓 not less than 𝒙𝒙

 A type system ensures that a type-checked
expression behaves according to the type
 Only universal branching properties
can be expressed
POPL'18, Los Angeles, United States
5Overview: Our Type System• Extends dependent refinement types with:• Qualified types 𝝉𝝉𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐
to express universal/existential branching behaviors
and partial/total correctness• Qualified bindings 𝒙𝒙∶𝑸𝑸 𝝉𝝉
to cope with non-determinism from program inputs• Gödel encoding of function-type values& guarded intersection types
to achieve relative completeness
POPL'18, Los Angeles, United States

6Overview: Our Type System• Extends dependent refinement types with:• Qualified types 𝝉𝝉𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐
to express universal/existential branching behaviors
and partial/total correctness• Qualified bindings 𝒙𝒙∶𝑸𝑸 𝝉𝝉
to cope with non-determinism from program inputs• Gödel encoding of function-type values& guarded intersection typesto achieve relative completeness
POPL'18, Los Angeles, United States

7

𝑸𝑸𝑸𝑸
𝟏𝟏
Qualified Types 𝝉𝝉 𝟐𝟐• 𝑸𝑸𝟏𝟏 ∈ ∀, ∃ (universal/existential non-det.)
specifies whether the expression being typed
behaves according to the type:• for any non-det. evaluation (𝑸𝑸𝟏𝟏 = ∀), or• for some non-det. evaluation (𝑸𝑸𝟏𝟏 = ∃)• 𝑸𝑸𝟐𝟐 ∈ ∀, ∃ (partial/total correctness)
specifies whether:• 𝝉𝝉 holds for all value obtained (𝑸𝑸𝟐𝟐 = ∀), or• there exists a final value for which 𝝉𝝉 holds (𝑸𝑸𝟐𝟐 = ∃)POPL'18, Los Angeles, United States8𝑸𝑸𝑸𝑸
𝟏𝟏Qualified Types 𝝉𝝉 𝟐𝟐• 𝑸𝑸𝟏𝟏 ∈ ∀, ∃ (universal/existential non-det.)
specifies whether the expression being typed
behaves according to the type:• for any non-det. evaluation (𝑸𝑸𝟏𝟏 = ∀), or• for some non-det. evaluation (𝑸𝑸𝟏𝟏 = ∃)• 𝑸𝑸𝟐𝟐 ∈ ∀, ∃ (partial/total correctness)
specifies whether:• the evaluation diverges or 𝝉𝝉 is satisfied (𝑸𝑸𝟐𝟐 = ∀), or• the evaluation terminates and 𝝉𝝉 is satisfied (𝑸𝑸𝟐𝟐 = ∃)POPL'18, Los Angeles, United States

9𝑸𝑸𝑸𝑸
𝟏𝟏Examples: Qualified Types 𝝉𝝉 𝟐𝟐• ⊢ 𝒆𝒆 ∶ 𝒖𝒖 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝒖𝒖 > 𝟎𝟎 ∀∀for any non-deterministic evaluation of 𝒆𝒆,
if any integer 𝒖𝒖 is obtained, then 𝒖𝒖 is positive• ⊢ 𝒆𝒆 ∶ 𝒖𝒖 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝒖𝒖 > 𝟎𝟎 ∃∃for some non-deterministic evaluation of 𝒆𝒆,some integer 𝒖𝒖 is obtained, and 𝒖𝒖 is positive
POPL'18, Los Angeles, United States10Typing Integer Constants

Rule:

Integer
constant
𝚫𝚫 ⊢ 𝒏𝒏 ∶ 𝒙𝒙 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝒙𝒙 = 𝒏𝒏 ∀∃Type
environment

POPL'18, Los Angeles, United States

Universaland Total

11

Converting Qualified Types
Subtyping Rule:
Universaland Partial∀∃

Universaland Total

𝚫𝚫 ⊢ 𝝉𝝉𝟏𝟏 <∶ 𝝉𝝉𝟐𝟐

𝑸𝑸𝟏𝟏 𝑸𝑸′𝟏𝟏 ⊑ 𝑸𝑸𝟐𝟐 𝑸𝑸′𝟐𝟐

𝑸𝑸𝟏𝟏 𝑸𝑸′𝟏𝟏
𝑸𝑸𝟐𝟐 𝑸𝑸′𝟐𝟐
𝚫𝚫 ⊢ 𝝉𝝉𝟏𝟏<∶ 𝝉𝝉𝟐𝟐∀∀∃∃

Existential
POPL'18,Los Angeles,United States
andTotal∃∀

Existentialand Partial
12Typing Let-Bindings
Rule:
𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐
𝚫𝚫 ⊢ 𝒆𝒆𝟏𝟏 ∶ 𝝉𝝉𝟏𝟏
𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐
𝚫𝚫, 𝒙𝒙 ∶ 𝝉𝝉𝟏𝟏 ⊢ 𝒆𝒆𝟐𝟐 ∶ 𝝉𝝉𝟐𝟐𝒙𝒙 ∉ 𝒇𝒇𝒇𝒇𝒇𝒇 𝝉𝝉𝟐𝟐
𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐
𝚫𝚫 ⊢ 𝐥𝐥𝐥𝐥𝐥𝐥 𝒙𝒙 = 𝒆𝒆𝟏𝟏 𝐢𝐢𝐢𝐢 𝒆𝒆𝟐𝟐 ∶ 𝝉𝝉𝟐𝟐

POPL'18, Los Angeles, United States13

Typing Recursive Functions
for Partial Correctness
Rule:
𝑸𝑸∀

𝑸𝑸∀

𝚫𝚫, 𝒙𝒙 ∶ 𝝉𝝉𝟏𝟏 , 𝒇𝒇 ∶ 𝒙𝒙 ∶ 𝝉𝝉𝟏𝟏 → 𝝉𝝉𝟐𝟐 ⊢ 𝒆𝒆 ∶ 𝝉𝝉𝟐𝟐
𝚫𝚫 ⊢ 𝐫𝐫𝐫𝐫𝐫𝐫 𝒇𝒇, 𝒙𝒙, 𝒆𝒆 ∶ 𝒙𝒙 ∶ 𝝉𝝉𝟏𝟏

(recursive) function
𝐥𝐥𝐥𝐥𝐥𝐥 𝐫𝐫𝐫𝐫𝐫𝐫 𝒇𝒇 𝒙𝒙 = 𝒆𝒆
POPL'18, Los Angeles, United States𝑸𝑸∀→ 𝝉𝝉𝟐𝟐14

Typing Recursive Functions for
Total Correctness (cf. [Xi ’01])
Rule:

Well-founded relation witnessing thetermination of 𝒇𝒇, as a recursion guard
𝑸𝑸∃𝝉𝝉𝒓𝒓𝒓𝒓𝒓𝒓 = 𝒙𝒙′ : 𝝉𝝉𝟏𝟏 ′ → 𝝓𝝓 ⊳ 𝝉𝝉𝟐𝟐 ′ 𝑸𝑸∃ =𝜶𝜶 𝒙𝒙 ∶ 𝝉𝝉𝟏𝟏 → 𝝉𝝉𝟐𝟐

𝑸𝑸∃
𝚫𝚫, 𝒙𝒙 ∶ 𝝉𝝉𝟏𝟏 , 𝒇𝒇 ∶ 𝝉𝝉𝒓𝒓𝒓𝒓𝒓𝒓 ⊢ 𝒆𝒆 ∶ 𝝉𝝉𝟐𝟐𝑸𝑸∃𝚫𝚫 ⊢ 𝐫𝐫𝐫𝐫𝐫𝐫 𝒇𝒇, 𝒙𝒙, 𝒆𝒆 ∶ 𝒙𝒙 ∶ 𝝉𝝉𝟏𝟏 → 𝝉𝝉𝟐𝟐

𝚫𝚫 ⊨ 𝑾𝑾𝑾𝑾 𝝀𝝀 𝒙𝒙, 𝒙𝒙′ . 𝝓𝝓

Example:𝒙𝒙𝒙 ∶ 𝒙𝒙𝒙 ∣ 𝒙𝒙𝒙 ≥ 𝟎𝟎→ 𝒙𝒙 > 𝒙𝒙′ ≥ 𝟎𝟎 ⊳ 𝒚𝒚𝒚 ∣ 𝒚𝒚𝒚 ≥ 𝒙𝒙𝒙 ∀∃𝒙𝒙 ∶ 𝒙𝒙 ∣ 𝒙𝒙 ≥ 𝟎𝟎 , 𝒔𝒔𝒔𝒔𝒔𝒔 ∶ 𝝉𝝉𝒓𝒓𝒓𝒓𝒓𝒓 ⊢ 𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝟎𝟎 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝟎𝟎 𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞 … ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∀∃⊨ 𝑾𝑾𝑾𝑾 𝝀𝝀 𝒙𝒙, 𝒙𝒙′ . 𝒙𝒙 > 𝒙𝒙′ ≥ 𝟎𝟎
⊢ 𝐫𝐫𝐫𝐫𝐫𝐫 𝒔𝒔𝒔𝒔𝒔𝒔, 𝒙𝒙, 𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝟎𝟎 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝟎𝟎 𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞 𝒙𝒙 + 𝒔𝒔𝒔𝒔𝒔𝒔 𝒙𝒙 − 𝟏𝟏 ∶ 𝝉𝝉
𝒙𝒙 ∶ 𝒙𝒙 ∣ 𝒙𝒙 ≥ 𝟎𝟎

POPL'18, Los Angeles, United States→ 𝐢𝐢𝐢𝐢𝐢𝐢 ∀∃15

Overview: Our Type System• Extends dependent refinement types with:• Qualified types 𝝉𝝉𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐
to express universal/existential branching behaviors
and partial/total correctness• Qualified bindings 𝒙𝒙∶𝑸𝑸 𝝉𝝉
to cope with non-determinism from program inputs• Gödel encoding of function-type values& guarded intersection types
to achieve relative completeness
POPL'18, Los Angeles, United States

16

𝑸𝑸
Qualified Bindings 𝒙𝒙∶ 𝝉𝝉• Occur in type environments and theargument of dependent function types• 𝑸𝑸 ∈ ∀, ∃ specifies whether a certain factmust hold for:• any input 𝒙𝒙 that satisfies 𝝉𝝉 (𝑸𝑸 = ∀), or• some input 𝒙𝒙 that satisfies 𝝉𝝉 (𝑸𝑸 = ∃)POPL'18, Los Angeles, United States17

Examples: Qualified Bindings 𝒙𝒙∶ 𝝉𝝉• 𝒙𝒙∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒖𝒖 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝒖𝒖 > 𝒙𝒙 ∀∃𝑸𝑸

functions that, for any integer 𝒙𝒙 andfor any run with the argument 𝒙𝒙,
return some integer 𝒖𝒖,
which is greater than 𝒙𝒙• 𝒙𝒙∶∃ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒖𝒖 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝒖𝒖 > 𝒙𝒙 ∀∃functions that, there exists an integer 𝒙𝒙,
for any run with the argument 𝒙𝒙,
return some integer 𝒖𝒖,
which is greater than 𝒙𝒙
POPL'18, Los Angeles, United States18

Skolemizing Existential Bindings
Rule:Type environment
consisting of only∀-bindings

Example:Skolemization Predicate

𝚫𝚫, 𝒙𝒙 :∃ 𝝉𝝉 ⊨ 𝝓𝝓
𝚫𝚫, 𝒙𝒙 :∀ 𝝉𝝉, 𝝓𝝓, 𝚪𝚪 ⊢ 𝒆𝒆 ∶ 𝝈𝝈
𝚫𝚫, 𝒙𝒙 :∃ 𝝉𝝉, 𝚪𝚪 ⊢ 𝒆𝒆 ∶ 𝝈𝝈Type environment consistingof both ∀- and ∃-bindings

𝒙𝒙 :∀ 𝐢𝐢𝐢𝐢𝐢𝐢, 𝒚𝒚 :∃ 𝐢𝐢𝐢𝐢𝐢𝐢 ⊨ 𝒚𝒚 = −𝒙𝒙
𝒙𝒙 :∀ 𝐢𝐢𝐢𝐢𝐢𝐢, 𝒚𝒚 :∀ 𝐢𝐢𝐢𝐢𝐢𝐢, 𝒚𝒚 = −𝒙𝒙 ⊢ 𝒙𝒙 + 𝒚𝒚 ∶ 𝒛𝒛 ∣ 𝒛𝒛 = 𝟎𝟎 ∀∃𝒙𝒙 :∀ 𝐢𝐢𝐢𝐢𝐢𝐢, 𝒚𝒚 :∃ 𝐢𝐢𝐢𝐢𝐢𝐢 ⊢ 𝒙𝒙 + 𝒚𝒚 ∶ 𝒛𝒛 ∣ 𝒛𝒛 = 𝟎𝟎 ∀∃POPL'18, Los Angeles, United States19

Typing Non-deterministic Choice
Rule:
𝚫𝚫, 𝒙𝒙∶𝑸𝑸𝟏𝟏 𝐢𝐢𝐢𝐢𝐢𝐢 ⊢ 𝒆𝒆 ∶ 𝝉𝝉𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐 𝒙𝒙 ∉ 𝒇𝒇𝒇𝒇𝒇𝒇 𝝉𝝉𝚫𝚫 ⊢ 𝐥𝐥𝐥𝐥𝐥𝐥 𝒙𝒙 = ∗ 𝐢𝐢𝐢𝐢 𝒆𝒆 ∶ 𝝉𝝉𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐

Example:𝒙𝒙∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢, 𝒚𝒚∶∃ 𝐢𝐢𝐢𝐢𝐢𝐢 ⊢ 𝒙𝒙 + 𝒚𝒚 ∶ 𝒛𝒛 ∣ 𝒛𝒛 = 𝟎𝟎 ∃∃𝒙𝒙 ∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢 ⊢ 𝐥𝐥𝐥𝐥𝐥𝐥 𝒚𝒚 = ∗ 𝐢𝐢𝐢𝐢 𝒙𝒙 + 𝒚𝒚 ∶ 𝒛𝒛 ∣ 𝒛𝒛 = 𝟎𝟎 ∃∃POPL'18, Los Angeles, United States20

Typing Function Applications(Universal Bindings)
Rule:
𝚫𝚫 ⊢ 𝒗𝒗𝟏𝟏 ∶ 𝒙𝒙 :∀ 𝝉𝝉 → 𝝈𝝈 𝚫𝚫 ⊢ 𝒗𝒗𝟐𝟐 ∶ 𝝉𝝉
𝚫𝚫 ⊢ 𝒗𝒗𝟏𝟏 𝒗𝒗𝟐𝟐 ∶ [𝒗𝒗𝟐𝟐 /𝒙𝒙]𝝈𝝈

POPL'18, Los Angeles, United States21

Typing Function Applications(Existential Bindings)

Observational
equivalence

Rule:

𝚫𝚫 ⊢ 𝒗𝒗𝟏𝟏 ∶ 𝒙𝒙∶∃ 𝝉𝝉 → 𝝈𝝈 𝚫𝚫, 𝒙𝒙∶∀ 𝝉𝝉, 𝚪𝚪 ⊨ 𝒙𝒙 ∼ 𝒗𝒗𝟐𝟐
𝚫𝚫, 𝚪𝚪 ⊢ 𝒗𝒗𝟏𝟏 𝒗𝒗𝟐𝟐 ∶ [𝒗𝒗𝟐𝟐 /𝒙𝒙]𝝈𝝈

Example:𝒇𝒇∶∀ 𝝉𝝉 ⊢ 𝒇𝒇 ∶ 𝝉𝝉 𝒇𝒇∶∀ 𝝉𝝉, 𝒙𝒙∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢, 𝒚𝒚∶∃ 𝐢𝐢𝐢𝐢𝐢𝐢 ⊨ 𝒙𝒙 = 𝒚𝒚𝒇𝒇∶∀ 𝝉𝝉, 𝒚𝒚∶∃ 𝐢𝐢𝐢𝐢𝐢𝐢 ⊢ 𝒇𝒇 𝒚𝒚 ∶ 𝒛𝒛 ⊥ ∃∀𝒇𝒇∶∀ 𝝉𝝉 ⊢ 𝐥𝐥𝐥𝐥𝐥𝐥 𝒚𝒚 = ∗ 𝐢𝐢𝐢𝐢 𝒇𝒇 𝒚𝒚 ∶ 𝒛𝒛 ⊥ ∃∀𝒙𝒙 :∃ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒛𝒛

⊥ ∃∀POPL'18, Los Angeles, United States22

Converting Function Types (1/4)
Subtyping Rule:
𝚫𝚫 ⊢ 𝝉𝝉𝟐𝟐 <∶ 𝝉𝝉𝟏𝟏 𝚫𝚫, 𝒙𝒙 ∶∀ 𝝉𝝉𝟐𝟐 ⊢ 𝝈𝝈𝟏𝟏 <∶ 𝝈𝝈𝟐𝟐
𝚫𝚫 ⊢ 𝒙𝒙∶∀ 𝝉𝝉𝟏𝟏 → 𝝈𝝈𝟏𝟏 <∶ 𝒙𝒙∶∀ 𝝉𝝉𝟐𝟐 → 𝝈𝝈𝟐𝟐

Example:⊢ 𝒙𝒙∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒚𝒚 ∣ 𝒚𝒚 = 𝒙𝒙 ∀∃<∶ 𝒙𝒙∶∀ 𝒙𝒙 ∣ 𝒙𝒙 ≥ 𝟎𝟎 → 𝒚𝒚 ∣ 𝒚𝒚 ≥ 𝟎𝟎 ∀∃POPL'18, Los Angeles, United States23

Converting Function Types (2/4)
Subtyping Rule:
𝚫𝚫 ⊢ 𝝉𝝉𝟏𝟏 <∶ 𝝉𝝉𝟐𝟐 𝚫𝚫, 𝒙𝒙 ∶∀ 𝝉𝝉𝟏𝟏 ⊢ 𝝈𝝈𝟏𝟏 <∶ 𝝈𝝈𝟐𝟐
𝚫𝚫 ⊢ 𝒙𝒙∶∃ 𝝉𝝉𝟏𝟏 → 𝝈𝝈𝟏𝟏 <∶ 𝒙𝒙∶∃ 𝝉𝝉𝟐𝟐 → 𝝈𝝈𝟐𝟐

Example:⊢ 𝒙𝒙∶∃ 𝒙𝒙 ∣ 𝒙𝒙 ≥ 𝟎𝟎 → 𝒚𝒚 ∣ 𝒚𝒚 = 𝒙𝒙 ∀∃<∶ 𝒙𝒙∶∃ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒚𝒚 ∣ 𝒚𝒚 ≥ 𝟎𝟎 ∀∃POPL'18, Los Angeles, United States24

Converting Function Types (3/4)
Subtyping Rule:
𝚫𝚫 ⊢ 𝝉𝝉 <∶ 𝝉𝝉𝟏𝟏 𝚫𝚫 ⊢ 𝝉𝝉 <∶ 𝝉𝝉𝟐𝟐
𝚫𝚫, 𝒙𝒙 ∶∃ 𝝉𝝉 ⊢ 𝝈𝝈𝟏𝟏 <∶ 𝝈𝝈𝟐𝟐
𝚫𝚫 ⊢ 𝒙𝒙∶∀ 𝝉𝝉𝟏𝟏 → 𝝈𝝈𝟏𝟏 <∶ 𝒙𝒙∶∃ 𝝉𝝉𝟐𝟐 → 𝝈𝝈𝟐𝟐

Example:⊢ 𝒙𝒙 ∣ 𝒙𝒙 ≥ 𝟎𝟎 <∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ⊢ 𝒙𝒙 ∣ 𝒙𝒙 ≥ 𝟎𝟎 <∶ 𝐢𝐢𝐢𝐢𝐢𝐢
𝒙𝒙∶∃ 𝒙𝒙 ∣ 𝒙𝒙 ≥ 𝟎𝟎 ⊢ 𝒚𝒚 ∣ 𝒚𝒚 = 𝒙𝒙 ∀∃ <∶ 𝒚𝒚 ∣ 𝒚𝒚 = 𝟎𝟎 ∀∃⊢ 𝒙𝒙∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒚𝒚 ∣ 𝒚𝒚 = 𝒙𝒙 ∀∃ <∶ 𝒙𝒙∶∃ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒚𝒚 ∣ 𝒚𝒚 = 𝟎𝟎 ∀∃POPL'18, Los Angeles, United States25

Converting Function Types (4/4)
Subtyping Rule:𝚫𝚫, 𝒙𝒙∶∀ 𝝉𝝉𝟏𝟏 ∧ 𝝉𝝉𝟐𝟐 , 𝒚𝒚∶∀ 𝝉𝝉𝟏𝟏 ∧ 𝝉𝝉𝟐𝟐 ⊨ 𝒙𝒙 ∼ 𝒚𝒚𝚫𝚫, 𝒙𝒙∶∀ 𝝉𝝉𝟏𝟏 ∧ 𝝉𝝉𝟐𝟐 ⊢ 𝝈𝝈𝟏𝟏 <∶ 𝝈𝝈𝟐𝟐
Observational∀𝚫𝚫, 𝒙𝒙∶ 𝝉𝝉𝟏𝟏 ∖ 𝝉𝝉𝟐𝟐 ⊢ 𝝈𝝈𝟏𝟏 <∶ ⊥equivalence
𝚫𝚫, 𝒙𝒙∶∀ 𝝉𝝉𝟐𝟐 ∖ 𝝉𝝉𝟏𝟏 ⊢ ⊤ <∶ 𝝈𝝈𝟐𝟐
𝚫𝚫 ⊢ 𝒙𝒙∶∃ 𝝉𝝉𝟏𝟏 → 𝝈𝝈𝟏𝟏 <∶ 𝒙𝒙∶∀ 𝝉𝝉𝟐𝟐 → 𝝈𝝈𝟐𝟐

Example:⊢ 𝒙𝒙∶∃ 𝒙𝒙 ∣ 𝒙𝒙 = 𝟎𝟎 → 𝒚𝒚 ∣ 𝒚𝒚 = 𝟎𝟎 ∀∃<∶ 𝒙𝒙∶∀ 𝒙𝒙 ∣ 𝒙𝒙 = 𝟎𝟎 → 𝒚𝒚 ∣ 𝒚𝒚 = 𝒙𝒙 ∀∃POPL'18, Los Angeles, United States

26

Overview: Our Type System• Extends dependent refinement types with:• Qualified types 𝝉𝝉𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐
to express universal/existential branching behaviors
and partial/total correctness• Qualified bindings 𝒙𝒙∶𝑸𝑸 𝝉𝝉
to cope with non-determinism from program inputs• Gödel encoding of function-type values& guarded intersection types
to achieve relative completeness
POPL'18, Los Angeles, United States27

Gödel Encoding ofFunction-Type Values• Enables predicates of the underlying logic 𝑻𝑻(e.g., second-order arithmetic) to depend on
function-type arguments encoded as 𝑻𝑻-objects• 𝒇𝒇∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 ∀∃ → 𝒈𝒈∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝐢𝐢𝐢𝐢𝐢𝐢 ∀∃ → 𝒖𝒖 ∣ 𝒇𝒇 ∼ 𝒈𝒈 ∀∀Functions that, given two terminating
functions 𝒇𝒇 and 𝒈𝒈, always diverge
if 𝒇𝒇 is not observationally equivalent to 𝒈𝒈
POPL'18, Los Angeles, United States

28

Guarded Intersection Types
𝑸𝑸𝒊𝒊 𝑸𝑸′𝒊𝒊⋀𝒊𝒊 𝝓𝝓𝒊𝒊 ⊳ 𝝉𝝉𝒊𝒊

• Collectively express different behaviors offunctions depending on the arguments∀∃ ∧ 𝒙𝒙 < 𝟎𝟎 ⊳ 𝒚𝒚 ⊥ ∀∀ ∧𝒙𝒙>
𝟎𝟎⊳𝐢𝐢𝐢𝐢𝐢𝐢• 𝒙𝒙 :∀ 𝐢𝐢𝐢𝐢𝐢𝐢 →𝒙𝒙 = 𝟎𝟎 ⊳ 𝐢𝐢𝐢𝐢𝐢𝐢 ∃∃ ∧ 𝒙𝒙 = 𝟎𝟎 ⊳ 𝒚𝒚 ⊥ ∃∀Functions that, given the argument 𝒙𝒙 :• always terminate if 𝒙𝒙 > 𝟎𝟎,• always diverge if 𝒙𝒙 < 𝟎𝟎, and otherwise,• non-deterministically terminate or diverge
POPL'18, Los Angeles, United States

29

Our Contributions• Novel dependent refinement type system that can:• uniformly express and verify universal and existential
branching properties of call-by-value, higher-order,and non-deterministic programs:• (cond.) safety, non-safety, termination, and non-termination• seamlessly combine universal and existential reasoning• e.g., Prove non-safety via termination• e.g., Prove non-termination via safety• e.g., Prove termination and non-termination simultaneously• Meta-theoretic properties of the type system:• Closure of types under complement• Soundness• Relative completeness

POPL'18, Los Angeles, United States

30

Complement Types ¬𝝈𝝈• Thanks to having both modes of non-determinism,
the type complement operator ¬ can be defined:¬¬ 𝝉𝝉𝑸𝑸𝟏𝟏 𝑸𝑸𝟐𝟐 ≜ ¬𝝉𝝉 ¬𝑸𝑸𝟏𝟏 ¬𝑸𝑸𝟐𝟐¬ 𝒙𝒙 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝝓𝝓 ≜ 𝒙𝒙 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ ¬𝝓𝝓𝒙𝒙 ∶𝑸𝑸 𝝉𝝉 → 𝝈𝝈 ≜ 𝒙𝒙 :¬𝑸𝑸 𝝉𝝉 → ¬𝝈𝝈¬∀ ≜ ∃¬∃ ≜ ∀POPL'18, Los Angeles, United States31Example: Complement Types ¬𝝈𝝈• 𝝈𝝈 ≜ 𝒙𝒙 ∶∀ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒖𝒖 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝒖𝒖 = 𝒙𝒙 ∀∀functions that, for any integer 𝒙𝒙 andfor any run with the argument 𝒙𝒙,diverge or return an integer 𝒖𝒖 = 𝒙𝒙

• ¬𝝈𝝈 = 𝒙𝒙 ∶∃ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒖𝒖 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 ∣ 𝒖𝒖 ≠ 𝒙𝒙 ∃∃functions that, for some integer 𝒙𝒙 andfor some run with the argument 𝒙𝒙,terminate and return an integer 𝒖𝒖 ≠ 𝒙𝒙
POPL'18, Los Angeles, United States

32

Example: Combined Reasoning(Non-safety via Termination)
Goal: prove that𝐥𝐥𝐥𝐥𝐥𝐥 𝐫𝐫𝐫𝐫𝐫𝐫 𝒇𝒇 𝒙𝒙 𝒚𝒚 =𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒚𝒚 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝟎𝟎
𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞 𝒇𝒇 𝒙𝒙 − 𝟏𝟏 𝒚𝒚𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = 𝒇𝒇 𝟏𝟏𝟏𝟏𝟗𝟗 𝟎𝟎 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝒛𝒛 = ∗ 𝐢𝐢𝐢𝐢 𝒛𝒛 + 𝒓𝒓

violates𝒖𝒖 ∣ 𝒖𝒖 = 𝟎𝟎 ∀∀POPL'18, Los Angeles, United States

33

Example: Combined Reasoning(Non-safety via Termination)
Goal: prove that𝐥𝐥𝐥𝐥𝐥𝐥 𝐫𝐫𝐫𝐫𝐫𝐫 𝒇𝒇 𝒙𝒙 𝒚𝒚 =𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒚𝒚 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝟎𝟎
𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞 𝒇𝒇 𝒙𝒙 − 𝟏𝟏 𝒚𝒚𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = 𝒇𝒇 𝟏𝟏𝟏𝟏𝟗𝟗 𝟎𝟎 𝐢𝐢𝐢𝐢
𝐥𝐥𝐥𝐥𝐥𝐥 𝒛𝒛 = ∗ 𝐢𝐢𝐢𝐢 𝒛𝒛 + 𝒓𝒓

satisfies¬ 𝒖𝒖 ∣ 𝒖𝒖 = 𝟎𝟎 ∀∀POPL'18, Los Angeles, United States34Example: Combined Reasoning(Non-safety via Termination)
Goal: prove that

1. Show that 𝒇𝒇 isconditionally terminating:satisfiesby checking ⊨ 𝟎𝟎 ≤ 𝟏𝟏𝟎𝟎𝟗𝟗
3. Show that, for any integer 𝒓𝒓,we can choose an integer 𝒛𝒛
such that 𝒛𝒛 + 𝒓𝒓 ≠ 𝟎𝟎
Q.E.D.

𝐥𝐥𝐥𝐥𝐥𝐥 𝐫𝐫𝐫𝐫𝐫𝐫 𝒇𝒇 𝒙𝒙 𝒚𝒚 =The well-founded relation
𝝀𝝀 𝒙𝒙, 𝒚𝒚 , 𝒙𝒙′ , 𝒚𝒚𝒚 .
𝐢𝐢𝐢𝐢 𝒙𝒙 = 𝒚𝒚 𝐭𝐭𝐭𝐭𝐭𝐭𝐭𝐭 𝟎𝟎
𝒙𝒙 > 𝒙𝒙′ ∧ 𝒚𝒚 = 𝒚𝒚′ ∧ 𝒙𝒙 ≥ 𝒚𝒚
𝐞𝐞𝐞𝐞𝐞𝐞𝐞𝐞 𝒇𝒇 𝒙𝒙 − 𝟏𝟏 𝒚𝒚
witnesses that 𝒇𝒇 has the type:𝒙𝒙 ∶ 𝐢𝐢𝐢𝐢𝐢𝐢 → 𝒚𝒚 ∶ 𝒚𝒚 ∣ 𝒚𝒚 ≤ 𝒙𝒙 → 𝐢𝐢𝐢𝐢𝐢𝐢 ∀∃𝟗𝟗𝐥𝐥𝐥𝐥𝐥𝐥 𝒓𝒓 = 𝒇𝒇 𝟏𝟏𝟏𝟏 𝟎𝟎 𝐢𝐢𝐢𝐢
2. Show that the actual call𝐥𝐥𝐥𝐥𝐥𝐥 𝒛𝒛 = ∗ 𝐢𝐢𝐢𝐢 𝒛𝒛 + 𝒓𝒓
𝒇𝒇 𝟏𝟏𝟏𝟏𝟗𝟗 𝟎𝟎 always terminates𝒖𝒖 ∣ 𝒖𝒖 ≠ 𝟎𝟎 ∃∃POPL'18, Los Angeles, United States

35

Our Contributions• Novel dependent refinement type system that can:• uniformly express and verify universal and existential
branching properties of call-by-value, higher-order,and non-deterministic programs:• (cond.) safety, non-safety, termination, and non-termination• seamlessly combine universal and existential reasoning• e.g., Prove non-safety via termination• e.g., Prove non-termination via safety• e.g., Prove termination and non-termination simultaneously• Meta-theoretic properties of the type system:• Closure of types under complement• Soundness• Relative completeness

POPL'18, Los Angeles, United States36

Closure of Types under Complement
For any type 𝝈𝝈 refining a simple type 𝑺𝑺,• 𝝈𝝈 ∩ ¬𝝈𝝈 = ∅ and• 𝝈𝝈 ∪ ¬𝝈𝝈 = 𝑺𝑺
where
• 𝝈𝝈 : the set of expressions
that behave according to 𝝈𝝈• 𝑺𝑺 : the set of expressions of the type 𝑺𝑺
POPL'18, Los Angeles, United States37

Soundness𝚪𝚪 ⊢ 𝒆𝒆 ∶ 𝝈𝝈 implies 𝒆𝒆 ∈ 𝚪𝚪 ⊢ 𝝈𝝈

the set of expressions
that behave according to𝝈𝝈 under any valuation
conforming to 𝚪𝚪
POPL'18, Los Angeles, United States

38

Relative Completeness𝑒𝑒 ∈ Γ ⊢ 𝜎𝜎 implies Γ ⊢ 𝑒𝑒 ∶ 𝜎𝜎under the assumption that the underlying logic
is sufficiently expressible• to Gödel encode arbitrary functions definable in
the target programming language• to represent well-founded relations witnessing
the termination of the definable functions

POPL'18, Los Angeles, United States

39

Summary• Novel dependent refinement type system that can:• uniformly express and verify universal and existential
branching properties of call-by-value, higher-order,and non-deterministic programs:• (cond.) safety, non-safety, termination, and non-termination• seamlessly combine universal and existential reasoning• e.g., Prove non-safety via termination• e.g., Prove non-termination via safety• e.g., Prove termination and non-termination simultaneously• Meta-theoretic properties of the type system:• Closure of types under complement• Soundness• Relative completeness

POPL'18, Los Angeles, United States40

Future Work
• Extensions with temporal specifications:• Temporal trace specs. (e.g., LTL)
• Branching temporal specs. (e.g., CTL, modal-𝜇𝜇)• Extensions with language features:• Recursive data structures• Linked data structures• Call-by-name evaluation• Probabilistic choice• Automation of type checking and inference
POPL'18, Los Angeles, United States

41

Towards Automation (Ongoing)• Type Checking• How to leverage off-the-shelf SMT solvers?
Abstraction and counterexample guided refinement
for the encoding of function-type values• Type Inference• How to synthesize inductive invariants, well-foundedrelations, and Skolemization predicates?
Reduction to existentially-quantified
Horn clause and well-foundedness constraints• How to achieve scalable inference?
Combination of universal and existential reasoning
POPL'18, Los Angeles, United States42