4 min read
On this page

Type Theory for Verification

Overview

Type systems enforce correctness properties at compile time. Advanced type systems go far beyond preventing "int vs string" errors -- they can encode complex invariants, resource management protocols, and communication patterns directly in types. The compiler becomes a verification tool.

Dependent Types

A dependent type is a type that depends on a value. This allows types to express precise specifications.

-- Vector: a list whose length is tracked in the type
Vec : Type → Nat → Type
Vec A 0       = Nil
Vec A (n + 1) = Cons A (Vec A n)

-- head is total: can only be called on non-empty vectors
head : Vec A (n + 1) → A

-- append tracks lengths precisely
append : Vec A m → Vec A n → Vec A (m + n)

-- Matrix multiplication: dimensions must be compatible
matmul : Matrix m n → Matrix n p → Matrix m p

Key insight: dependent types shift runtime checks to compile time. If it type-checks, certain classes of errors are impossible.

Dependent types in practice:

  • Full spectrum: Coq, Agda, Lean, Idris 2 (types and programs in one language)
  • Limited forms: Haskell (GADTs, type families, singletons), Scala 3 (match types)

Sigma Types and Pi Types

The two fundamental dependent type constructors:

Π(x : A). B(x)    -- dependent function: for all x in A, produce a B(x)
                   -- generalizes A → B when B doesn't depend on x

Σ(x : A). B(x)    -- dependent pair: an x in A together with a proof/value of B(x)
                   -- generalizes A × B when B doesn't depend on x

Example: a function returning a sorted list with a proof of sortedness:

sort : List Nat → Σ(l : List Nat). Sorted l

Refinement Types

Refinement types augment base types with logical predicates, without requiring full dependent type programming. The predicates are checked by SMT solvers.

{v : Int | v > 0}          -- positive integers
{v : List a | len v > 0}   -- non-empty lists
{v : Int | v mod 2 == 0}   -- even integers

Liquid Haskell

Adds refinement types to Haskell via special comments. Uses Z3 for verification.

{-@ type Pos = {v:Int | v > 0} @-}
{-@ type NonEmpty a = {v:[a] | len v > 0} @-}

{-@ divide :: Int -> Pos -> Int @-}
divide :: Int -> Int -> Int
divide x y = x `div` y  -- y > 0 guaranteed by type

{-@ safeHead :: NonEmpty a -> a @-}
safeHead :: [a] -> a
safeHead (x:_) = x
-- No need for empty list case: type makes it unreachable

-- Measures: lift Haskell functions into the refinement logic
{-@ measure elems @-}
elems :: Ord a => [a] -> Set a
elems []     = empty
elems (x:xs) = singleton x `union` elems xs

{-@ sort :: Ord a => xs:[a] -> {v:[a] | elems v == elems xs} @-}

Liquid types use liquid inference: infer refinements from a fixed set of predicates using abstract interpretation over predicate abstraction. Many annotations can be omitted.

F* (F-star)

A full-spectrum verification language combining dependent types, refinement types, and effect tracking. Developed at Microsoft Research.

val factorial : n:nat -> Tot (r:nat{r >= 1})
let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1)

(* Effect system tracks side effects *)
val read_file : filename:string -> ML string        (* may have side effects *)
val pure_add  : x:int -> y:int -> Tot (z:int{z = x + y})  (* pure, total *)

(* Low*: a subset of F* that compiles to C *)
val memcpy: dst:buffer UInt8.t -> src:buffer UInt8.t ->
            len:UInt32.t{v len <= length dst /\ v len <= length src} ->
            Stack unit (requires fun h -> live h dst /\ live h src)
                       (ensures  fun h0 _ h1 -> modifies (loc_buffer dst) h0 h1)

F* extracts to OCaml, F#, C (via KaRaMeL), and WebAssembly. Notable project: Project Everest -- verified HTTPS stack (TLS 1.3, cryptographic primitives).

Linear Types and Ownership

Linear types ensure resources are used exactly once, preventing leaks and use-after-free.

Rust's Ownership System

Rust implements an affine type system (values used at most once) with borrowing:

PROCEDURE CONSUME(s: owned String)   // s is moved here, caller can't use it

PROCEDURE BORROW(s: shared ref String)   // immutable borrow, original still usable

PROCEDURE MUTATE(s: exclusive ref String)   // exclusive mutable borrow

// Compile-time enforced rules:
// 1. Each value has exactly one owner
// 2. Multiple immutable borrows OR one mutable borrow (not both)
// 3. References cannot outlive the value they borrow (lifetimes)

What Rust's type system prevents (without runtime overhead):

  • Use-after-free
  • Double-free
  • Data races (in safe Rust)
  • Null pointer dereference (Option instead of null)
  • Iterator invalidation

Lifetimes are a form of region-based type system:

PROCEDURE LONGEST(x: ref[a] string, y: ref[a] string) → ref[a] string
    IF LENGTH(x) > LENGTH(y) THEN RETURN x ELSE RETURN y
// Return value lives as long as the shorter-lived input

Session Types

Session types specify communication protocols as types. They ensure that interacting processes follow a prescribed message exchange pattern.

// A protocol for an ATM:
type ATMProtocol =
    Recv Authenticate .           // receive credentials
    Branch {                      // client chooses:
      CheckBalance:
        Send Balance . End,       // send balance, done
      Withdraw:
        Recv Amount .             // receive amount
        Branch {                  // server decides:
          Approve: Send Cash . End,
          Deny: Send Reason . End
        }
    }

Properties guaranteed by session types:

  • Communication safety: messages have expected types
  • Protocol fidelity: messages follow the prescribed order
  • Deadlock freedom (in some systems): no circular waiting

Duality: if one end has type Send Int . Recv Bool . End, the other end must have Recv Int . Send Bool . End. The type checker ensures both ends are dual.

Implementations: Haskell (session-types library), Rust (session_types crate), Scala, OCaml, and research languages like SILL and Links.

Effect Systems

Effect systems track what side effects a computation may perform, in addition to what value it returns.

-- A function type with effects:
f : A → {Read, Write, Throw} B
-- f takes A, may Read, Write, or Throw, and produces B

-- Pure function:
g : A → {} B    -- or equivalently: A → Pure B

Common tracked effects:

  • IO (console, file, network)
  • State (mutable variables)
  • Exceptions
  • Nondeterminism
  • Divergence (non-termination)

Algebraic effects (Eff, Koka, OCaml 5) provide user-definable effects with handlers:

effect ask<a> {
  fun ask() : a
}

fun greet() : ask<string> string {
  val name = ask()
  "Hello, " ++ name
}

fun main() {
  with fun ask() { "World" }
  println(greet())  // "Hello, World"
}

F* uses an effect system to distinguish Tot (pure, terminating), Ghost (pure, for specs), ML (may diverge, have side effects), and Stack/Heap (memory management effects).

Gradual Verification

Gradual verification bridges the gap between unverified and fully verified code by allowing partial specifications that are checked statically where possible and dynamically (via runtime checks) where specifications are missing.

// Gradually verified function
fn search(arr: Vec<i32>, target: i32) -> Option<usize>
  requires sorted(arr)     // checked statically if caller provides proof
                           // checked dynamically (runtime assert) otherwise
{
  // ...
}

Key ideas:

  • Programmers add specifications incrementally
  • Unspecified portions get runtime checks (like contracts)
  • As specifications grow, more is verified statically, fewer runtime checks remain
  • Inspired by gradual typing (TypeScript, mypy)

Research tools: Gradual C0, Gradual Verification for Rust.

Comparison

| Approach | Power | Automation | Annotation Burden | Languages | |----------|-------|------------|-------------------|-----------| | Dependent types | Very high | Low | High | Coq, Agda, Lean, Idris | | Refinement types | High | High (SMT) | Moderate | Liquid Haskell, F* | | Linear/affine types | Moderate | High | Low-moderate | Rust, Linear Haskell | | Session types | Moderate | High | Moderate | Research + libraries | | Effect systems | Moderate | High | Low | Koka, F*, Eff | | Gradual verification | Variable | Mixed | Low (incremental) | Research |

Key Takeaways

  • Dependent types are the most expressive: types can encode arbitrary logical properties
  • Refinement types offer a practical middle ground with SMT-automated checking
  • Rust demonstrates that linear types can prevent memory and concurrency bugs at scale
  • Session types bring protocol verification to the type level
  • Effect systems make side effects explicit and controllable
  • Gradual verification enables incremental adoption without all-or-nothing commitment