| Symbol | Specification | Kind | Type |
|---|
| # . | refset | f | refset → nat |
| # . | heap | f | heap → nat |
| # . | tree | f | tree → nat |
| . * . | heap-sep | f | (heap → bool) × (heap → bool) → heap → bool |
| . + . | nat-basic | f | nat × nat → nat |
| . ++ . | refset | f | refset × ref → refset |
| . ++ . | heap | f | heap × ref → heap |
| . +1 | nat-basic | f | nat → nat |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -* . | heap-sep | f | (heap → bool) × (heap → bool) → heap → bool |
| . -- . | refset | f | refset × ref → refset |
| . -- . | heap | f | heap × ref → heap |
| . -> . | heap-sep | f | (heap → bool) × (heap → bool) → heap → bool |
| . -⊗ . | heap-sep | f | (heap → bool) × (heap → bool) → heap → bool |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . .left | node | f | node → ref |
| . .left | tree | pf | tree → tree with λ t. t ≠ leaf |
| . .left:= . | node | f | node × ref → node |
| . .left:= . | tree | pf | tree × tree → tree with λ t, t0. t ≠ leaf |
| . .right | node | f | node → ref |
| . .right | tree | pf | tree → tree with λ t. t ≠ leaf |
| . .right:= . | node | f | node × ref → node |
| . .right:= . | tree | pf | tree × tree → tree with λ t, t0. t ≠ leaf |
| . .val | node | f | node → elem |
| . .val | tree | pf | tree → elem with λ t. t ≠ leaf |
| . .val:= . | node | f | node × elem → node |
| . .val:= . | tree | pf | tree × elem → tree with λ t, val. t ≠ leaf |
| . < . | nat-basic | p | nat × nat |
| . => . | node-heap | f | ref × node → heap → bool |
| . =>? | maplet | f | ref → heap → bool |
| . =>_ | maplet | f | ref → heap → bool |
| . > . | nat | p | nat × nat |
| . [ . ] | node-heap | f | heap × ref → node |
| . [ . ] | node-heap | f | heap × ref × node → heap |
| . \ . | refset | f | refset × refset → refset |
| . \ . | heap | f | heap × refset → heap |
| . \ . | heap | f | heap × heap → heap |
| . ∈ . | refset | p | ref × refset |
| . ∈ . | heap | p | ref × heap |
| . ∩ . | refset | f | refset × refset → refset |
| . ∪ . | refset | f | refset × refset → refset |
| . ∪ . | heap | f | heap × heap → heap |
| . ≡ . | separation | p | heap × heap |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | refset | p | refset × refset |
| . ⊆ . | heap | p | heap × heap |
| . ⊆ . | heap-sep | p | (heap → bool) × (heap → bool) |
| . ⊗ . | heap-sep | f | (heap → bool) × (heap → bool) → heap → bool |
| . ⊥ . | heap | p | heap × heap |
| . and . | heap-sep | f | (heap → bool) × (heap → bool) → heap → bool |
| . or . | heap-sep | f | (heap → bool) × (heap → bool) → heap → bool |
| _∃ . | maplet | f | (ref → heap → bool) → heap → bool |
| _∃ . | maplet | f | (ref × ref → heap → bool) → heap → bool |
| _∃ . | node-heap | f | (node → heap → bool) → heap → bool |
| { . } | refset | f | ref → refset |
| { . } | heap-sep | f | heap → heap → bool |
| ∅ | refset | c | refset |
| ∅ | heap | c | heap |
| ⌜ . ⌝ | heap-sep | f | bool → heap → bool |
| True | separation | p | bool |
| a | linked-tree | v | elem |
| alloc | ops | pr | : ref × heap (nondeterministic) |
| alloc# | ops | pr | refset : ref × heap (nondeterministic) |
| branch | tree | f | tree × elem × tree → tree |
| dom . | heap | f | heap → refset |
| elem | elem | s | |
| emp | heap-sep | p | heap |
| false | heap-sep | p | heap |
| free | ops | pr | ref : heap |
| h | linked-tree | v | heap |
| hP | linked-tree | v | heap → bool |
| heap | heap | s | |
| ite | heap-sep | f | bool × (heap → bool) × (heap → bool) → heap → bool |
| leaf | tree | c | tree |
| mknode | node | f | ref × elem × ref → node |
| nat | nat-basic | s | |
| node | node | s | |
| not . | heap-sep | f | (heap → bool) → heap → bool |
| null | ref | c | ref |
| precise | heap-sep | p | (heap → bool) |
| r | linked-tree | v | ref |
| read | node-heap | pr | ref × heap : : node |
| ref | ref | s | |
| refset | refset | s | |
| t | linked-tree | v | tree |
| tr | linked-tree | f | ref × tree → heap → bool |
| tree | tree | s | |
| true | heap-sep | p | heap |
| write | node-heap | pr | ref × node : heap |