diff --git a/Cargo.lock b/Cargo.lock
index bfb5320c6fffa6fdedf2475f23c8c6436f9a9739..13eff2b427c1bf146fa6b064977f498e93e70b2f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -56,6 +56,18 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
 
+[[package]]
+name = "bitvec"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1bc2832c24239b0141d5674bb9174f9d68a8b5b3f2753311927c172ca46f7e9c"
+dependencies = [
+ "funty",
+ "radium",
+ "tap",
+ "wyz",
+]
+
 [[package]]
 name = "clap"
 version = "4.4.2"
@@ -102,6 +114,12 @@ version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7"
 
+[[package]]
+name = "funty"
+version = "2.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e6d5a32815ae3f33302d95fdcb2ce17862f8c65363dcfd29360480ba1001fc9c"
+
 [[package]]
 name = "heck"
 version = "0.4.1"
@@ -112,6 +130,7 @@ checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8"
 name = "hercules_ir"
 version = "0.1.0"
 dependencies = [
+ "bitvec",
  "nom",
  "ordered-float",
 ]
@@ -182,6 +201,12 @@ dependencies = [
  "proc-macro2",
 ]
 
+[[package]]
+name = "radium"
+version = "0.7.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dc33ff2d4973d518d823d61aa239014831e521c75da58e3df4840d3f47749d09"
+
 [[package]]
 name = "strsim"
 version = "0.10.0"
@@ -199,6 +224,12 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "tap"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "55937e1799185b12863d447f42597ed69d9928686b8d88a1df17376a097d8369"
+
 [[package]]
 name = "unicode-ident"
 version = "1.0.11"
@@ -276,3 +307,12 @@ name = "windows_x86_64_msvc"
 version = "0.48.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538"
+
+[[package]]
+name = "wyz"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "05f360fc0b24296329c78fda852a1e9ae82de9cf7b27dae4b7f62f118f77b9ed"
+dependencies = [
+ "tap",
+]
diff --git a/DESIGN.md b/DESIGN.md
index 9d5d7ddd9c5e41c20c1a9cc2c526c946960ce4ff..cd51e630fe4316741a31778e104c747529a6f294 100644
--- a/DESIGN.md
+++ b/DESIGN.md
@@ -24,28 +24,36 @@ The Hercules' compiler is split into the following components:
 
 The IR of the Hercules compiler is similar to the sea of nodes IR presented in "A Simple Graph-Based Intermediate Representation", with a few differences.
 
-- There are dynamic constants, which are constants provided dynamically to the runtime system - these can be used to specify array types, unlike input dependent values.
-- There is no single global store. The closest analog are individual values with an array type, which support dynamic indexed read and write operations.
+- There are dynamic constants, which are constants provided dynamically to the runtime system - these can be used to specify array type sizes, unlike normal runtime values.
+- There is no single global store. The closest analog are individual values with an array type, which support dynamically indexed read and write operations.
 - There is no I/O, or other side effects.
 - There is no recursion.
 - The implementation of Hercules IR does not follow the original object oriented design.
 
 A key design consideration of Hercules IR is the absence of a concept of memory. A downside of this approach is that any language targetting Hecules IR must also be very restrictive regarding memory - in practice, this means tightly controlling or eliminating first-class references. The upside is that the compiler has complete freedom to layout data however it likes in memory when performing code generation. This includes deciding which data resides in which address spaces, which is a necessary ability for a compiler striving to have fine-grained control over what operations are computed on what devices.
 
-In addition to not having a generalized memory, Hercules IR has no functionality for calling functions with side-effects, or doing IO. In other words, Hercules is a pure IR (it's not functional, as functions aren't first class values). This may be changed in the future - we could support effectful programs by giving call operators a control input and output edge. However, at least for now, we need to work with the simplest IR possible.
+In addition to not having a generalized memory, Hercules IR has no functionality for calling functions with side-effects, or doing IO. In other words, Hercules is a pure IR (it's not functional, as functions aren't first class values). This may be changed in the future - we could support effectful programs by giving call operators a control input and output edge. However, at least for now, we need to work with the simplest IR possible, so the IR is pure.
 
 ### Optimizations
 
+Hercules relies on other compiler infrastructures, such as LLVM, to do code generation for specific devices. Thus, Hercules itself doesn't perform particularly sophisticated optimizations. In general, the optimizations Hercules do are done to make partitioning easier. This includes things like GVN and peephole optimizations, which in general, make the IR "simpler".
+
 TODO: @rarbore2
 
 ### Partitioning
 
+Partitioning is responsible for deciding which operations in the IR graph are executed on which devices. Additionally, operations are broken up into shards - every node in a shard executes on the same device, and the runtime system schedules execution at the shard level. Partitioning is conceptually very similar to instruction selection. Each shard can be thought of as a single instruction, and the device the shard is executed on can be thought of as the particular instruction being selected. In instruction selection, there is not only the choice of which instructions to use, but also how to partition the potentially many operations in the IR into a smaller number of target instructions. Similarly, partitioning Hercules IR must decide which operations are grouped together into the same shard, and for each shard, which device it should execute on. The set of operations each potential target device is capable of executing is crucial information when forming the shard boundaries, so this cannot be performed optimally as a sequential two step process.
+
 TODO: @rarbore2
 
 ### Code Generation
 
 Hercules uses LLVM for generating CPU and GPU code. Memory is "introduced" into the program representation at this stage. Operations in a function are separated into basic blocks. The data layout of values is decided on, and memory is allocated on the stack or is designated as separately allocated and passed into functions as necessary. Code is generated corresponding to possibly several estimates of dynamic constants.
 
+TODO: @rarbore2
+
 ## Runtime System
 
 The runtime system is responsible for dynamically executing code generated by Hercules. It exposes a Rust API for executing Hercules code. It takes care of memory allocation, synchronization, and scheduling.
+
+TODO: @rarbore2
diff --git a/hercules_ir/Cargo.toml b/hercules_ir/Cargo.toml
index c7056cc49f2edb07b65e075eb617afd362e285a9..aab636b20b5cbfdbe2650043475baa234ae30a84 100644
--- a/hercules_ir/Cargo.toml
+++ b/hercules_ir/Cargo.toml
@@ -5,4 +5,5 @@ authors = ["Russel Arbore <rarbore2@illinois.edu>"]
 
 [dependencies]
 nom = "*"
-ordered-float = "*"
\ No newline at end of file
+ordered-float = "*"
+bitvec = "*"
\ No newline at end of file
diff --git a/hercules_ir/src/dataflow.rs b/hercules_ir/src/dataflow.rs
new file mode 100644
index 0000000000000000000000000000000000000000..9dfa68670dad8460a2dc8b2dfe1508ee28d66277
--- /dev/null
+++ b/hercules_ir/src/dataflow.rs
@@ -0,0 +1,126 @@
+extern crate bitvec;
+
+use dataflow::bitvec::prelude::*;
+
+use crate::*;
+
+/*
+ * Trait for a type that is a semilattice. Semilattice types must also be Eq,
+ * so that the dataflow analysis can determine when to terminate.
+ */
+pub trait Semilattice: Eq {
+    fn meet(a: &Self, b: &Self) -> Self;
+    fn bottom() -> Self;
+    fn top() -> Self;
+}
+
+/*
+ * Top level forward dataflow function. This routine is slightly more generic
+ * than the typical textbook definition. The flow function takes an ordered
+ * slice of predecessor lattice values, rather than a single lattice value.
+ * Thus, the flow function can perform non-associative and non-commutative
+ * operations on the "in" lattice values. This makes this routine more useful
+ * for some analyses, such as typechecking. To perform the typical behavior,
+ * the flow function should start by meeting the input lattice values into a
+ * single lattice value.
+ */
+pub fn forward_dataflow<L, F>(
+    function: &Function,
+    reverse_postorder: &Vec<NodeID>,
+    mut flow_function: F,
+) -> Vec<L>
+where
+    L: Semilattice,
+    F: FnMut(&[&L], &Node) -> L,
+{
+    // Step 1: compute NodeUses for each node in function.
+    let uses: Vec<NodeUses> = function.nodes.iter().map(|n| get_uses(n)).collect();
+
+    // Step 2: create initial set of "out" points.
+    let mut outs: Vec<L> = (0..function.nodes.len())
+        .map(|id| {
+            flow_function(
+                &vec![&(if id == 0 { L::bottom() } else { L::top() }); uses[id].as_ref().len()],
+                &function.nodes[id],
+            )
+        })
+        .collect();
+
+    // Step 3: peform main dataflow loop.
+    loop {
+        let mut change = false;
+
+        // Iterate nodes in reverse post order.
+        for node_id in reverse_postorder {
+            // Assemble the "out" values of the predecessors of this node. This
+            // vector's definition is hopefully LICMed out, so that we don't do
+            // an allocation per node. This can't be done manually because of
+            // Rust's ownership rules (in particular, pred_outs holds a
+            // reference to a value inside outs, which is mutated below).
+            let mut pred_outs = vec![];
+            for u in uses[node_id.idx()].as_ref() {
+                pred_outs.push(&outs[u.idx()]);
+            }
+
+            // Compute new "out" value from predecessor "out" values.
+            let new_out = flow_function(&pred_outs[..], &function.nodes[node_id.idx()]);
+            if outs[node_id.idx()] != new_out {
+                change = true;
+            }
+
+            // Update outs vector.
+            outs[node_id.idx()] = new_out;
+        }
+
+        // If no lattice value changed, we've reached the maximum fixed point
+        // solution, and can terminate.
+        if !change {
+            break;
+        }
+    }
+
+    // Step 4: return "out" set.
+    outs
+}
+
+/*
+ * Compute reverse post order of nodes in function.
+ */
+pub fn reverse_postorder(def_uses: &ImmutableDefUseMap) -> Vec<NodeID> {
+    // Initialize order vector and bitset for tracking which nodes have been
+    // visited.
+    let order = Vec::with_capacity(def_uses.num_nodes());
+    let visited = bitvec![u8, Lsb0; 0; def_uses.num_nodes()];
+
+    // Order and visited are threaded through arguments / return pair of
+    // reverse_postorder_helper for ownership reasons.
+    let (mut order, _) = reverse_postorder_helper(NodeID::new(0), def_uses, order, visited);
+
+    // Reverse order in-place.
+    order.reverse();
+    order
+}
+
+fn reverse_postorder_helper(
+    node: NodeID,
+    def_uses: &ImmutableDefUseMap,
+    mut order: Vec<NodeID>,
+    mut visited: BitVec<u8, Lsb0>,
+) -> (Vec<NodeID>, BitVec<u8, Lsb0>) {
+    if visited[node.idx()] {
+        // If already visited, return early.
+        (order, visited)
+    } else {
+        // Set visited to true.
+        visited.set(node.idx(), true);
+
+        // Iterate over users.
+        for user in def_uses.get_users(node) {
+            (order, visited) = reverse_postorder_helper(*user, def_uses, order, visited);
+        }
+
+        // After iterating users, push this node.
+        order.push(node);
+        (order, visited)
+    }
+}
diff --git a/hercules_ir/src/def_use.rs b/hercules_ir/src/def_use.rs
new file mode 100644
index 0000000000000000000000000000000000000000..0e750ca59e7e0baa237c9e6c0b0eece6d3b5a811
--- /dev/null
+++ b/hercules_ir/src/def_use.rs
@@ -0,0 +1,144 @@
+use crate::*;
+
+/*
+ * Custom type for an immutable def_use map. This is a relatively efficient
+ * storage of def_use edges, requiring 2 heap allocations.
+ */
+#[derive(Debug, Clone)]
+pub struct ImmutableDefUseMap {
+    first_edges: Vec<u32>,
+    users: Vec<NodeID>,
+}
+
+impl ImmutableDefUseMap {
+    pub fn num_edges(&self, id: NodeID) -> u32 {
+        if id.idx() + 1 < self.first_edges.len() {
+            self.first_edges[id.idx() + 1] - self.first_edges[id.idx()]
+        } else {
+            self.users.len() as u32 - self.first_edges[id.idx()]
+        }
+    }
+
+    pub fn get_users(&self, id: NodeID) -> &[NodeID] {
+        let first_edge = self.first_edges[id.idx()] as usize;
+        let num_edges = self.num_edges(id) as usize;
+        &self.users[first_edge..first_edge + num_edges]
+    }
+
+    pub fn num_nodes(&self) -> usize {
+        self.first_edges.len()
+    }
+}
+
+/*
+ * Top level def_use function.
+ */
+pub fn def_use(function: &Function) -> ImmutableDefUseMap {
+    // Step 1: get uses for each node.
+    let node_uses: Vec<NodeUses> = function.nodes.iter().map(|node| get_uses(node)).collect();
+
+    // Step 2: count number of users per node.
+    let mut num_users: Vec<u32> = vec![0; node_uses.len()];
+    for uses in node_uses.iter() {
+        for u in uses.as_ref() {
+            num_users[u.idx()] += 1;
+        }
+    }
+
+    // Step 3: assemble first_edges vector.
+    let mut first_edges: Vec<u32> = vec![];
+    let mut num_edges = 0;
+    for num_users in num_users {
+        first_edges.push(num_edges);
+        num_edges += num_users;
+    }
+
+    // Step 4: assemble users vector.
+    let mut users: Vec<NodeID> = vec![NodeID::new(0); num_edges as usize];
+    let mut num_users_per_node: Vec<u32> = vec![0; node_uses.len()];
+    for (idx, uses) in node_uses.iter().enumerate() {
+        for u in uses.as_ref() {
+            let first_edge = first_edges[u.idx()];
+            let num_users_so_far = num_users_per_node[u.idx()];
+            users[first_edge as usize + num_users_so_far as usize] = NodeID::new(idx);
+            num_users_per_node[u.idx()] = num_users_so_far + 1;
+        }
+    }
+
+    // Step 5: pack and return.
+    ImmutableDefUseMap { first_edges, users }
+}
+
+/*
+ * Enum for storing uses of node. Using get_uses, one can easily iterate over
+ * the defs that a node uses.
+ */
+#[derive(Debug, Clone)]
+pub enum NodeUses<'a> {
+    Zero,
+    One([NodeID; 1]),
+    Two([NodeID; 2]),
+    Three([NodeID; 3]),
+    Variable(&'a Box<[NodeID]>),
+    // Phi nodes are special, and store both a NodeID locally *and* many in a
+    // boxed slice. Since these NodeIDs are not stored contiguously, we have to
+    // construct a new contiguous slice by copying. Sigh.
+    Phi(Box<[NodeID]>),
+}
+
+impl<'a> AsRef<[NodeID]> for NodeUses<'a> {
+    fn as_ref(&self) -> &[NodeID] {
+        match self {
+            NodeUses::Zero => &[],
+            NodeUses::One(x) => x,
+            NodeUses::Two(x) => x,
+            NodeUses::Three(x) => x,
+            NodeUses::Variable(x) => x,
+            NodeUses::Phi(x) => x,
+        }
+    }
+}
+
+/*
+ * Construct NodeUses for a Node.
+ */
+pub fn get_uses<'a>(node: &'a Node) -> NodeUses<'a> {
+    match node {
+        Node::Start => NodeUses::Zero,
+        Node::Region { preds } => NodeUses::Variable(preds),
+        Node::If { control, cond } => NodeUses::Two([*control, *cond]),
+        Node::Fork { control, factor: _ } => NodeUses::One([*control]),
+        Node::Join { control, data } => NodeUses::Two([*control, *data]),
+        Node::Phi { control, data } => {
+            let mut uses: Vec<NodeID> = Vec::from(&data[..]);
+            uses.push(*control);
+            NodeUses::Phi(uses.into_boxed_slice())
+        }
+        Node::Return { control, value } => NodeUses::Two([*control, *value]),
+        Node::Parameter { index: _ } => NodeUses::Zero,
+        Node::Constant { id: _ } => NodeUses::Zero,
+        Node::DynamicConstant { id: _ } => NodeUses::Zero,
+        Node::Unary { input, op: _ } => NodeUses::One([*input]),
+        Node::Binary { left, right, op: _ } => NodeUses::Two([*left, *right]),
+        Node::Call {
+            function: _,
+            dynamic_constants: _,
+            args,
+        } => NodeUses::Variable(args),
+        Node::ReadProd { prod, index: _ } => NodeUses::One([*prod]),
+        Node::WriteProd {
+            prod,
+            data,
+            index: _,
+        } => NodeUses::Two([*prod, *data]),
+        Node::ReadArray { array, index } => NodeUses::Two([*array, *index]),
+        Node::WriteArray { array, data, index } => NodeUses::Three([*array, *data, *index]),
+        Node::Match { control, sum } => NodeUses::Two([*control, *sum]),
+        Node::BuildSum {
+            data,
+            sum_ty: _,
+            variant: _,
+        } => NodeUses::One([*data]),
+        Node::ExtractSum { data, variant: _ } => NodeUses::One([*data]),
+    }
+}
diff --git a/hercules_ir/src/dot.rs b/hercules_ir/src/dot.rs
index e72f118df0d0bca613758e55a77a6285c1194693..dd85cc9972f9217bcd8dbcafa13afcdd48f534ad 100644
--- a/hercules_ir/src/dot.rs
+++ b/hercules_ir/src/dot.rs
@@ -46,7 +46,7 @@ fn write_node<W: std::fmt::Write>(
         Ok((visited.get(&id).unwrap().clone(), visited))
     } else {
         let node = &module.functions[i].nodes[j];
-        let name = format!("{}_{}_{}", get_string_node_kind(node), i, j);
+        let name = format!("{}_{}_{}", node.lower_case_name(), i, j);
         visited.insert(NodeID::new(j), name.clone());
         let visited = match node {
             Node::Start => {
@@ -155,13 +155,13 @@ fn write_node<W: std::fmt::Write>(
                 visited
             }
             Node::Unary { input, op } => {
-                write!(w, "{} [label=\"{}\"];\n", name, get_string_uop_kind(*op))?;
+                write!(w, "{} [label=\"{}\"];\n", name, op.lower_case_name())?;
                 let (input_name, visited) = write_node(i, input.idx(), module, visited, w)?;
                 write!(w, "{} -> {} [label=\"input\"];\n", input_name, name)?;
                 visited
             }
             Node::Binary { left, right, op } => {
-                write!(w, "{} [label=\"{}\"];\n", name, get_string_bop_kind(*op))?;
+                write!(w, "{} [label=\"{}\"];\n", name, op.lower_case_name())?;
                 let (left_name, visited) = write_node(i, left.idx(), module, visited, w)?;
                 let (right_name, visited) = write_node(i, right.idx(), module, visited, w)?;
                 write!(w, "{} -> {} [label=\"left\"];\n", left_name, name)?;
@@ -257,89 +257,13 @@ fn write_node<W: std::fmt::Write>(
                 write!(w, "{} -> {} [label=\"data\"];\n", data_name, name)?;
                 visited
             }
+            Node::ExtractSum { data, variant } => {
+                write!(w, "{} [label=\"extract_sum({})\"];\n", name, variant)?;
+                let (data_name, visited) = write_node(i, data.idx(), module, visited, w)?;
+                write!(w, "{} -> {} [label=\"data\"];\n", data_name, name)?;
+                visited
+            }
         };
         Ok((visited.get(&id).unwrap().clone(), visited))
     }
 }
-
-fn get_string_node_kind(node: &Node) -> &'static str {
-    match node {
-        Node::Start => "start",
-        Node::Region { preds: _ } => "region",
-        Node::If {
-            control: _,
-            cond: _,
-        } => "if",
-        Node::Fork {
-            control: _,
-            factor: _,
-        } => "fork",
-        Node::Join {
-            control: _,
-            data: _,
-        } => "join",
-        Node::Phi {
-            control: _,
-            data: _,
-        } => "phi",
-        Node::Return {
-            control: _,
-            value: _,
-        } => "return",
-        Node::Parameter { index: _ } => "parameter",
-        Node::DynamicConstant { id: _ } => "dynamic_constant",
-        Node::Constant { id: _ } => "constant",
-        Node::Unary { input: _, op } => get_string_uop_kind(*op),
-        Node::Binary {
-            left: _,
-            right: _,
-            op,
-        } => get_string_bop_kind(*op),
-        Node::Call {
-            function: _,
-            dynamic_constants: _,
-            args: _,
-        } => "call",
-        Node::ReadProd { prod: _, index: _ } => "read_prod",
-        Node::WriteProd {
-            prod: _,
-            data: _,
-            index: _,
-        } => "write_prod ",
-        Node::ReadArray { array: _, index: _ } => "read_array",
-        Node::WriteArray {
-            array: _,
-            data: _,
-            index: _,
-        } => "write_array",
-        Node::Match { control: _, sum: _ } => "match",
-        Node::BuildSum {
-            data: _,
-            sum_ty: _,
-            variant: _,
-        } => "build_sum",
-    }
-}
-
-fn get_string_uop_kind(uop: UnaryOperator) -> &'static str {
-    match uop {
-        UnaryOperator::Not => "not",
-        UnaryOperator::Neg => "neg",
-    }
-}
-
-fn get_string_bop_kind(bop: BinaryOperator) -> &'static str {
-    match bop {
-        BinaryOperator::Add => "add",
-        BinaryOperator::Sub => "sub",
-        BinaryOperator::Mul => "mul",
-        BinaryOperator::Div => "div",
-        BinaryOperator::Rem => "rem",
-        BinaryOperator::LT => "lt",
-        BinaryOperator::LTE => "lte",
-        BinaryOperator::GT => "gt",
-        BinaryOperator::GTE => "gte",
-        BinaryOperator::EQ => "eq",
-        BinaryOperator::NE => "ne",
-    }
-}
diff --git a/hercules_ir/src/ir.rs b/hercules_ir/src/ir.rs
index 639437a6763c42bcf5db65ce8f522b75739d027e..d07484a5337c11db35d9db48b27a09470273807e 100644
--- a/hercules_ir/src/ir.rs
+++ b/hercules_ir/src/ir.rs
@@ -47,6 +47,7 @@ pub struct Function {
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Type {
     Control(Box<[DynamicConstantID]>),
+    Boolean,
     Integer8,
     Integer16,
     Integer32,
@@ -62,6 +63,60 @@ pub enum Type {
     Array(TypeID, DynamicConstantID),
 }
 
+impl Type {
+    pub fn is_control(&self) -> bool {
+        if let Type::Control(_) = self {
+            true
+        } else {
+            false
+        }
+    }
+
+    pub fn is_bool(&self) -> bool {
+        self == &Type::Boolean
+    }
+
+    pub fn is_unsigned(&self) -> bool {
+        match self {
+            Type::UnsignedInteger8 => true,
+            Type::UnsignedInteger16 => true,
+            Type::UnsignedInteger32 => true,
+            Type::UnsignedInteger64 => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_fixed(&self) -> bool {
+        match self {
+            Type::Integer8 => true,
+            Type::Integer16 => true,
+            Type::Integer32 => true,
+            Type::Integer64 => true,
+            Type::UnsignedInteger8 => true,
+            Type::UnsignedInteger16 => true,
+            Type::UnsignedInteger32 => true,
+            Type::UnsignedInteger64 => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_float(&self) -> bool {
+        match self {
+            Type::Float32 => true,
+            Type::Float64 => true,
+            _ => false,
+        }
+    }
+
+    pub fn is_arithmetic(&self) -> bool {
+        self.is_fixed() || self.is_float()
+    }
+
+    pub fn is_primitive(&self) -> bool {
+        self.is_bool() || self.is_fixed() || self.is_float()
+    }
+}
+
 /*
  * Constants are pretty standard in Hercules IR. Float constants used the
  * ordered_float crate so that constants can be keys in maps (used for
@@ -72,6 +127,7 @@ pub enum Type {
  */
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub enum Constant {
+    Boolean(bool),
     Integer8(i8),
     Integer16(i16),
     Integer32(i32),
@@ -111,7 +167,7 @@ pub enum DynamicConstant {
  * type instead. For example, the if node produces prod(control(N),
  * control(N)), where the first control token represents the false branch, and
  * the second control token represents the true branch. Another example is the
- * fork node, which produces prod(control(N*k), u64), where the u64 is the
+ * fork node, which produces prod(control(N, K), u64), where the u64 is the
  * thread ID. Functions are devoid of side effects, so call nodes don't take as
  * input or output control tokens. There is also no global memory - use arrays.
  */
@@ -191,12 +247,17 @@ pub enum Node {
         sum_ty: TypeID,
         variant: usize,
     },
+    ExtractSum {
+        data: NodeID,
+        variant: usize,
+    },
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub enum UnaryOperator {
     Not,
     Neg,
+    Bitflip,
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@@ -212,6 +273,213 @@ pub enum BinaryOperator {
     GTE,
     EQ,
     NE,
+    Or,
+    And,
+    Xor,
+    LSh,
+    RSh,
+}
+
+impl Node {
+    pub fn is_return(&self) -> bool {
+        if let Node::Return {
+            control: _,
+            value: _,
+        } = self
+        {
+            true
+        } else {
+            false
+        }
+    }
+
+    pub fn upper_case_name(&self) -> &'static str {
+        match self {
+            Node::Start => "Start",
+            Node::Region { preds: _ } => "Region",
+            Node::If {
+                control: _,
+                cond: _,
+            } => "If",
+            Node::Fork {
+                control: _,
+                factor: _,
+            } => "Fork",
+            Node::Join {
+                control: _,
+                data: _,
+            } => "Join",
+            Node::Phi {
+                control: _,
+                data: _,
+            } => "Phi",
+            Node::Return {
+                control: _,
+                value: _,
+            } => "Return",
+            Node::Parameter { index: _ } => "Parameter",
+            Node::DynamicConstant { id: _ } => "DynamicConstant",
+            Node::Constant { id: _ } => "Constant",
+            Node::Unary { input: _, op } => op.upper_case_name(),
+            Node::Binary {
+                left: _,
+                right: _,
+                op,
+            } => op.upper_case_name(),
+            Node::Call {
+                function: _,
+                dynamic_constants: _,
+                args: _,
+            } => "Unary",
+            Node::ReadProd { prod: _, index: _ } => "ReadProd",
+            Node::WriteProd {
+                prod: _,
+                data: _,
+                index: _,
+            } => "WriteProd",
+            Node::ReadArray { array: _, index: _ } => "ReadArray",
+            Node::WriteArray {
+                array: _,
+                data: _,
+                index: _,
+            } => "WriteArray",
+            Node::Match { control: _, sum: _ } => "Match",
+            Node::BuildSum {
+                data: _,
+                sum_ty: _,
+                variant: _,
+            } => "BuildSum",
+            Node::ExtractSum {
+                data: _,
+                variant: _,
+            } => "ExtractSum",
+        }
+    }
+
+    pub fn lower_case_name(&self) -> &'static str {
+        match self {
+            Node::Start => "start",
+            Node::Region { preds: _ } => "region",
+            Node::If {
+                control: _,
+                cond: _,
+            } => "if",
+            Node::Fork {
+                control: _,
+                factor: _,
+            } => "fork",
+            Node::Join {
+                control: _,
+                data: _,
+            } => "join",
+            Node::Phi {
+                control: _,
+                data: _,
+            } => "phi",
+            Node::Return {
+                control: _,
+                value: _,
+            } => "return",
+            Node::Parameter { index: _ } => "parameter",
+            Node::DynamicConstant { id: _ } => "dynamic_constant",
+            Node::Constant { id: _ } => "constant",
+            Node::Unary { input: _, op } => op.lower_case_name(),
+            Node::Binary {
+                left: _,
+                right: _,
+                op,
+            } => op.lower_case_name(),
+            Node::Call {
+                function: _,
+                dynamic_constants: _,
+                args: _,
+            } => "call",
+            Node::ReadProd { prod: _, index: _ } => "read_prod",
+            Node::WriteProd {
+                prod: _,
+                data: _,
+                index: _,
+            } => "write_prod ",
+            Node::ReadArray { array: _, index: _ } => "read_array",
+            Node::WriteArray {
+                array: _,
+                data: _,
+                index: _,
+            } => "write_array",
+            Node::Match { control: _, sum: _ } => "match",
+            Node::BuildSum {
+                data: _,
+                sum_ty: _,
+                variant: _,
+            } => "build_sum",
+            Node::ExtractSum {
+                data: _,
+                variant: _,
+            } => "extract_sum",
+        }
+    }
+}
+
+impl UnaryOperator {
+    pub fn upper_case_name(&self) -> &'static str {
+        match self {
+            UnaryOperator::Not => "Not",
+            UnaryOperator::Neg => "Neg",
+            UnaryOperator::Bitflip => "Bitflip",
+        }
+    }
+
+    pub fn lower_case_name(&self) -> &'static str {
+        match self {
+            UnaryOperator::Not => "not",
+            UnaryOperator::Neg => "neg",
+            UnaryOperator::Bitflip => "bitflip",
+        }
+    }
+}
+
+impl BinaryOperator {
+    pub fn upper_case_name(&self) -> &'static str {
+        match self {
+            BinaryOperator::Add => "Add",
+            BinaryOperator::Sub => "Sub",
+            BinaryOperator::Mul => "Mul",
+            BinaryOperator::Div => "Div",
+            BinaryOperator::Rem => "Rem",
+            BinaryOperator::LT => "LT",
+            BinaryOperator::LTE => "LTE",
+            BinaryOperator::GT => "GT",
+            BinaryOperator::GTE => "GTE",
+            BinaryOperator::EQ => "EQ",
+            BinaryOperator::NE => "NE",
+            BinaryOperator::Or => "Or",
+            BinaryOperator::And => "And",
+            BinaryOperator::Xor => "Xor",
+            BinaryOperator::LSh => "LSh",
+            BinaryOperator::RSh => "RSh",
+        }
+    }
+
+    pub fn lower_case_name(&self) -> &'static str {
+        match self {
+            BinaryOperator::Add => "add",
+            BinaryOperator::Sub => "sub",
+            BinaryOperator::Mul => "mul",
+            BinaryOperator::Div => "div",
+            BinaryOperator::Rem => "rem",
+            BinaryOperator::LT => "lt",
+            BinaryOperator::LTE => "lte",
+            BinaryOperator::GT => "gt",
+            BinaryOperator::GTE => "gte",
+            BinaryOperator::EQ => "eq",
+            BinaryOperator::NE => "ne",
+            BinaryOperator::Or => "or",
+            BinaryOperator::And => "and",
+            BinaryOperator::Xor => "xor",
+            BinaryOperator::LSh => "lsh",
+            BinaryOperator::RSh => "rsh",
+        }
+    }
 }
 
 /*
diff --git a/hercules_ir/src/lib.rs b/hercules_ir/src/lib.rs
index 2974253714fce85ded0ec37c1b86b6357e12a4a7..cd66d5fb5ea57a37aa6b85f09f5b1683f02146f0 100644
--- a/hercules_ir/src/lib.rs
+++ b/hercules_ir/src/lib.rs
@@ -1,7 +1,15 @@
+pub mod dataflow;
+pub mod def_use;
 pub mod dot;
 pub mod ir;
 pub mod parse;
+pub mod typecheck;
+pub mod verify;
 
+pub use crate::dataflow::*;
+pub use crate::def_use::*;
 pub use crate::dot::*;
 pub use crate::ir::*;
 pub use crate::parse::*;
+pub use crate::typecheck::*;
+pub use crate::verify::*;
diff --git a/hercules_ir/src/parse.rs b/hercules_ir/src/parse.rs
index 50613f5c82190aa61b0617ef82775fba52c0a22d..a54f81096e42e98618342f10dde30f20b7ee85f9 100644
--- a/hercules_ir/src/parse.rs
+++ b/hercules_ir/src/parse.rs
@@ -9,8 +9,10 @@ use crate::*;
 /*
  * Top level parse function.
  */
-pub fn parse(ir_test: &str) -> Module {
-    parse_module(ir_test, Context::default()).unwrap().1
+pub fn parse(ir_test: &str) -> Result<Module, ()> {
+    parse_module(ir_test, Context::default())
+        .map(|x| x.1)
+        .map_err(|_| ())
 }
 
 /*
@@ -280,6 +282,7 @@ fn parse_node<'a>(
         // parse them into Unary or Binary node kinds.
         "not" => parse_unary(ir_text, context, UnaryOperator::Not)?,
         "neg" => parse_unary(ir_text, context, UnaryOperator::Neg)?,
+        "bitflip" => parse_unary(ir_text, context, UnaryOperator::Bitflip)?,
         "add" => parse_binary(ir_text, context, BinaryOperator::Add)?,
         "sub" => parse_binary(ir_text, context, BinaryOperator::Sub)?,
         "mul" => parse_binary(ir_text, context, BinaryOperator::Mul)?,
@@ -291,6 +294,11 @@ fn parse_node<'a>(
         "gte" => parse_binary(ir_text, context, BinaryOperator::GTE)?,
         "eq" => parse_binary(ir_text, context, BinaryOperator::EQ)?,
         "ne" => parse_binary(ir_text, context, BinaryOperator::NE)?,
+        "or" => parse_binary(ir_text, context, BinaryOperator::Or)?,
+        "and" => parse_binary(ir_text, context, BinaryOperator::And)?,
+        "xor" => parse_binary(ir_text, context, BinaryOperator::Xor)?,
+        "lsh" => parse_binary(ir_text, context, BinaryOperator::LSh)?,
+        "rsh" => parse_binary(ir_text, context, BinaryOperator::RSh)?,
         "call" => parse_call(ir_text, context)?,
         "read_prod" => parse_read_prod(ir_text, context)?,
         "write_prod" => parse_write_prod(ir_text, context)?,
@@ -298,6 +306,7 @@ fn parse_node<'a>(
         "write_array" => parse_write_array(ir_text, context)?,
         "match" => parse_match(ir_text, context)?,
         "build_sum" => parse_build_sum(ir_text, context)?,
+        "extract_sum" => parse_extract_sum(ir_text, context)?,
         _ => Err(nom::Err::Error(nom::error::Error {
             input: ir_text,
             code: nom::error::ErrorKind::IsNot,
@@ -581,6 +590,16 @@ fn parse_build_sum<'a>(
     ))
 }
 
+fn parse_extract_sum<'a>(
+    ir_text: &'a str,
+    context: &RefCell<Context<'a>>,
+) -> nom::IResult<&'a str, Node> {
+    let (ir_text, (data, variant)) =
+        parse_tuple2(parse_identifier, |x| parse_prim::<usize>(x, "1234567890"))(ir_text)?;
+    let data = context.borrow_mut().get_node_id(data);
+    Ok((ir_text, Node::ExtractSum { data, variant }))
+}
+
 fn parse_type<'a>(ir_text: &'a str, context: &RefCell<Context<'a>>) -> nom::IResult<&'a str, Type> {
     // Parser combinators are very convenient, if a bit hard to read.
     let ir_text = nom::character::complete::multispace0(ir_text)?.0;
@@ -611,6 +630,7 @@ fn parse_type<'a>(ir_text: &'a str, context: &RefCell<Context<'a>>) -> nom::IRes
             Type::Control(Box::new([]))
         }),
         // Primitive types are written in Rust style.
+        nom::combinator::map(nom::bytes::complete::tag("bool"), |_| Type::Boolean),
         nom::combinator::map(nom::bytes::complete::tag("i8"), |_| Type::Integer8),
         nom::combinator::map(nom::bytes::complete::tag("i16"), |_| Type::Integer16),
         nom::combinator::map(nom::bytes::complete::tag("i32"), |_| Type::Integer32),
@@ -750,6 +770,7 @@ fn parse_constant<'a>(
             input: ir_text,
             code: nom::error::ErrorKind::IsNot,
         }))?,
+        Type::Boolean => parse_boolean(ir_text)?,
         Type::Integer8 => parse_integer8(ir_text)?,
         Type::Integer16 => parse_integer16(ir_text)?,
         Type::Integer32 => parse_integer32(ir_text)?,
@@ -797,6 +818,14 @@ fn parse_prim<'a, T: FromStr>(ir_text: &'a str, chars: &'static str) -> nom::IRe
     Ok((ir_text, x))
 }
 
+fn parse_boolean<'a>(ir_text: &'a str) -> nom::IResult<&'a str, Constant> {
+    let (ir_text, val) = nom::branch::alt((
+        nom::combinator::map(nom::bytes::complete::tag("false"), |_| false),
+        nom::combinator::map(nom::bytes::complete::tag("true"), |_| true),
+    ))(ir_text)?;
+    Ok((ir_text, Constant::Boolean(val)))
+}
+
 fn parse_integer8<'a>(ir_text: &'a str) -> nom::IResult<&'a str, Constant> {
     let (ir_text, num) = parse_prim(ir_text, "-1234567890")?;
     Ok((ir_text, Constant::Integer8(num)))
@@ -1060,6 +1089,7 @@ fn add<1>(x: i32, y: i32) -> i32
   w = add(z, c)
   z = add(x, y)
 ",
-        );
+        )
+        .unwrap();
     }
 }
diff --git a/hercules_ir/src/typecheck.rs b/hercules_ir/src/typecheck.rs
new file mode 100644
index 0000000000000000000000000000000000000000..4bfa9faecb57ce29137b0d892765e837b1bc4f9d
--- /dev/null
+++ b/hercules_ir/src/typecheck.rs
@@ -0,0 +1,879 @@
+use std::collections::HashMap;
+use std::iter::zip;
+
+use crate::*;
+
+use self::TypeSemilattice::*;
+
+/*
+ * Enum for type semilattice.
+ */
+#[derive(Eq, Clone)]
+enum TypeSemilattice {
+    Unconstrained,
+    Concrete(TypeID),
+    Error(String),
+}
+
+impl TypeSemilattice {
+    fn is_error(&self) -> bool {
+        if let Error(_) = self {
+            true
+        } else {
+            false
+        }
+    }
+}
+
+impl PartialEq for TypeSemilattice {
+    fn eq(&self, other: &Self) -> bool {
+        match (self, other) {
+            (Unconstrained, Unconstrained) => true,
+            (Concrete(id1), Concrete(id2)) => id1 == id2,
+            (Error(_), Error(_)) => true,
+            _ => false,
+        }
+    }
+}
+
+impl Semilattice for TypeSemilattice {
+    fn meet(a: &Self, b: &Self) -> Self {
+        match (a, b) {
+            (Unconstrained, Unconstrained) => Unconstrained,
+            (Unconstrained, b) => b.clone(),
+            (a, Unconstrained) => a.clone(),
+            (Concrete(id1), Concrete(id2)) => {
+                if id1 == id2 {
+                    Concrete(*id1)
+                } else {
+                    // Error will only allocate when a type error has occurred.
+                    // In that case, we're less concerned about speed to the
+                    // compiler, and more allocations are acceptable.
+                    Error(format!(
+                        "Couldn't reconcile two different concrete types, with IDs {} and {}.",
+                        id1.idx(),
+                        id2.idx()
+                    ))
+                }
+            }
+            (Error(msg), _) => Error(msg.clone()),
+            (_, Error(msg)) => Error(msg.clone()),
+        }
+    }
+
+    fn bottom() -> Self {
+        // Strings don't allocate unless they actually contain characters, so
+        // this is cheap.
+        Error(String::new())
+    }
+
+    fn top() -> Self {
+        Unconstrained
+    }
+}
+
+pub type ModuleTyping = Vec<Vec<TypeID>>;
+
+/*
+ * Top level typecheck function. Typechecking is a module-wide analysis.
+ * Returns a type for every node in every function.
+ */
+pub fn typecheck(
+    module: &mut Module,
+    reverse_postorders: &Vec<Vec<NodeID>>,
+) -> Result<ModuleTyping, String> {
+    // Step 1: assemble a reverse type map. This is needed to get or create the
+    // ID of potentially new types. Break down module into references to
+    // individual elements at this point, so that borrows don't overlap each
+    // other.
+    let Module {
+        ref functions,
+        ref mut types,
+        ref constants,
+        ref dynamic_constants,
+    } = module;
+    let mut reverse_type_map: HashMap<Type, TypeID> = types
+        .iter()
+        .enumerate()
+        .map(|(idx, ty)| (ty.clone(), TypeID::new(idx)))
+        .collect();
+
+    // Step 2: run dataflow. This is an occurrence of dataflow where the flow
+    // function performs a non-associative operation on the predecessor "out"
+    // values.
+    let results: Vec<Vec<TypeSemilattice>> = zip(functions, reverse_postorders)
+        .map(|(function, reverse_postorder)| {
+            forward_dataflow(function, reverse_postorder, |inputs, id| {
+                typeflow(
+                    inputs,
+                    id,
+                    function,
+                    functions,
+                    types,
+                    constants,
+                    dynamic_constants,
+                    &mut reverse_type_map,
+                )
+            })
+        })
+        .collect();
+
+    // Step 3: convert the individual type lattice values into lists of
+    // concrete type values, or a single error.
+    results
+        .into_iter()
+        // For each type list, we want to convert its element TypeSemilattices
+        // into Result<TypeID, String>.
+        .map(|result| {
+            result
+                .into_iter()
+                // For each TypeSemilattice, convert into Result<TypeID, String>.
+                .map(|x| match x {
+                    Unconstrained => Err(String::from("Found unconstrained type in program.")),
+                    Concrete(id) => Ok(id),
+                    Error(msg) => Err(msg.clone()),
+                })
+                .collect()
+        })
+        .collect()
+}
+
+/*
+ * Flow function for typechecking.
+ */
+fn typeflow(
+    inputs: &[&TypeSemilattice],
+    node: &Node,
+    function: &Function,
+    functions: &Vec<Function>,
+    types: &mut Vec<Type>,
+    constants: &Vec<Constant>,
+    dynamic_constants: &Vec<DynamicConstant>,
+    reverse_type_map: &mut HashMap<Type, TypeID>,
+) -> TypeSemilattice {
+    // Whenever we want to reference a specific type (for example, for the
+    // start node), we need to get its type ID. This helper function gets the
+    // ID if it already exists. If the type doesn't already exist, the helper
+    // adds it to the type intern list.
+    let get_type_id =
+        |ty: Type, types: &mut Vec<Type>, reverse_type_map: &mut HashMap<Type, TypeID>| -> TypeID {
+            if let Some(id) = reverse_type_map.get(&ty) {
+                *id
+            } else {
+                let id = TypeID::new(reverse_type_map.len());
+                reverse_type_map.insert(ty.clone(), id);
+                types.push(ty);
+                id
+            }
+        };
+
+    // Each node requires different type logic. This unfortunately results in a
+    // large match statement. Oh well. Each arm returns the lattice value for
+    // the "out" type of the node.
+    match node {
+        Node::Start => {
+            if inputs.len() != 0 {
+                return Error(String::from("Start node must have zero inputs."));
+            }
+
+            // The start node is the producer of the control token.
+            Concrete(get_type_id(
+                Type::Control(Box::new([])),
+                types,
+                reverse_type_map,
+            ))
+        }
+        Node::Region { preds: _ } => {
+            if inputs.len() == 0 {
+                return Error(String::from("Region node must have at least one input."));
+            }
+
+            let mut meet = inputs[0].clone();
+            for l in inputs[1..].iter() {
+                meet = TypeSemilattice::meet(&meet, l);
+            }
+
+            // Only special case is if concrete type is non-control. In
+            // this case, we override that concrete type with an error,
+            // since the input types must all be control types. Any other
+            // lattice value can be returned as-is.
+            if let Concrete(id) = meet {
+                if !types[id.idx()].is_control() {
+                    return Error(String::from(
+                        "Region node's input type cannot be non-control.",
+                    ));
+                }
+            }
+
+            meet
+        }
+        Node::If {
+            control: _,
+            cond: _,
+        } => {
+            if inputs.len() != 2 {
+                return Error(String::from("If node must have exactly two inputs."));
+            }
+
+            // Check type of data input first, since we may return while
+            // checking control input.
+            if let Concrete(id) = inputs[1] {
+                if !types[id.idx()].is_bool() {
+                    return Error(String::from(
+                        "If node's condition input cannot have non-boolean type.",
+                    ));
+                }
+            } else if inputs[1].is_error() {
+                // If an input has an error lattice value, it must be
+                // propagated.
+                return inputs[1].clone();
+            }
+
+            if let Concrete(id) = inputs[0] {
+                if !types[id.idx()].is_control() {
+                    return Error(String::from(
+                        "If node's control input cannot have non-control type.",
+                    ));
+                } else {
+                    let out_ty = Type::Product(Box::new([*id, *id]));
+                    return Concrete(get_type_id(out_ty, types, reverse_type_map));
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::Fork { control: _, factor } => {
+            if inputs.len() != 1 {
+                return Error(String::from("Fork node must have exactly one input."));
+            }
+
+            if let Concrete(id) = inputs[0] {
+                if let Type::Control(factors) = &types[id.idx()] {
+                    // Fork adds a new factor to the thread spawn factor list.
+                    let mut new_factors = factors.clone().into_vec();
+                    new_factors.push(*factor);
+
+                    // Out type is a pair - first element is the control type,
+                    // second is the index type (u64). Each thread gets a
+                    // different thread ID at runtime.
+                    let control_out_id = get_type_id(
+                        Type::Control(new_factors.into_boxed_slice()),
+                        types,
+                        reverse_type_map,
+                    );
+                    let index_out_id =
+                        get_type_id(Type::UnsignedInteger64, types, reverse_type_map);
+                    let out_ty = Type::Product(Box::new([control_out_id, index_out_id]));
+                    return Concrete(get_type_id(out_ty, types, reverse_type_map));
+                } else {
+                    return Error(String::from(
+                        "Fork node's input cannot have non-control type.",
+                    ));
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::Join {
+            control: _,
+            data: _,
+        } => {
+            if inputs.len() != 2 {
+                return Error(String::from("Join node must have exactly two inputs."));
+            }
+
+            // If the data input isn't concrete, we can't assemble a concrete
+            // output type yet, so just return data input's type (either
+            // unconstrained or error) instead.
+            if let Concrete(data_id) = inputs[1] {
+                if types[data_id.idx()].is_control() {
+                    return Error(String::from(
+                        "Join node's second input must not have a control type.",
+                    ));
+                }
+
+                // Similarly, if the control input isn't concrete yet, we can't
+                // assemble a concrete output type, so just return the control
+                // input non-concrete type.
+                if let Concrete(control_id) = inputs[0] {
+                    if let Type::Control(factors) = &types[control_id.idx()] {
+                        // Join removes a factor from the factor list.
+                        if factors.len() == 0 {
+                            return Error(String::from("Join node's first input must have a control type with at least one thread replication factor."));
+                        }
+                        let mut new_factors = factors.clone().into_vec();
+                        let dc_id = new_factors.pop().unwrap();
+
+                        // Out type is a pair - first element is the control
+                        // type, second is the result array from the parallel
+                        // computation.
+                        let control_out_id = get_type_id(
+                            Type::Control(new_factors.into_boxed_slice()),
+                            types,
+                            reverse_type_map,
+                        );
+                        let array_out_id =
+                            get_type_id(Type::Array(*data_id, dc_id), types, reverse_type_map);
+                        let out_ty = Type::Product(Box::new([control_out_id, array_out_id]));
+                        return Concrete(get_type_id(out_ty, types, reverse_type_map));
+                    } else {
+                        return Error(String::from(
+                            "Join node's first input cannot have non-control type.",
+                        ));
+                    }
+                } else {
+                    return inputs[0].clone();
+                }
+            }
+
+            inputs[1].clone()
+        }
+        Node::Phi {
+            control: _,
+            data: _,
+        } => {
+            if inputs.len() < 2 {
+                return Error(String::from("Phi node must have at least two inputs."));
+            }
+
+            // Check type of control input first, since this may produce an
+            // error.
+            if let Concrete(id) = inputs[inputs.len() - 1] {
+                if !types[id.idx()].is_control() {
+                    return Error(String::from(
+                        "Phi node's control input cannot have non-control type.",
+                    ));
+                }
+            } else if inputs[inputs.len() - 1].is_error() {
+                // If an input has an error lattice value, it must be
+                // propagated.
+                return inputs[inputs.len() - 1].clone();
+            }
+
+            // Output type of phi node is same type as every data input.
+            let mut meet = inputs[0].clone();
+            for l in inputs[1..inputs.len() - 1].iter() {
+                if let Concrete(id) = l {
+                    if types[id.idx()].is_control() {
+                        return Error(String::from(
+                            "Phi node's data inputs cannot have control type.",
+                        ));
+                    }
+                }
+                meet = TypeSemilattice::meet(&meet, l);
+            }
+
+            meet
+        }
+        Node::Return {
+            control: _,
+            value: _,
+        } => {
+            if inputs.len() != 2 {
+                return Error(String::from("Return node must have exactly two inputs."));
+            }
+
+            // Check type of control input first, since this may produce an
+            // error.
+            if let Concrete(id) = inputs[0] {
+                if let Type::Control(factors) = &types[id.idx()] {
+                    if factors.len() != 0 {
+                        return Error(String::from(
+                            "Return node's control input must have no thread replications.",
+                        ));
+                    }
+                } else {
+                    return Error(String::from(
+                        "Return node's control input cannot have non-control type.",
+                    ));
+                }
+            } else if inputs[0].is_error() {
+                // If an input has an error lattice value, it must be
+                // propagated.
+                return inputs[0].clone();
+            }
+
+            if let Concrete(id) = inputs[1] {
+                if *id != function.return_type {
+                    return Error(String::from("Return node's data input type must be the same as the function's return type."));
+                }
+            } else if inputs[1].is_error() {
+                return inputs[1].clone();
+            }
+
+            Concrete(get_type_id(
+                Type::Product(Box::new([])),
+                types,
+                reverse_type_map,
+            ))
+        }
+        Node::Parameter { index } => {
+            if inputs.len() != 0 {
+                return Error(String::from("Parameter node must have zero inputs."));
+            }
+
+            if *index >= function.param_types.len() {
+                return Error(String::from("Parameter node must reference an index corresponding to an existing function argument."));
+            }
+
+            // Type of parameter is stored directly in function.
+            let param_id = function.param_types[*index];
+
+            Concrete(param_id)
+        }
+        Node::Constant { id } => {
+            if inputs.len() != 0 {
+                return Error(String::from("Constant node must have zero inputs."));
+            }
+
+            // Most constants' type are obvious.
+            match constants[id.idx()] {
+                Constant::Boolean(_) => {
+                    Concrete(get_type_id(Type::Boolean, types, reverse_type_map))
+                }
+                Constant::Integer8(_) => {
+                    Concrete(get_type_id(Type::Integer8, types, reverse_type_map))
+                }
+                Constant::Integer16(_) => {
+                    Concrete(get_type_id(Type::Integer16, types, reverse_type_map))
+                }
+                Constant::Integer32(_) => {
+                    Concrete(get_type_id(Type::Integer32, types, reverse_type_map))
+                }
+                Constant::Integer64(_) => {
+                    Concrete(get_type_id(Type::Integer64, types, reverse_type_map))
+                }
+                Constant::UnsignedInteger8(_) => {
+                    Concrete(get_type_id(Type::UnsignedInteger8, types, reverse_type_map))
+                }
+                Constant::UnsignedInteger16(_) => Concrete(get_type_id(
+                    Type::UnsignedInteger16,
+                    types,
+                    reverse_type_map,
+                )),
+                Constant::UnsignedInteger32(_) => Concrete(get_type_id(
+                    Type::UnsignedInteger32,
+                    types,
+                    reverse_type_map,
+                )),
+                Constant::UnsignedInteger64(_) => Concrete(get_type_id(
+                    Type::UnsignedInteger64,
+                    types,
+                    reverse_type_map,
+                )),
+                Constant::Float32(_) => {
+                    Concrete(get_type_id(Type::Float32, types, reverse_type_map))
+                }
+                Constant::Float64(_) => {
+                    Concrete(get_type_id(Type::Float64, types, reverse_type_map))
+                }
+                // Product, summation, and array constants are exceptions.
+                // Technically, only summation constants need to explicitly
+                // store their type, but product and array constants also
+                // explicitly store their type specifically to make this code
+                // simpler (although their type could be derived from the
+                // constant itself).
+                Constant::Product(id, _) => {
+                    if let Type::Product(_) = types[id.idx()] {
+                        Concrete(id)
+                    } else {
+                        Error(String::from(
+                            "Product constant must store an explicit product type.",
+                        ))
+                    }
+                }
+                Constant::Summation(id, _, _) => {
+                    if let Type::Summation(_) = types[id.idx()] {
+                        Concrete(id)
+                    } else {
+                        Error(String::from(
+                            "Summation constant must store an explicit summation type.",
+                        ))
+                    }
+                }
+                // Array typechecking also consists of validating the number of constant elements.
+                Constant::Array(id, ref elems) => {
+                    if let Type::Array(_, dc_id) = types[id.idx()] {
+                        if dynamic_constants[dc_id.idx()] == DynamicConstant::Constant(elems.len())
+                        {
+                            Concrete(id)
+                        } else {
+                            Error(String::from("Array constant must have the correct number of constant elements as specified by its type."))
+                        }
+                    } else {
+                        Error(String::from(
+                            "Array constant must store an explicit array type.",
+                        ))
+                    }
+                }
+            }
+        }
+        Node::DynamicConstant { id: _ } => {
+            if inputs.len() != 0 {
+                return Error(String::from("DynamicConstant node must have zero inputs."));
+            }
+
+            // Dynamic constants are always u64.
+            Concrete(get_type_id(
+                Type::UnsignedInteger64,
+                types,
+                reverse_type_map,
+            ))
+        }
+        Node::Unary { input: _, op } => {
+            if inputs.len() != 1 {
+                return Error(String::from("Unary node must have exactly one input."));
+            }
+
+            if let Concrete(id) = inputs[0] {
+                match op {
+                    UnaryOperator::Not => {
+                        if !types[id.idx()].is_bool() {
+                            return Error(String::from(
+                                "Not unary node input cannot have non-boolean type.",
+                            ));
+                        }
+                    }
+                    UnaryOperator::Neg => {
+                        if !types[id.idx()].is_arithmetic() {
+                            return Error(String::from(
+                                "Neg unary node input cannot have non-arithmetic type.",
+                            ));
+                        }
+                    }
+                    UnaryOperator::Bitflip => {
+                        if !types[id.idx()].is_fixed() {
+                            return Error(String::from(
+                                "Bitflip unary node input cannot have non-fixed type.",
+                            ));
+                        }
+                    }
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::Binary {
+            left: _,
+            right: _,
+            op,
+        } => {
+            if inputs.len() != 2 {
+                return Error(String::from("Binary node must have exactly two inputs."));
+            }
+
+            let input_ty = TypeSemilattice::meet(inputs[0], inputs[1]);
+
+            if let Concrete(id) = input_ty {
+                match op {
+                    BinaryOperator::Add
+                    | BinaryOperator::Sub
+                    | BinaryOperator::Mul
+                    | BinaryOperator::Div
+                    | BinaryOperator::Rem => {
+                        if !types[id.idx()].is_arithmetic() {
+                            return Error(format!(
+                                "{:?} binary node input cannot have non-arithmetic type.",
+                                op,
+                            ));
+                        }
+                    }
+                    BinaryOperator::LT
+                    | BinaryOperator::LTE
+                    | BinaryOperator::GT
+                    | BinaryOperator::GTE => {
+                        if !types[id.idx()].is_arithmetic() {
+                            return Error(format!(
+                                "{:?} binary node input cannot have non-arithmetic type.",
+                                op,
+                            ));
+                        }
+
+                        // Comparison operators change the input type.
+                        return Concrete(get_type_id(Type::Boolean, types, reverse_type_map));
+                    }
+                    BinaryOperator::EQ | BinaryOperator::NE => {
+                        if types[id.idx()].is_control() {
+                            return Error(format!(
+                                "{:?} binary node input cannot have control type.",
+                                op,
+                            ));
+                        }
+
+                        // Equality operators potentially change the input type.
+                        return Concrete(get_type_id(Type::Boolean, types, reverse_type_map));
+                    }
+                    BinaryOperator::Or
+                    | BinaryOperator::And
+                    | BinaryOperator::Xor
+                    | BinaryOperator::LSh
+                    | BinaryOperator::RSh => {
+                        if !types[id.idx()].is_fixed() {
+                            return Error(format!(
+                                "{:?} binary node input cannot have non-fixed type.",
+                                op,
+                            ));
+                        }
+                    }
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::Call {
+            function: callee_id,
+            dynamic_constants: dc_args,
+            args: _,
+        } => {
+            let callee = &functions[callee_id.idx()];
+
+            // Check number of run-time arguments.
+            if inputs.len() != callee.param_types.len() {
+                return Error(format!(
+                    "Call node has {} inputs, but calls a function with {} parameters.",
+                    inputs.len(),
+                    callee.param_types.len(),
+                ));
+            }
+
+            // Check number of dynamic constant arguments.
+            if dc_args.len() != callee.num_dynamic_constants as usize {
+                return Error(format!(
+                    "Call node references {} dynamic constants, but calls a function expecting {} dynamic constants.",
+                    dc_args.len(),
+                    callee.num_dynamic_constants
+                ));
+            }
+
+            // Check argument types.
+            for (input, param_ty) in zip(inputs.iter(), callee.param_types.iter()) {
+                if let Concrete(input_id) = input {
+                    if input_id != param_ty {
+                        return Error(String::from(
+                            "Call node mismatches argument types with callee function.",
+                        ));
+                    }
+                } else if input.is_error() {
+                    // If an input type is an error, we must propagate it.
+                    return (*input).clone();
+                }
+            }
+
+            Concrete(callee.return_type)
+        }
+        Node::ReadProd { prod: _, index } => {
+            if inputs.len() != 1 {
+                return Error(String::from("ReadProd node must have exactly one input."));
+            }
+
+            // If the input type isn't concrete, just propagate input type.
+            if let Concrete(id) = inputs[0] {
+                if let Type::Product(elem_tys) = &types[id.idx()] {
+                    if *index >= elem_tys.len() {
+                        // ReadProd's index being out of range is a type error.
+                        return Error(String::from("ReadProd node's index must be within range of input product type's element list."));
+                    } else {
+                        return Concrete(elem_tys[*index]);
+                    }
+                } else {
+                    return Error(String::from(
+                        "ReadProd node's input type must be a product type.",
+                    ));
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::WriteProd {
+            prod: _,
+            data: _,
+            index,
+        } => {
+            if inputs.len() != 2 {
+                return Error(String::from("WriteProd node must have exactly two inputs."));
+            }
+
+            // If the input type isn't concrete, just propagate input type.
+            if let Concrete(id) = inputs[0] {
+                if let Type::Product(elem_tys) = &types[id.idx()] {
+                    if *index >= elem_tys.len() {
+                        // ReadProd's index being out of range is a type error.
+                        return Error(String::from("WriteProd node's index must be within range of input product type's element list."));
+                    } else if let Concrete(data_id) = inputs[1] {
+                        if elem_tys[*index] != *data_id {
+                            return Error(format!("WriteProd node's data input doesn't match the type of the element at index {} inside the product type.", index));
+                        }
+                    } else if inputs[1].is_error() {
+                        // If an input lattice value is an error, we must
+                        // propagate it.
+                        return inputs[1].clone();
+                    }
+                    return Concrete(elem_tys[*index]);
+                } else {
+                    return Error(String::from(
+                        "WriteProd node's input type must be a product type.",
+                    ));
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::ReadArray { array: _, index: _ } => {
+            if inputs.len() != 2 {
+                return Error(String::from("ReadArray node must have exactly two inputs."));
+            }
+
+            // Check that index has unsigned type.
+            if let Concrete(id) = inputs[1] {
+                if !types[id.idx()].is_unsigned() {
+                    return Error(String::from(
+                        "ReadArray node's index input must have unsigned type.",
+                    ));
+                }
+            } else if inputs[1].is_error() {
+                return inputs[1].clone();
+            }
+
+            // If array input is concrete, we can get type of ReadArray node.
+            if let Concrete(id) = inputs[0] {
+                if let Type::Array(elem_id, _) = types[id.idx()] {
+                    return Concrete(elem_id);
+                } else {
+                    return Error(String::from(
+                        "ReadArray node's array input must have array type.",
+                    ));
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::WriteArray {
+            array: _,
+            data: _,
+            index: _,
+        } => {
+            if inputs.len() != 3 {
+                return Error(String::from("WriteArray node must have exactly 3 inputs."));
+            }
+
+            // Check that index has unsigned type.
+            if let Concrete(id) = inputs[2] {
+                if !types[id.idx()].is_unsigned() {
+                    return Error(String::from(
+                        "WriteArray node's index input must have unsigned type.",
+                    ));
+                }
+            } else if inputs[2].is_error() {
+                return inputs[2].clone();
+            }
+
+            // Check that array and data types match.
+            if let Concrete(array_id) = inputs[0] {
+                if let Type::Array(elem_id, _) = types[array_id.idx()] {
+                    if let Concrete(data_id) = inputs[1] {
+                        if elem_id != *data_id {
+                            return Error(String::from("WriteArray node's array and data inputs must have compatible types (type of data input must be the same as the array input's element type)."));
+                        }
+                    }
+                } else {
+                    return Error(String::from(
+                        "WriteArray node's array input must have array type.",
+                    ));
+                }
+            }
+
+            // If an input type is an error, we must propagate it.
+            if inputs[1].is_error() {
+                return inputs[1].clone();
+            }
+
+            inputs[0].clone()
+        }
+        Node::Match { control: _, sum: _ } => {
+            if inputs.len() != 2 {
+                return Error(String::from("Match node must have exactly two inputs."));
+            }
+
+            // Check sum and control inputs simultaneously, since both need to
+            // be concrete to determine a concrete type for a match node.
+            if let (Concrete(control_id), Concrete(sum_id)) = (inputs[0], inputs[1]) {
+                if let Type::Summation(variants) = &types[sum_id.idx()] {
+                    if !types[control_id.idx()].is_control() {
+                        return Error(String::from(
+                            "Match node's control input cannot have non-control type.",
+                        ));
+                    } else {
+                        let out_ty =
+                            Type::Product(vec![*control_id; variants.len()].into_boxed_slice());
+                        return Concrete(get_type_id(out_ty, types, reverse_type_map));
+                    }
+                } else {
+                    return Error(String::from(
+                        "Match node's condition input cannot have non-sum type.",
+                    ));
+                }
+            }
+
+            // Otherwise, currently unconstrained, or an error.
+            match TypeSemilattice::meet(inputs[0], inputs[1]) {
+                TypeSemilattice::Unconstrained => TypeSemilattice::Unconstrained,
+                TypeSemilattice::Concrete(_) => TypeSemilattice::Unconstrained,
+                TypeSemilattice::Error(msg) => TypeSemilattice::Error(msg),
+            }
+        }
+        Node::BuildSum {
+            data: _,
+            sum_ty,
+            variant,
+        } => {
+            if inputs.len() != 1 {
+                return Error(String::from("BuildSum node must have exactly one input."));
+            }
+
+            if let Concrete(id) = inputs[0] {
+                // BuildSum node stores its own result type.
+                if let Type::Summation(variants) = &types[sum_ty.idx()] {
+                    // Must reference an existing variant.
+                    if *variant >= variants.len() {
+                        return Error(String::from("BuildSum node's variant number must be in range of valid variant numbers for referenced sum type."));
+                    }
+
+                    // The variant type has to be the same as the type of data.
+                    if *id == variants[*variant] {
+                        return Error(String::from(
+                            "BuildSum node's input type must match the referenced variant type.",
+                        ));
+                    }
+
+                    return Concrete(*sum_ty);
+                } else {
+                    return Error(String::from("BuildSum node must reference a sum type."));
+                }
+            }
+
+            inputs[0].clone()
+        }
+        Node::ExtractSum { data: _, variant } => {
+            if inputs.len() != 1 {
+                return Error(String::from("ExtractSum node must have exactly one input."));
+            }
+
+            if let Concrete(id) = inputs[0] {
+                if let Type::Summation(variants) = &types[id.idx()] {
+                    // Must reference an existing variant.
+                    if *variant >= variants.len() {
+                        return Error(String::from("BuildSum node's variant number must be in range of valid variant numbers for referenced sum type."));
+                    }
+
+                    return Concrete(variants[*variant]);
+                } else {
+                    return Error(String::from(
+                        "ExtractSum node's input cannot have non-sum type.",
+                    ));
+                }
+            }
+
+            inputs[0].clone()
+        }
+    }
+}
diff --git a/hercules_ir/src/verify.rs b/hercules_ir/src/verify.rs
new file mode 100644
index 0000000000000000000000000000000000000000..a737aafef6dc776be2b13e8f824455a8f9fd2e68
--- /dev/null
+++ b/hercules_ir/src/verify.rs
@@ -0,0 +1,146 @@
+extern crate bitvec;
+
+use std::iter::zip;
+
+use verify::bitvec::prelude::*;
+
+use crate::*;
+
+/*
+ * Top level IR verification function. Verification runs passes that produce
+ * useful results (typing, dominator trees, etc.), so if verification succeeds,
+ * return those useful results. Otherwise, return the first error string found.
+ */
+pub fn verify(module: &mut Module) -> Result<ModuleTyping, String> {
+    let def_uses: Vec<_> = module
+        .functions
+        .iter()
+        .map(|function| def_use(function))
+        .collect();
+    let reverse_postorders: Vec<_> = def_uses
+        .iter()
+        .map(|def_use| reverse_postorder(def_use))
+        .collect();
+
+    // Typecheck the module.
+    let typing = typecheck(module, &reverse_postorders)?;
+
+    // Check the structure of the functions in the module.
+    for (function, (def_use, typing)) in
+        zip(module.functions.iter(), zip(def_uses.iter(), typing.iter()))
+    {
+        verify_structure(function, def_use, typing, &module.types)?;
+    }
+    Ok(typing)
+}
+
+/*
+ * There are structural constraints the IR must follow, such as all Phi nodes'
+ * control input must be a region node. This is where those properties are
+ * verified.
+ */
+fn verify_structure(
+    function: &Function,
+    def_use: &ImmutableDefUseMap,
+    typing: &Vec<TypeID>,
+    types: &Vec<Type>,
+) -> Result<(), String> {
+    for (idx, node) in function.nodes.iter().enumerate() {
+        let users = def_use.get_users(NodeID::new(idx));
+        match node {
+            // If, fork, and join nodes all have the same structural
+            // constraints - each must have exactly two ReadProd users, which
+            // reference differing elements of the node's output product.
+            Node::If {
+                control: _,
+                cond: _,
+            }
+            | Node::Fork {
+                control: _,
+                factor: _,
+            }
+            | Node::Join {
+                control: _,
+                data: _,
+            } => {
+                if users.len() != 2 {
+                    Err(format!(
+                        "{} node must have 2 users, not {}.",
+                        node.upper_case_name(),
+                        users.len()
+                    ))?;
+                }
+                if let (
+                    Node::ReadProd {
+                        prod: _,
+                        index: index1,
+                    },
+                    Node::ReadProd {
+                        prod: _,
+                        index: index2,
+                    },
+                ) = (
+                    &function.nodes[users[0].idx()],
+                    &function.nodes[users[1].idx()],
+                ) {
+                    if !((*index1 == 0 && *index2 == 1) || (*index1 == 1 && *index2 == 0)) {
+                        Err(format!("{} node's user ReadProd nodes must reference different elements of output product.", node.upper_case_name()))?;
+                    }
+                } else {
+                    Err(format!(
+                        "{} node's users must both be ReadProd nodes.",
+                        node.upper_case_name()
+                    ))?;
+                }
+            }
+            // Phi nodes must depend on a region node.
+            Node::Phi { control, data: _ } => {
+                if let Node::Region { preds: _ } = function.nodes[control.idx()] {
+                } else {
+                    Err("Phi node's control input must be a region node.")?;
+                }
+            }
+            // Return nodes must have no users.
+            Node::Return {
+                control: _,
+                value: _,
+            } => {
+                if users.len() != 0 {
+                    Err(format!(
+                        "Return node must have 0 users, not {}.",
+                        users.len()
+                    ))?;
+                }
+            }
+            // Match nodes are similar to if nodes, but have a variable number
+            // of ReadProd users, corresponding to the sum type being matched.
+            Node::Match { control: _, sum } => {
+                let sum_ty = &types[typing[sum.idx()].idx()];
+                if let Type::Summation(tys) = sum_ty {
+                    let correct_number_of_users = tys.len();
+                    if users.len() != correct_number_of_users {
+                        Err(format!(
+                            "Match node must have {} users, not {}.",
+                            correct_number_of_users,
+                            users.len()
+                        ))?;
+                    }
+                    let mut users_covered = bitvec![u8, Lsb0; 0; users.len()];
+                    for user in users {
+                        if let Node::ReadProd { prod: _, index } = function.nodes[user.idx()] {
+                            assert!(index < users.len(), "ReadProd child of match node reads from bad index, but ran after typecheck succeeded.");
+                            users_covered.set(index, true);
+                        }
+                    }
+                    if users_covered.count_ones() != users.len() {
+                        Err(format!("Match node's user ReadProd nodes must reference all {} elements of match node's output product, but they only reference {} of them.", users.len(), users_covered.count_ones()))?;
+                    }
+                } else {
+                    panic!("Type of match node's sum input is not a summation type, but ran after typecheck succeeded.");
+                }
+            }
+            _ => {}
+        };
+    }
+    Ok(())
+}
diff --git a/hercules_tools/src/hercules_dot/main.rs b/hercules_tools/src/hercules_dot/main.rs
index a9153689434d50bb7cb288d2068acb9cffd35372..226f91db9121ef0d02cb61c9c520f2b3596ce086 100644
--- a/hercules_tools/src/hercules_dot/main.rs
+++ b/hercules_tools/src/hercules_dot/main.rs
@@ -26,7 +26,10 @@ fn main() {
     let mut contents = String::new();
     file.read_to_string(&mut contents)
         .expect("PANIC: Unable to read input file contents.");
-    let module = hercules_ir::parse::parse(&contents);
+    let mut module =
+        hercules_ir::parse::parse(&contents).expect("PANIC: Failed to parse Hercules IR file.");
+    let _types = hercules_ir::verify::verify(&mut module)
+        .expect("PANIC: Failed to typecheck Hercules IR module.");
     if args.output.is_empty() {
         let mut tmp_path = temp_dir();
         tmp_path.push("hercules_dot.dot");