diff --git a/README.md b/README.md
index 0140c75a..e54ed457 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,3 @@
-
 # HVM-Core: a parallel Interaction Combinator evaluator
 
 HVM-Core is a parallel evaluator for extended [Symmetric Interaction Combinators](https://www-lipn.univ-paris13.fr/~mazza/papers/CombSem-MSCS.pdf).
@@ -9,7 +8,7 @@ optimal evaluation semantics and concurrent model of computation make it a great
 compile target for high-level languages seeking massive parallelism.
 
 HVM-Core will be used as the compile target for
-[HVM](https://github.com/higherorderco/hvm1) on its upcoming update, available at [HVM-lang](https://github.com/higherorderco/hvm-lang)
+[HVM](https://github.com/higherorderco/hvm) on its upcoming update.
 
 ## Usage
 
@@ -79,18 +78,18 @@ HVM-Core's textual syntax represents interaction combinators via an AST:
 ```
 <TERM> ::=
   <ERA> ::= "*"
-  <CON> ::= "(" <TERM>{0-8} ")"
-  <TUP> ::= "[" <TERM>{0-8} "]"
-  <DUP> ::= "{" <label> " " <TERM>{0-8} "}"
+  <CON> ::= "(" <TERM> " " <TERM> ")"
+  <TUP> ::= "[" <TERM> " " <TERM> "]"
+  <DUP> ::= "{" <label> " " <TERM> " " <TERM> "}"
   <REF> ::= "@" <name>
   <U60> ::= "#" <value>
   <OP2> ::= "<" <op> " " <TERM> " " <TERM> ">"
-  <MAT> ::= "?" "<" <TERM> " " <TERM> " " <TERM> ">"
+  <MAT> ::= "?" "<" <TERM> " " <TERM> ">"
   <VAR> ::= <name>
 
 <NET> ::=
   <ROOT> ::= <TERM>
-  <REDEX> ::= <NET> "&" <TERM> "~" <TERM>
+  <REDEX> ::= "&" <TERM> "~" <TERM> <NET>
 
 <BOOK> ::= 
   <DEF> ::= "@" <name> "=" <NET> <BOOK>
@@ -120,7 +119,7 @@ integers, numeric operations and numeric pattern-matching.
 
 - `U60`: an unboxed 60-bit unsigned integer.
 
-- `OP`: a binary operation on u60 operands.
+- `OP2`: a binary operation on u60 operands.
 
 - `MAT`: a pattern-matching operator on u60 values.
 
@@ -157,15 +156,102 @@ hierarchy, the wires between aux ports are denoted by named variables, and the
 single wire between main ports is denoted by the `& A ~ B` syntax. Note this
 always represents an active pair (or redex)!
 
-## Node types and interactions
+## CPU Evaluator
+
+HVMC's main evaluator is a Rust package that runs on the CPU, although GPU
+versions are in development (see below). It is completely eager, which means it
+will reduce *every* generated active pair (redex) in an ultra-greedy,
+massively-parallel fashion. 
+
+The evaluator works by keeping a vector of current active pairs (redexes) and,
+for each redex in parallel, performing local "interaction", or "graph rewrite",
+as described below. To distribute work, a simple task stealing queue is used.
+
+Note that, due to HVM's ultra-strict evaluator, languages targeting it should
+convert top-level definitions to
+[supercombinators](https://en.wikipedia.org/wiki/Supercombinator), which enables
+recursive definitions halt. HVM-Lang performs this transformation before
+converting to HVM-Core.
+
+## GPU Evaluator
+
+The GPU evaluator is similar to the CPU one, except two main differences: "1/4"
+rewrites and a task-sharing grid.  For example, on NVidia's RTX 4090, we keep a
+grid of 128x128 redex bags, where each bag contains redexes to be processed by a
+"squad", which consists of 4 threads, each one performing "1/4" of the rewrite,
+which increases the granularity. This allows us to keep `16,384` active squads,
+for a total of `65,536` active threads, which means the maximum degree of
+parallelism (65k) is achieved at just 16k redexes. Visually:
+
+```
+REDEX ::= (Ptr32, Ptr32)
+
+    A1 --|\        /|-- B2
+         | |A0--B0| |
+    A2 --|/        \|-- B1
+
+REDEX_BAG ::= Vec<REDEX>
+
+    [(A0,B0), (C0,D0), (E0,F0), ...]
+
+REDEX_GRID ::= Matrix<128, 128 REDEX_BAG>
+
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
+     |      |      |      |      |      |      |      |
+    ...    ...    ...    ...    ...    ...    ...    ... 
+
+SQUAD ::= Vec<4, THREAD>
+
+THREAD ::=
+
+    loop {
+      if (A, B) = pop_redex():
+        atomic_rewrite(A, B)
+      share_redexes()
+    }
+
+    atomic_rewrite(A, B):
+      ... match redex type ...
+      ... perform atomic links ...
+
+    atomic_link(a, b):
+      ... see algorithm on 'paper/' ...
+
+RESULT:
+
+    - thread 0 links A1 -> B1
+    - thread 1 links B1 -> A1
+    - thread 2 links A2 -> B2
+    - thread 3 links B2 -> A2
+
+OUTPUT:
+
+    A1 <--------------> B1
+    A2 <--------------> B2
+```
+
+
+## Interactions
 
 The available interactions are the same described on the reference paper, namely
 annihilation and commutation rules, plus a few additional interactions,
-including primitive numeric operations, conditionals, and dereference.
-
-### Ctr and Era
+including primitive numeric operations, conditionals, and dereference. The core
+interactions are:
 
-`Ctr` and `Era` are the two basic node types that are present in the original interaction combinators paper. However, unlike in regular Interaction Combinators, `hvm-core` has up to 65535 distinct 2-ary combinators instead of just 2. This is an _extension_ to "pure" IC that is useful to implement many common patterns, such as duplications and tuples. `hvm-core` would have the same power if it had only 2 combinator labels; however; programs written in it would have decreased performance.
 ```
 ()---()
 ~~~~~~~ ERA-ERA
@@ -204,37 +290,58 @@ A1 --|b|       |a|-- B2
 A2 --|b|       |a|-- B1
       \|-------|/
 ```
-### Num, Op, and Mat
 
-`hvm-core` allows programs to employ the host architecture's native number operators. `hvm-core` numbers are 60 bits long. 
+The dereference interactions happen when a @REF node interacts with another
+node. When that node is a constructor, the dereference will be unrolled
+efficiently. This makes HVM practical, because, without it, top-level
+definitions would need to be implemented with DUP nodes. This would cause
+considerable overhead when trying to implement functions, due to DUP nodes
+incremental copying nature. When the other node is anything else, that implies
+two closed nets got disconnected from the main graph, so both nodes are
+collected, allowing recursive functions to halt without infinite expansions.
 
-- `Num` is a 60-bit unsigned integer type. 
--  `Op` is a binary operation carried out on the integer in its principal port.
-- `Mat` is a match operator that can pattern-match on numbers, which allows branching when working with native integers.
+```
+() -- @REF
+~~~~~~~~~~ ERA-REF
+nothing
+```
 
-#### Op
+```
+A1 --|\
+     | |-- @REF
+A2 --|/
+~~~~~~~~~~~~~~~~ CTR-REF
+A1 --|\
+     | |-- {val}
+A2 --|/
+```
 
-An `Op` node is a 2-ary node that carries out an operation on the numbers between the numbers in its principal port and its first auxiliary port.
+Since Interaction Combinator nodes only have 1 active port, which is a property
+that is essential for key computational characteristics such as strong
+confluence, we can't have a binary numeric operation node. Instead, we split
+numeric operations in two nodes: OP2, which processes the first operand and
+returns an OP1 node, which then processes the second operand, performs the
+computation, and connects the result to the return wire.
 
 ```
-      /-----|1--- #Y
-#X --|Op[op]|
-      \-----|2--- out
-~~~~~~~~~~~~~~~~~~~~~~~ OP-NUM (A)
-#op(X, Y) ---- out
-
-      /-----|1--- other // (if `other` is not a Num)
-#X --|Op[op]|
-      \-----|2--- out
-~~~~~~~~~~~~~~~~~~~~~~~ OP-NUM (B)
-         /------|1--- #X
-other --|Op[op']|              // Operator inside Op node gets flipped
-         \------|2--- out
+A1 --,
+     [}-- #X
+A2 --' 
+~~~~~~~~~~~~~~ OP2-NUM
+A2 --[#X}-- A1
 ```
 
-The Op node commutes with other 
+```
+A1 --[#X}-- #Y
+~~~~~~~~~~~~~~ OP1-NUM
+A1 -- #Z
+```
 
-There are 16 supported operations. (plus their swapped versions, which aren't shown here)
+Note that the OP2 operator doesn't store the operation type. Instead, it is
+stored on 4 unused bits of the left operand. As such, an additional operation
+called "load-op-type" is used to load the next operation on the left operand.
+See the `/examples` directory for more info. Below is a table with all available
+operations:
 
 sym | name
 --- | ---------
@@ -256,92 +363,38 @@ sym | name
 `<<`| left-shift
 `>>`| right-shift
 
-
-### Mat
-
-Mat is a 3-ary pattern matching nodes with three auxiliary ports, `zero`, `succ`, and `out`
+Since HVM already provides plenty of solutions for branching (global references,
+lambda encoded booleans and pattern-matching, etc.), the pattern-match operation
+is only necessary to read bits from numbers: otherwise, numbers would be "black
+boxes" that can't interact with the rest of the program. The way it works is
+simple: it receives a number, two branches (case-zero and case-succ, stored in a
+CON node) and a return wire. If the number is 0, it erases the case-succ branch
+and returns the case-zero branch. Otherwise, it erases the case-zero branch and
+returns the case-succ branch applied to the predecessor of the number.
 
 ```
-zero --,
-succ --(?)-- #X
- out --' 
+A1 --,
+     (?)-- #X
+A2 --' 
 ~~~~~~~~~~~~~~~~~~ MAT-NUM (#X > 0)
-        /|-- out
-succ --| |
-        \|-- #(X-1)
-       
-zero -- ()
-
-
-zero --,
-succ --(?)-- #X
- out --' 
-~~~~~~~~~~~~~~~~~~ MAT-NUM (#X > 0)
-zero -- out
-succ -- ()
+           /|-- A2
+      /|--| |
+A1 --| |   \|-- #(X-1)
+      \|-- ()
 ```
-Since HVM already provides plenty of solutions for branching (global references,
-lambda encoded booleans and pattern-matching, etc.), the pattern-match operation
-is only necessary to read bits from numbers: otherwise, numbers would be "black
-boxes" that can't interact with the rest of the program. 
 
+```
+A1 --,
+     (?)-- #X
+A2 --' 
+~~~~~~~~~~~~~~~~~~ MAT-NUM (#X == 0)
+      /|-- ()
+A1 --| |   
+      \|-- A2
+```
 
 Note that some interactions like NUM-ERA are omitted, but should logically
 follow from the ones described above.
-### REF nodes
-
-REF nodes stand for "reference" nodes. However, they are much more powerful than that.
-
-Most REF nodes refer to closed nets. Interaction with these will "expand" the closed net, which is stored inside the REF.
-
-However, REF nodes allow a library that imports `hvm-core` to define arbitrary interactions, which might interact with the environment and call external functions. 
-
-### n-ary nodes
-
-`hvm-core` supports CTR nodes with up to 8 auxiliary ports. These are actually just optimized versions of trees of smaller nodes. 
-
-For example, `(a b c d e f)` is equivalent to `(a (b (c (d (e f)))))`. However, the redex `(a b c d e f) ~ (i j k l m n) `will reduce in just 1 step compared to the 6 steps and the pointer-chasing that are necessary to reduce `(a (b (c (d (e f))))) ~ (i (j (k (l (m n)))))`
-
-### ADT nodes
-
-ADT nodes are compact versions of a common combination of 2 n-ary nodes, which are usually used to represent Scott ADTs.
-
-In the textual syntax, they look like this:
-
-`(:1:2 a b)`
-
-This represents an ADT node with 2 variants and with variant index 1 (indices start from 0). It has two fields: `a` and `b`.
-
-Here's a list of examples which should be enough to show how they work.
-```
-As CTR tree: (* ((a R) R))
-ADT node:    (:1:2 a)
-λ-calculus:  λ* λx (x a)
-
-((a R) (* R))
-(:0:2 a)
-λx λ* (x a)
-
-(* (* ((a R) R)))
-(:2:3 a)
-λ* λ* λx (x a)
-
-(* ((a R) (* R)))
-(:1:3 a)
-λ* λx λ* (x a)
-
-((a (b R)) R)
-(:0:1 a b)
-λp (p a b)
-
-((a (b (c R))) R)
-(:0:1 a b c)
-λp (p a b c)
-
-(* ((a (b (c R))) R))
-(:1:2 a b c)
-λ* λp (p a b c)
-```
 
 ## Memory Layout
 
@@ -374,33 +427,24 @@ struct Net {
 As you can see, the memory layout resembles the textual syntax, with nets being
 represented as a vector of trees, with the 'redex' buffer storing the tree roots
 (as active pairs), and the 'nodes' buffer storing all the nodes. Each node has
-two 64-bit pointers and, thus, uses exactly 128 bits. 
-
-[comment]: <> (/* cSpell:disable */)
-``` 
-                                                             2-0
-                                                              v 
-[63----------48][47----------------------------------------3][-]
-LLLLLLLLLLLLLLLLAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAATTT
-[----Label-----][------------------Address------------------][-]
-                                                              ^
-                                                             Tag
-```
-[comment]: <> (/* cSpell:enable */)
-
-Pointers include a 4-bit tag, a 16-bit label (used for DUP labels, OP operators) and a 48-bit aligned addr,
-which allows addressing a 281 TB space per instance. There are 7 pointer types:
+two 32-bit pointers and, thus, uses exactly 64 bits. Pointers include a 4-bit
+tag, a 28-bit label (used for DUP colors, OP2 operators) and a 32-bit addr,
+which allows addressing a 2 GB space per instance. There are 12 pointer types:
+
 ```rust
-  pub enum Tag {
-    Red = 0,
-    Var = 1,
-    Ref = 2,
-    Num = 3,
-    Op = 4,
-    /* Coming soon :) */ = 5,
-    Mat = 6,
-    Ctr = 7,
-  }
+VR1: Tag = 0x0; // Variable to aux port 1
+VR2: Tag = 0x1; // Variable to aux port 2
+RD1: Tag = 0x2; // Redirect to aux port 1
+RD2: Tag = 0x3; // Redirect to aux port 2
+REF: Tag = 0x4; // Lazy closed net
+ERA: Tag = 0x5; // Unboxed eraser
+NUM: Tag = 0x6; // Unboxed number
+OP2: Tag = 0x7; // Binary numeric operation
+OP1: Tag = 0x8; // Unary numeric operation
+MAT: Tag = 0x9; // Numeric pattern-matching
+LAM: Tag = 0xA; // Main port of lam node
+TUP: Tag = 0xB; // Main port of tup node
+DUP: Tag = 0xC; // Main port of dup node
 ```
 
 This memory-efficient format allows for a fast implementation in many
@@ -425,95 +469,6 @@ with a ~46% efficiency using interaction-net-based trees. This structure isn't
 as compact as arrays, but it allows us access and transform data in parallel,
 which is a great tradeoff in practice.
 
-## CPU Evaluator
-
-HVMC's main evaluator is a Rust package that runs on the CPU, although GPU
-versions are in development (see below). It is completely eager, which means it
-will reduce *every* generated active pair (redex) in an ultra-greedy,
-massively-parallel fashion. 
-
-The evaluator works by keeping a vector of current active pairs (redexes) and,
-for each redex in parallel, performing local "interaction", or "graph rewrite",
-as described below. To distribute work, a simple task stealing queue is used.
-
-Note that, due to HVM's ultra-strict evaluator, languages targeting it should
-convert top-level definitions to
-[supercombinators](https://en.wikipedia.org/wiki/Supercombinator), which enables
-recursive definitions halt. HVM-Lang performs this transformation before
-converting to HVM-Core.
-
-## GPU Evaluator
-
-The GPU evaluator is similar to the CPU one, except two main differences: "1/4"
-rewrites and a task-sharing grid.  For example, on NVidia's RTX 4090, we keep a
-grid of 128x128 redex bags, where each bag contains redexes to be processed by a
-"squad", which consists of 4 threads, each one performing "1/4" of the rewrite,
-which increases the granularity. This allows us to keep `16,384` active squads,
-for a total of `65,536` active threads, which means the maximum degree of
-parallelism (65k) is achieved at just 16k redexes. Visually:
-
-```
-REDEX ::= (Ptr32, Ptr32)
-
-    A1 --|\        /|-- B2
-         | |A0--B0| |
-    A2 --|/        \|-- B1
-
-REDEX_BAG ::= Vec<REDEX>
-
-    [(A0,B0), (C0,D0), (E0,F0), ...]
-
-REDEX_GRID ::= Matrix<128, 128 REDEX_BAG>
-
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] -- [ ] ...
-     |      |      |      |      |      |      |      |
-    ...    ...    ...    ...    ...    ...    ...    ... 
-
-SQUAD ::= Vec<4, THREAD>
-
-THREAD ::=
-
-    loop {
-      if (A, B) = pop_redex():
-        atomic_rewrite(A, B)
-      share_redexes()
-    }
-
-    atomic_rewrite(A, B):
-      ... match redex type ...
-      ... perform atomic links ...
-
-    atomic_link(a, b):
-      ... see algorithm on 'paper/' ...
-
-RESULT:
-
-    - thread 0 links A1 -> B1
-    - thread 1 links B1 -> A1
-    - thread 2 links A2 -> B2
-    - thread 3 links B2 -> A2
-
-OUTPUT:
-
-    A1 <--------------> B1
-    A2 <--------------> B2
-```
-
-
 ## Lock-free Algorithm
 
 At the heart of HVM-Core's massively parallel evaluator lies a lock-free