TypeScript → OCaml → Separation Logic25 / 25 entail checks passed

TypeHL

Annotate TypeScript with @req / @ens specs

Get Heifer-type separation logic verification that TypeScript cannot express

tsx scripts/convert.ts examples/type_demo.ts

[PASS] plus [ Entail Check ] true

[PASS] deref [ Entail Check ] true

[PASS] inc_inplace [ Entail Check ] true

[PASS] swap [ Entail Check ] true

[PASS] tail [ Entail Check ] true

ALL 5 SPEC(S) VERIFIED

Heap ownershipSeparating conjunctionType mutationAliasing analysisParametric polymorphismADT dispatch

TypeHL for TypeScript is a research prototype demonstrating separation logic applied to mainstream programming languages. It provides a front-end for annotating TypeScript with structural separation-logic specifications, compiling them into OCaml stubs verified by the Heifer backend. This prevents issues like unsound aliasing while maintaining a familiar developer experience.

Live Demo

Edit TypeScript with @req / @ens JSDoc tags, then click Verify to run the full Heifer-type pipeline.

TypeScript Input.ts

Emitted OCaml

Click Verify to see emitted OCaml stubs

Heifer-type Results

Results appear here after verification

Core Evaluation Examples

Key patterns where TypeScript cannot express what Heifer-type verifies

Type Mutation

inc_inplace

TypeScript type-checks snapshots, not state transitions. It either rejects the typed version or loses all type info with any.

TypeScript: Rejects or loses type info

// TS: type error OR unconstrained any
function inc_inplace(x: { val: number }): void {
  // Error: string not assignable to number
  x.val = String(x.val + 1);
}

Heifer-type: Verifies type transition

let inc_inplace x = failwith "assume"
 (*@ assume
   req x->#Ref[int];
   ens x->#Ref[str]
 @*)

Key insight: Ref[int] before → Ref[str] after. TypeScript has no concept of type-state.

Aliasing Split

swap(x, x) vs swap(x, y)

TypeScript gives both calls the same type. Heifer separates them: disjoint ownership (*) vs aliased case (x=y).

TypeScript: Same type for both calls

// TS: swap(x, x) and swap(x, y)
// are completely indistinguishable
function swap(x: any, y: any): void {
  const t = x.val;
  x.val = y.val;
  y.val = t;
}

Heifer-type: Separate verified cases

let swap x y = failwith "assume"
 (*@ assume
   req x->#Ref[a'] /\ x=y;
   ens x->#Ref[a'] /\ x=y
 $ req x->#Ref[a'] * y->#Ref[b'];
   ens x->#Ref[b'] * y->#Ref[a']
 @*)

Key insight: * is separating conjunction — asserts x and y are disjoint heap locations.

Deep Structure

list_seg

TypeScript treats all arrays as T[] with no structural constraints. Heifer reasons about exact linked-list shapes and entails them to abstract predicates.

TypeScript: Unconstrained array (any[])

// TS: no structural constraints at all
// x is just "any" — could be anything
function list_seg(x: any): any {
  return x;
}

Heifer-type: Verified structural cases

let list_seg x = failwith "assume"
 (*@ assume
   req x->#Cons[int,y]
     * y->#Cons[int,z]
     * z->#Cons[int,Nil[]];
   ens x->#List[int] /\ res=x
 $ req x->#Cons[1,y]
     * y->#Cons[2,z]
     * z->#Cons[3,Nil[]];
   ens x->#List[int] /\ res=x
 @*)

Key insight: Heifer proves that a concrete 3-element Cons chain entails the abstract List[int] predicate.

All Spec Patterns

12 functions covering every separation-logic pattern in Heifer-type's test suite

plus

Simple integer addition with precise types

Value typesTS imprecise

let plus x y = failwith "assume"
 (*@ assume req x:#int /\ y:#int; ens res:#int @*)

Heifer: Verifies: both inputs and output are int

deref

Dereference — heap form vs value form

Heap ownershipTS imprecise

let deref x = failwith "assume"
 (*@ assume req x:#Ref[t']; ens res:#t'
  $ req x->#Ref[t']; ens x->#Ref[t'] /\ res:#t' @*)

Heifer: Two cases: value-form and heap-ownership-form — both verified

inc_inplace

Type mutation — int cell becomes str cell

Type-state / ownership mutationTS rejects

let inc_inplace x = failwith "assume"
 (*@ assume req x->#Ref[int]; ens x->#Ref[str] @*)

Heifer: Tracks type change: Ref[int] → Ref[str] across the call

swap

Aliased vs disjoint heap — separating conjunction

Separation / aliasingTS unsound

let swap x y = failwith "assume"
 (*@ assume req x->#Ref[a'] /\ x=y; ens x->#Ref[a'] /\ x=y
  $ req x->#Ref[a'] * y->#Ref[b']; ens x->#Ref[b'] * y->#Ref[a'] @*)

Heifer: * asserts disjoint heap; aliased case handled separately

tail

List tail — multi-case spec with Err on Nil

ADT dispatch / error typesTS imprecise

let tail x = failwith "assume"
 (*@ assume req x:#Cons[t',List[t']]; ens res:#List[t']
  $ req x:#Nil[]; ens res:#Err[] @*)

Heifer: Proves exhaustive case split: Cons returns List, Nil returns Err

id2

Parametric identity — forall quantifier

Parametric polymorphismTS imprecise

let id2 y = failwith "assume"
 (*@ assume forall t. req y:#t'; ens res:#t' @*)

Heifer: forall t proves the spec holds for every type, not just syntactically

make_ref

Allocate a new heap cell — ownership creation

Heap allocationTS imprecise

let make_ref x = failwith "assume"
 (*@ assume req x:#a'; ens res->#Ref[x] /\ x:#a' @*)

Heifer: res owns a fresh heap cell containing exactly x — TypeScript can't express ownership

update

Type-changing store — m changes from t' to a'

Type mutationTS unsound

let update m v = failwith "assume"
 (*@ assume req m->#Ref[t'] /\ v:#a'; ens m->#Ref[a'] @*)

Heifer: m's cell type changes from t' to a' — a type-state transition

list_seg

Three-element list segment — deep structural reasoning

List structureTS imprecise

let list_seg x = failwith "assume"
 (*@ assume req x->#Cons[int,y] * y->#Cons[int,z] * z->#Cons[int,Nil[]]; ens x->#List[int] /\ res=x
  $ req x->#Cons[1,y] * y->#Cons[2,z] * z->#Cons[3,Nil[]]; ens x->#List[int] /\ res=x
  $ req x->#Nil[]; ens x->#List[a'] /\ res = x @*)

Heifer: Reasons about concrete list shapes, exact values, and entailment to List[int]

map

Higher-order map — recursive, polymorphic, heap and value forms

Recursive polymorphismTS imprecise

let rec map f xs = failwith "assume"
 (*@ assume req f:#Any /\ xs:#Nil[]; ens res:#Nil[]
  $ req f:#(a'->b') /\ xs:#Cons[a',List[a']]; ens res:#Cons[b',List[b']] @*)

Heifer: Proves list structure is preserved: Cons[a'] in → Cons[b'] out

partial_app

Partial application — function type as first-class constraint

Higher-order / partial applicationTS imprecise

let partial_app x = failwith "assume"
 (*@ assume req plus:#(int->int->int) /\ x:#int; ens res:#int->int @*)

Heifer: Function types are logical constraints, not just annotations

two_pointer

Pointer-to-pointer aliasing — x now points to y's cell

Pointer aliasingTS unsound

let two_pointer x y = failwith "assume"
 (*@ assume req x->#Ref[a'] * y->#Ref[b']; ens x->#Ref[Ref[b']]
  $ req x->#Ref[a'] /\ x=y; ens x->#Ref[y] /\ x=y @*)

Heifer: x->#Ref[Ref[b']] expresses pointer-to-pointer — TypeScript has no such type

TypeScript vs Heifer-type

15 patterns where TypeScript falls short — and how Heifer-type's separation logic fills the gap

#	Pattern	TypeScript	Heifer-type spec	Why TypeScript fails
1	Parametric identity	`<T>(y: T): T` — syntactic, not verified	`forall t. req y:#t'; ens res:#t'`	TS checks syntax; Heifer proves the heap entailment holds
2	Predicate fold/unfold	No concept — TS has no named heap predicates	`req p_list(x); ens res=x /\ p_list(x)`	TS cannot abstract over heap shapes
3	Heap vs value duality	`deref(x: any): any` — loses type info	`req x->#Ref[t']; ens x->#Ref[t'] /\ res:#t'`	TS erases the distinction between heap cells and values
4	Type mutation	Forbids typed mutation; accepts untyped `any`	`req x->#Ref[int]; ens x->#Ref[str]`	TS checks snapshots; Heifer tracks state transitions
5	Aliasing split	`swap(x: any, y: any)` — no aliasing detection	`req x->#Ref[a'] /\ x=y; ens x->#Ref[a'] /\ x=y`	TS cannot express disjoint vs aliased ownership
6	Disjoint ownership	Same type as aliased — indistinguishable	`req x->#Ref[a'] * y->#Ref[b']; ens x->#Ref[b'] * y->#Ref[a']`	`*` is separating conjunction — TS has no analog
7	ADT constructor dispatch	`typeof` narrows syntactically, no verification	`req y:#Int[int]; ens res:#Int[int] $ req y:#Str[str]; ens res:#Str[str]`	Heifer proves the match is exhaustive and each arm correct
8	Disjunctive return type	`T \| Error` — accepts `x: null` without warning	`req x:#Cons[...]; ens res:#List[t'] $ req x:#Nil[]; ens res:#Err[]`	Spec precisely models the failure case
9	List segment shape	`any[]` or `T[]` — no structural constraint	`req x->#Cons[int,y] * y->#Cons[int,z] * z->#Cons[int,Nil[]]`	TS length/structure is runtime; Heifer reasons statically
10	Create reference + ownership	`make_ref<T>(x: T): {val: T}` — correct but no ownership	`req x:#a'; ens res->#Ref[x] /\ x:#a'`	TS cannot express that `res` owns a new heap cell
11	Type-changing update	`update(m: {val: any}, v: any)` — unconstrained	`req m->#Ref[t'] /\ v:#a'; ens m->#Ref[a']`	TS cannot express that m's cell type changes after update
12	Two-pointer aliasing	`(x: any, y: any) => x.val = y` — no pointer type	`req x->#Ref[a'] * y->#Ref[b']; ens x->#Ref[Ref[b']]`	TS cannot state that x now points to y's heap location
13	Completeness	`(x: any): any` — return type imprecise	`req x:#List[a']; ens res:#(List[a'] \/ Err[])`	TS unions are syntactic; Heifer proves exhaustiveness
14	Recursive map types	`map<A,B>(f:(a:A)=>B, xs:A[]): B[]` — shallow	Four cases: Nil/Cons × value/heap — both verified	TS doesn't verify list structure is preserved
15	Partial application	`partial_app(x: number) => (y: number) => number`	`req plus:#(int->int->int) /\ x:#int; ens res:#int->int`	Heifer specs constrain function types in the logic

Spec Syntax Reference

x:#intx evaluates to an int

x->#Ref[int]x points to a heap cell holding int

P * QP and Q on disjoint heap regions

P /\ QP and Q (same heap)

P \/ QP or Q holds

P $ Qcase split: P OR Q (multi-spec)

req P; ens Qprecondition P, postcondition Q

forall t.universal type quantifier

#Ref[t']heap cell holding type t'

#List[t']abstract list predicate

#Cons[h,t]constructor node: head h, tail t

#Nil[]empty list / nil constructor