diff --git a/Cargo.lock b/Cargo.lock
index 2624eb82c..e93849f52 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1327,6 +1327,7 @@ dependencies = [
  "merc_aterm",
  "merc_data",
  "merc_syntax",
+ "merc_typecheck",
  "merc_utilities",
  "rand",
  "rustc-hash 2.1.2",
@@ -1432,6 +1433,17 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "merc_typecheck"
+version = "2.0.0"
+dependencies = [
+ "indoc",
+ "merc_collections",
+ "merc_syntax",
+ "merc_utilities",
+ "thiserror",
+]
+
 [[package]]
 name = "merc_unsafety"
 version = "2.0.0"
diff --git a/Cargo.toml b/Cargo.toml
index 04724d04c..fd21d4aa7 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -42,6 +42,7 @@ members = [
     "crates/symbolic",
     "crates/syntax",
     "crates/tools",
+    "crates/typecheck",
     "crates/unsafety",
     "crates/utilities",
     "crates/vpg",
@@ -132,9 +133,9 @@ merc_ldd = { version = "3.0", path = "crates/ldd" }
 merc_lts = { version = "2.0", path = "crates/lts" }
 merc_macros = { version = "2.0", path = "crates/macros" }
 merc_number = { version = "2.0", path = "crates/number" }
-merc_refinement = { version = "2.0", path = "crates/refinement" }
 merc_rec-tests = { path = "crates/rec-tests" }
 merc_reduction = { version = "2.0", path = "crates/reduction" }
+merc_refinement = { version = "2.0", path = "crates/refinement" }
 merc_sabre = { version = "2.0", path = "crates/sabre" }
 merc_sabre-compiling = { path = "crates/sabre_compiling" }
 merc_sabre-ffi = { path = "crates/sabre_compiling/sabre_ffi" }
@@ -142,6 +143,7 @@ merc_sharedmutex = { version = "2.0", path = "crates/sharedmutex" }
 merc_symbolic = { version = "3.0", path = "crates/symbolic", features = ["clap"] }
 merc_syntax = { version = "2.0", path = "crates/syntax" }
 merc_tools = { path = "crates/tools" }
+merc_typecheck = { path = "crates/typecheck" }
 merc_unsafety = { version = "2.0", path = "crates/unsafety" }
 merc_utilities = { version = "3.0", path = "crates/utilities" }
 merc_vpg = { path = "crates/vpg", features = ["clap"] }
diff --git a/crates/collections/src/block_partition.rs b/crates/collections/src/block_partition.rs
index 13f257267..56dadb917 100644
--- a/crates/collections/src/block_partition.rs
+++ b/crates/collections/src/block_partition.rs
@@ -31,6 +31,10 @@ impl<A: Clone + fmt::Debug + Default> BlockPartition<A> {
 
 impl<A: Clone + fmt::Debug + Default> BlockPartition<A> {
     /// Create a block partition from an indexed partition.
+    ///
+    /// This function creates a new partition that is dense, i.e. it does not
+    /// contain empty blocks, and the blocks are indexed from 0 to n-1 even if the
+    /// indexed partition is sparse.
     pub fn from_indexed_partition(partition: &IndexedPartition) -> Self {
         let mut blocks = vec![Block::new_empty(); partition.num_of_blocks()];
         let num_of_blocks = partition.iter().count();
@@ -253,11 +257,15 @@ impl Iterator for BlockIter<'_> {
 
 #[cfg(test)]
 mod tests {
-    use merc_utilities::random_test;
     use rand::RngExt;
     use rand::seq::IteratorRandom;
 
-    use super::*;
+    use merc_utilities::random_test;
+
+    use super::BlockIndex;
+    use super::BlockPartition;
+    use super::IndexedPartition;
+    use super::trace;
 
     #[test]
     fn test_simple_block_partition() {
@@ -302,6 +310,11 @@ mod tests {
                         expected_block,
                         "Block {block} contains elements from different indexed-partition blocks"
                     );
+                    assert_eq!(
+                        partition.block(element),
+                        expected_block,
+                        "Block {block} contains elements from different indexed-partition blocks"
+                    );
                 }
             }
         })
diff --git a/crates/collections/src/compressed_vec.rs b/crates/collections/src/compressed_vec.rs
index de25afd6b..4b4fb9d4b 100644
--- a/crates/collections/src/compressed_vec.rs
+++ b/crates/collections/src/compressed_vec.rs
@@ -484,14 +484,15 @@ impl<T: CompressedEntry + Copy, Tag> CompressedEntry for TagIndex<T, Tag> {
 
 #[cfg(test)]
 mod tests {
-    use super::*;
-
     use rand::RngExt;
     use rand::distr::Uniform;
     use rand::seq::SliceRandom;
 
     use merc_utilities::random_test;
 
+    use super::ByteCompressedVec;
+    use super::CompressedEntry;
+
     #[test]
     fn test_index_bytevector() {
         let mut vec = ByteCompressedVec::new();
diff --git a/crates/collections/src/indexed_set.rs b/crates/collections/src/indexed_set.rs
index d98b158e4..bff52951c 100644
--- a/crates/collections/src/indexed_set.rs
+++ b/crates/collections/src/indexed_set.rs
@@ -382,9 +382,8 @@ impl<'a, T, S> IntoIterator for &'a IndexedSet<T, S> {
 
 #[cfg(test)]
 mod tests {
-    use std::collections::HashMap;
-
     use rand::RngExt;
+    use std::collections::HashMap;
 
     use merc_utilities::random_test;
 
diff --git a/crates/lts/src/labelled_transition_system.rs b/crates/lts/src/labelled_transition_system.rs
index fdd9050c0..f8d48758f 100644
--- a/crates/lts/src/labelled_transition_system.rs
+++ b/crates/lts/src/labelled_transition_system.rs
@@ -1,6 +1,7 @@
 #![forbid(unsafe_code)]
 
 use std::collections::HashMap;
+use std::collections::HashSet;
 use std::fmt;
 
 use merc_collections::ByteCompressedVec;
@@ -412,6 +413,26 @@ impl<Label: TransitionLabel> LabelledTransitionSystem<Label> {
                 num_states
             );
         }
+
+        for state in 0..num_states {
+            let start = self.states.index(state);
+            let end = self.states.index(state + 1);
+            let mut seen = HashSet::with_capacity(end.saturating_sub(start));
+
+            for i in start..end {
+                let edge = (
+                    self.transition_labels.index(i).value(),
+                    self.transition_to.index(i).value(),
+                );
+
+                debug_assert!(
+                    seen.insert(edge),
+                    "state {state} has duplicate outgoing transition with label {} to state {}",
+                    edge.0,
+                    edge.1
+                );
+            }
+        }
     }
 
     /// Returns metrics about the LTS.
diff --git a/crates/sabre/Cargo.toml b/crates/sabre/Cargo.toml
index 3b9746c46..dada16e0d 100644
--- a/crates/sabre/Cargo.toml
+++ b/crates/sabre/Cargo.toml
@@ -16,6 +16,7 @@ version.workspace = true
 merc_aterm.workspace = true
 merc_data.workspace = true
 merc_syntax.workspace = true
+merc_typecheck.workspace = true
 merc_utilities.workspace = true
 
 rustc-hash.workspace = true
diff --git a/crates/syntax/src/builder.rs b/crates/syntax/src/builder.rs
index 33feb9dc7..e16561feb 100644
--- a/crates/syntax/src/builder.rs
+++ b/crates/syntax/src/builder.rs
@@ -17,9 +17,10 @@ where
     apply_statefrm_rec(formula, &mut function)
 }
 
-pub fn apply_sort_expression<F>(sort_expr: SortExpression, mut function: F) -> Result<SortExpression, MercError>
+/// Applies the given function recursively to the sort expression.
+pub fn apply_sort_expression<E, F>(sort_expr: SortExpression, mut function: F) -> Result<SortExpression, E>
 where
-    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, MercError>,
+    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, E>,
 {
     apply_sort_expression_rec(sort_expr, &mut function)
 }
@@ -164,9 +165,10 @@ where
     }
 }
 
-fn apply_sort_expression_rec<F>(sort_expr: SortExpression, apply: &mut F) -> Result<SortExpression, MercError>
+/// See [`apply_sort_expression`].
+fn apply_sort_expression_rec<E, F>(sort_expr: SortExpression, apply: &mut F) -> Result<SortExpression, E>
 where
-    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, MercError>,
+    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, E>,
 {
     if let Some(sort_expr) = apply(&sort_expr)? {
         // A substitution was made, return the new sort expression.
@@ -203,7 +205,18 @@ where
             let inner = apply_sort_expression_rec(*sort_expression, apply)?;
             Ok(SortExpression::Complex(complex_sort, Box::new(inner)))
         }
-        SortExpression::Reference(_) | SortExpression::Simple(_) => {
+        SortExpression::FlattenedFunction { domain, range } => {
+            let domain = domain
+                .into_iter()
+                .map(|sort| apply_sort_expression_rec(sort, apply))
+                .collect::<Result<Vec<SortExpression>, _>>()?;
+            let range = apply_sort_expression_rec(*range, apply)?;
+            Ok(SortExpression::FlattenedFunction {
+                domain,
+                range: Box::new(range),
+            })
+        }
+        SortExpression::Reference(_) | SortExpression::Simple(_) | SortExpression::Resolved(_, _) => {
             // Ignored
             Ok(sort_expr)
         }
diff --git a/crates/syntax/src/syntax_tree.rs b/crates/syntax/src/syntax_tree.rs
index b2cae02f8..e3dc5f86b 100644
--- a/crates/syntax/src/syntax_tree.rs
+++ b/crates/syntax/src/syntax_tree.rs
@@ -3,10 +3,10 @@ use std::hash::Hash;
 use merc_utilities::TagIndex;
 
 /// A unique type for declarations.
-pub struct DeclTag;
+pub struct DefTag;
 
 /// The index type for a label.
-pub type DeclId = TagIndex<usize, DeclTag>;
+pub type DefId = TagIndex<usize, DefTag>;
 
 /// A complete mCRL2 process specification.
 #[derive(Debug, Default, Eq, PartialEq, Hash)]
@@ -106,7 +106,7 @@ pub struct IdDecl {
     /// Source location information
     pub span: Span,
     /// Unique ID assigned to this declaration during name resolution.
-    pub id: Option<DeclId>,
+    pub id: Option<DefId>,
 }
 
 impl IdDecl {
@@ -143,6 +143,13 @@ pub enum SortExpression {
     Simple(Sort),
     /// Parameterized complex sort
     Complex(ComplexSort, Box<SortExpression>),
+    /// Resolved reference to a sort after name resolution
+    Resolved(String, DefId),
+    /// Function sort (A_0 # ... # A_n -> B) after flattening (performed during name resolution)
+    FlattenedFunction {
+        domain: Vec<SortExpression>,
+        range: Box<SortExpression>,
+    },
 }
 
 /// Constructor declaration
@@ -183,7 +190,7 @@ pub struct SortDecl {
     /// Where the sort is defined
     pub span: Span,
     /// Unique ID assigned to this declaration during name resolution.
-    pub id: Option<DeclId>,
+    pub id: Option<DefId>,
 }
 
 impl SortDecl {
diff --git a/crates/syntax/src/syntax_tree_display.rs b/crates/syntax/src/syntax_tree_display.rs
index 5ec503760..2c96a26a7 100644
--- a/crates/syntax/src/syntax_tree_display.rs
+++ b/crates/syntax/src/syntax_tree_display.rs
@@ -340,13 +340,18 @@ impl fmt::Display for SortExpression {
         match self {
             SortExpression::Product { lhs, rhs } => write!(f, "({lhs} # {rhs})"),
             SortExpression::Function { domain, range } => write!(f, "({domain} -> {range})"),
-            SortExpression::Reference(ident) => write!(f, "{ident}"),
+            SortExpression::Reference(name) => write!(f, "{name}"),
             SortExpression::Simple(sort) => write!(f, "{sort}"),
             SortExpression::Complex(complex, inner) => write!(f, "{complex}({inner})"),
             SortExpression::Struct { inner } => {
                 write!(f, "struct ")?;
                 write!(f, "{}", inner.iter().format(" | "))
             }
+            SortExpression::Resolved(name, _id) => write!(f, "{name}"),
+            SortExpression::FlattenedFunction { domain, range } => {
+                let domain = domain.iter().format(" # ");
+                write!(f, "({domain} -> {range})")
+            }
         }
     }
 }
diff --git a/crates/syntax/src/visitor.rs b/crates/syntax/src/visitor.rs
index f8f1d7ace..6875169f6 100644
--- a/crates/syntax/src/visitor.rs
+++ b/crates/syntax/src/visitor.rs
@@ -1,3 +1,4 @@
+use std::convert::Infallible;
 use std::ops::ControlFlow;
 
 use merc_utilities::MercError;
@@ -20,9 +21,21 @@ where
     visit_statefrm_rec(formula, &mut visitor)
 }
 
-pub fn visit_sort_expr<T, F>(sort_expr: &SortExpression, mut visitor: F) -> Result<Option<T>, MercError>
+/// Visits all sort expressions in the sort expression.
+pub fn visit_sort_expr<T, F>(sort_expr: &SortExpression, mut visitor: F) -> Option<T>
 where
-    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, MercError>,
+    F: FnMut(&SortExpression) -> ControlFlow<T>,
+{
+    try_visit_sort_expr(sort_expr, |sort_expr| -> Result<_, Infallible> {
+        Ok(visitor(sort_expr))
+    })
+    .expect("Inner function does not fail")
+}
+
+/// Visits all sort expressions in the sort expression, allowing the visitor to return an error.
+pub fn try_visit_sort_expr<E, T, F>(sort_expr: &SortExpression, mut visitor: F) -> Result<Option<T>, E>
+where
+    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, E>,
 {
     visit_sort_expr_rec(sort_expr, &mut visitor)
 }
@@ -75,9 +88,10 @@ where
     Ok(None)
 }
 
-fn visit_sort_expr_rec<T, F>(sort_expr: &SortExpression, function: &mut F) -> Result<Option<T>, MercError>
+/// See [`visit_sort_expr`].
+fn visit_sort_expr_rec<E, T, F>(sort_expr: &SortExpression, function: &mut F) -> Result<Option<T>, E>
 where
-    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, MercError>,
+    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, E>,
 {
     if let ControlFlow::Break(result) = function(sort_expr)? {
         // The visitor requested to break the traversal.
@@ -103,7 +117,13 @@ where
         SortExpression::Complex(_complex_sort, sort_expression) => {
             visit_sort_expr_rec(sort_expression, function)?;
         }
-        SortExpression::Reference(_) | SortExpression::Simple(_) => {}
+        SortExpression::FlattenedFunction { domain, range } => {
+            for domain_sort in domain {
+                visit_sort_expr_rec(domain_sort, function)?;
+            }
+            visit_sort_expr_rec(range, function)?;
+        }
+        SortExpression::Reference(_) | SortExpression::Simple(_) | SortExpression::Resolved(_, _) => {}
     }
 
     // The visitor did not break the traversal.
diff --git a/crates/typecheck/Cargo.toml b/crates/typecheck/Cargo.toml
new file mode 100644
index 000000000..34435a84d
--- /dev/null
+++ b/crates/typecheck/Cargo.toml
@@ -0,0 +1,17 @@
+[package]
+name = "merc_typecheck"
+
+edition.workspace = true
+homepage.workspace = true
+license.workspace = true
+repository.workspace = true
+rust-version.workspace = true
+version.workspace = true
+
+[dependencies]
+indoc.workspace = true
+thiserror.workspace = true
+
+merc_collections.workspace = true
+merc_syntax.workspace = true
+merc_utilities.workspace = true
\ No newline at end of file
diff --git a/crates/typecheck/src/alias.rs b/crates/typecheck/src/alias.rs
new file mode 100644
index 000000000..3356f5d6b
--- /dev/null
+++ b/crates/typecheck/src/alias.rs
@@ -0,0 +1,104 @@
+use std::collections::HashMap;
+use std::ops::ControlFlow;
+
+use merc_collections::BlockIndex;
+use merc_collections::BlockPartition;
+use merc_collections::Graph;
+use merc_collections::scc_decomposition;
+use merc_syntax::DefId;
+use merc_syntax::SortExpression;
+use merc_syntax::UntypedDataSpecification;
+use merc_syntax::visit_sort_expr;
+use merc_utilities::TagIndex;
+
+/// Returns true iff there is a cycle in the alias declarations.
+pub fn has_alias_cycle(spec: &UntypedDataSpecification) -> Result<(), Vec<DefId>> {
+    // A mapping that keeps track of the relation between sorts.
+    let mut mapping: HashMap<DefId, Vec<DefId>> = HashMap::new();
+
+    for sort_decl in &spec.sort_declarations {
+        if let Some(alias) = &sort_decl.expr {
+            let mut visited = Vec::new();
+
+            visit_sort_expr::<(), _>(alias, |sort| {
+                if let SortExpression::Resolved(_, id) = sort {
+                    visited.push(*id);
+                }
+
+                ControlFlow::Continue(())
+            });
+
+            mapping.insert(sort_decl.id.expect("Name must have been resolved"), visited);
+        }
+    }
+
+    let scc_partition =
+        BlockPartition::<()>::from_indexed_partition(&scc_decomposition(&SortGraph { mapping }, |_, _, _| true));
+
+    for block in (0..scc_partition.len()).map(BlockIndex::new) {
+        if scc_partition.block(block).len() > 1 {
+            return Err(scc_partition.iter_block(block).map(|id| DefId::new(id)).collect());
+        }
+    }
+    Ok(())
+}
+
+/// A graph structure representing the alias declarations in a data
+/// specification. The vertices are the sorts, and there is an edge from sort A
+/// to sort B if B is contained in the alias of A, i.e. `A -> B` if `A = List(B)`.
+struct SortGraph {
+    mapping: HashMap<DefId, Vec<DefId>>,
+}
+
+/// A unique type for the sorts.
+pub struct SortTag;
+
+/// The index type for a sort.
+pub type SortIndex = TagIndex<usize, SortTag>;
+
+impl Graph for SortGraph {
+    type VertexIndex = SortIndex;
+
+    type LabelIndex = ();
+
+    fn num_of_vertices(&self) -> usize {
+        self.mapping.keys().map(|id| **id).max().map_or(0, |max_id| max_id + 1)
+    }
+
+    fn iter_vertices(&self) -> impl Iterator<Item = Self::VertexIndex> {
+        (0..self.num_of_vertices()).map(SortIndex::new)
+    }
+
+    fn outgoing_edges(&self, vertex: Self::VertexIndex) -> impl Iterator<Item = (Self::LabelIndex, Self::VertexIndex)> {
+        self.mapping
+            .get(&DefId::new(*vertex))
+            .into_iter()
+            .flat_map(|targets| targets.iter())
+            .map(|id| ((), SortIndex::new(**id)))
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use merc_syntax::UntypedDataSpecification;
+
+    use crate::DataSpecification;
+    use crate::WellTypedError;
+
+    #[test]
+    fn test_trivial_alias_cycle() {
+        let spec = UntypedDataSpecification::parse(
+            "sort S = T;
+            T = U;
+            U = S;",
+        )
+        .unwrap();
+
+        match DataSpecification::from_untyped(spec) {
+            Err(WellTypedError::AliasCycle { sorts })
+                if sorts == vec!["S".to_string(), "T".to_string(), "U".to_string()] => {}
+            Err(other) => panic!("Unexpected error {:?}", other),
+            _ => panic!("Expected from_untyped to fail"),
+        }
+    }
+}
diff --git a/crates/typecheck/src/data_specification.rs b/crates/typecheck/src/data_specification.rs
new file mode 100644
index 000000000..0277ef2ee
--- /dev/null
+++ b/crates/typecheck/src/data_specification.rs
@@ -0,0 +1,106 @@
+use std::collections::HashMap;
+use std::convert::Infallible;
+
+use merc_syntax::DefId;
+use merc_syntax::EqnSpec;
+use merc_syntax::IdDecl;
+use merc_syntax::SortExpression;
+use merc_syntax::UntypedDataSpecification;
+use merc_syntax::apply_sort_expression;
+
+use crate::WellTypedError;
+use crate::basic_sort_data_specification;
+use crate::has_alias_cycle;
+use crate::is_well_typed;
+use crate::map_sorts_in_spec;
+use crate::resolve_names;
+
+/// A type checked and well-typed data specification.
+pub struct DataSpecification {
+    pub sort_declarations: HashMap<DefId, (Vec<IdDecl>, Vec<EqnSpec>)>,
+}
+
+impl DataSpecification {
+    /// Create a completed well-typed data specification from an untyped data specification.
+    pub fn from_untyped(mut spec: UntypedDataSpecification) -> Result<Self, WellTypedError> {
+        map_sorts_in_spec(&mut spec, |sort| -> Result<_, Infallible> {
+            Ok(flatten_function_sorts(sort))
+        })
+        .expect("The inner function never fails");
+
+        let sorts = resolve_names(&mut spec)?;
+
+        has_alias_cycle(&spec).map_err(|cycle| WellTypedError::AliasCycle {
+            sorts: cycle
+                .iter()
+                .map(|id| sorts.get_by_index(**id).expect("The sort should be declared").clone())
+                .collect(),
+        })?;
+
+        is_well_typed(&spec)?;
+
+        // Obtain the definitions for all basic sort.
+        let _basic_sort_spec = basic_sort_data_specification().map_err(|e| WellTypedError::Custom(e))?;
+
+        // Add all the occurring standard sorts to the specification.
+
+        Ok(Self {
+            sort_declarations: HashMap::new(), // TODO: Fill this in with the actual sort declarations.
+        })
+    }
+}
+
+/// Returns the target sort of a sort expression, i.e. the range of a function
+/// sort, or the sort itself if it is not a function sort.
+pub fn target_sort(sort: &SortExpression) -> &SortExpression {
+    debug_assert!(
+        !matches!(sort, SortExpression::Function { .. }),
+        "target_sort should only be called on non-function sorts or flattened function sorts"
+    );
+
+    if let SortExpression::FlattenedFunction { domain: _, range } = sort {
+        range
+    } else {
+        sort
+    }
+}
+
+/// Returns the arguments of a function sort, requires that function sorts are flattened.
+pub fn argument_sorts(sort: &SortExpression) -> &Vec<SortExpression> {
+    if let SortExpression::FlattenedFunction { domain, range: _ } = sort {
+        domain
+    } else {
+        unreachable!("argument_sorts should only be called on function sorts")
+    }
+}
+
+/// Replaces sort references of `identifier` in `sort` by the given `result_sort`.
+fn flatten_function_sorts(sort: &SortExpression) -> SortExpression {
+    apply_sort_expression(sort.clone(), |expr| -> Result<_, Infallible> {
+        if let SortExpression::Function { domain, range } = expr {
+            let mut flattened_domain = Vec::new();
+            flatten_function_domain_rec(domain, &mut flattened_domain);
+
+            return Ok(Some(SortExpression::FlattenedFunction {
+                domain: flattened_domain,
+                range: range.clone(),
+            }));
+        }
+
+        Ok(None)
+    })
+    .expect("flatten_function_sorts should not fail")
+}
+
+/// Flattens a function sort of the form ((A_0 # A_1) # ... # A_n) -> B into a
+/// sort of the form A_0 # A_1 # ... # A_n -> B, where B is the original range
+/// of the function.
+fn flatten_function_domain_rec(sort: &SortExpression, domain: &mut Vec<SortExpression>) {
+    match sort {
+        SortExpression::Product { lhs, rhs } => {
+            flatten_function_domain_rec(lhs, domain);
+            flatten_function_domain_rec(rhs, domain);
+        }
+        _ => domain.push(sort.clone()),
+    }
+}
diff --git a/crates/typecheck/src/is_finite.rs b/crates/typecheck/src/is_finite.rs
new file mode 100644
index 000000000..28b66c9c5
--- /dev/null
+++ b/crates/typecheck/src/is_finite.rs
@@ -0,0 +1,24 @@
+use merc_syntax::ComplexSort;
+use merc_syntax::SortExpression;
+
+/// Returns true iff the sort is finite.
+pub fn is_finite(sort: &SortExpression) -> bool {
+    match sort {
+        SortExpression::Product { lhs, rhs } => is_finite(lhs) && is_finite(rhs),
+        SortExpression::Function { domain, range: _ } => is_finite(domain),
+        SortExpression::Struct { inner } => inner
+            .iter()
+            .all(|decl| decl.args.iter().all(|(_, sort)| is_finite(sort))),
+        SortExpression::Simple(sort) => match sort {
+            merc_syntax::Sort::Bool => true,
+            _ => false, // All number sorts are infinite.
+        },
+        SortExpression::Complex(complex_sort, sort_expression) => {
+            (*complex_sort == ComplexSort::Set || *complex_sort == ComplexSort::FSet) && is_finite(sort_expression)
+        }
+        SortExpression::FlattenedFunction { domain, range: _ } => domain.iter().all(|sort| is_finite(sort)),
+        SortExpression::Reference(_) | SortExpression::Resolved(_, _) => {
+            unreachable!("is_finite should not be called on reference sorts")
+        }
+    }
+}
diff --git a/crates/typecheck/src/is_well_typed.rs b/crates/typecheck/src/is_well_typed.rs
new file mode 100644
index 000000000..d1464ac8b
--- /dev/null
+++ b/crates/typecheck/src/is_well_typed.rs
@@ -0,0 +1,131 @@
+use thiserror::Error;
+
+use merc_syntax::SortExpression;
+use merc_syntax::UntypedDataSpecification;
+use merc_utilities::MercError;
+
+use crate::is_nonempty_sort;
+use crate::target_sort;
+
+/// Checks if a signature is well-typed, i.e. it satisfies the conditions of 15.1.7.
+pub fn is_well_typed(spec: &UntypedDataSpecification) -> Result<(), WellTypedError> {
+    are_constructors_and_mappings_disjoint(spec)?;
+
+    // Check that there are no constructors defined for the basic sorts.
+    for constructor in &spec.constructor_declarations {
+        let sort = target_sort(&constructor.sort);
+
+        // There are not more constructors for basic sorts.
+        if is_basic_sort(sort) {
+            return Err(WellTypedError::ConstructorForBasicSort {
+                constructor: constructor.identifier.clone(),
+                sort: sort.to_string(),
+            }
+            .into());
+        }
+
+        // Function sorts are not constructor sorts
+        if matches!(sort, SortExpression::Function { domain: _, range: _ }) {
+            return Err(WellTypedError::ConstructorForFunctionSort {
+                constructor: constructor.identifier.clone(),
+                sort: sort.to_string(),
+            });
+        }
+    }
+
+    // Check that all sorts are syntactically non-empty.
+    for sort in &spec.sort_declarations {
+        if !is_nonempty_sort(&sort.identifier, spec) {
+            return Err(WellTypedError::EmptySort {
+                sort: sort.identifier.clone(),
+            });
+        }
+    }
+
+    Ok(())
+}
+
+#[derive(Debug, Error)]
+pub enum WellTypedError {
+    #[error("Constructor '{}' and mapping '{}' have the same identifier", constructor, map)]
+    ConstructorAndMappingConflict { constructor: String, map: String },
+
+    #[error(
+        "Constructors cannot be defined for basic sorts, but constructor '{}' is defined for sort '{}'",
+        constructor,
+        sort
+    )]
+    ConstructorForBasicSort { constructor: String, sort: String },
+
+    #[error(
+        "Constructors cannot be defined for function sorts, but constructor '{}' is defined for sort '{}'",
+        constructor,
+        sort
+    )]
+    ConstructorForFunctionSort { constructor: String, sort: String },
+
+    #[error("Sort '{}' is syntactically empty", sort)]
+    EmptySort { sort: String },
+
+    #[error("Alias cycle detected: {:?}", sorts)]
+    AliasCycle { sorts: Vec<String> },
+
+    #[error("Error: '{}'", 0)]
+    Custom(MercError),
+
+    // These are name resolution errors, but we include them here to avoid having to define a separate error type for name resolution.
+    #[error("Duplicate sort declaration: '{}'", sort)]
+    DuplicateSortDeclaration { sort: String },
+
+    #[error("Undefined sort: '{}'", sort)]
+    UndefinedSort { sort: String },
+}
+
+/// Checks that the constructors and mappings are disjoint, i.e. that no identifier is both a constructor and a mapping.
+fn are_constructors_and_mappings_disjoint(spec: &UntypedDataSpecification) -> Result<(), WellTypedError> {
+    for constructor in &spec.constructor_declarations {
+        if let Some(map) = spec
+            .map_declarations
+            .iter()
+            .find(|map| map.identifier == constructor.identifier)
+        {
+            return Err(WellTypedError::ConstructorAndMappingConflict {
+                constructor: constructor.identifier.clone(),
+                map: map.identifier.clone(),
+            });
+        }
+    }
+
+    Ok(())
+}
+
+/// The set of basic sorts `BS` are exactly the sorts Bool, Pos, Int, Nat, and Real. Definition 15.1.2.
+fn is_basic_sort(sort: &SortExpression) -> bool {
+    matches!(sort, SortExpression::Simple(_))
+}
+
+#[cfg(test)]
+mod tests {
+    use merc_syntax::UntypedDataSpecification;
+
+    use crate::DataSpecification;
+    use crate::WellTypedError;
+
+    #[test]
+    fn test_well_typed_spec() {
+        let spec = UntypedDataSpecification::parse(
+            "
+            sort D;
+            cons f: D -> Nat;
+        ",
+        )
+        .unwrap();
+
+        match DataSpecification::from_untyped(spec) {
+            Err(WellTypedError::ConstructorForBasicSort { constructor, sort })
+                if constructor == "f" && sort == "Nat" => {}
+            Err(other) => panic!("Unexpected error {:?}", other),
+            _ => panic!("Expected from_untyped to fail"),
+        }
+    }
+}
diff --git a/crates/typecheck/src/lib.rs b/crates/typecheck/src/lib.rs
new file mode 100644
index 000000000..a391accdc
--- /dev/null
+++ b/crates/typecheck/src/lib.rs
@@ -0,0 +1,15 @@
+mod alias;
+mod data_specification;
+mod is_finite;
+mod is_well_typed;
+mod name_resolution;
+mod non_empty;
+mod standard_sorts;
+
+pub use alias::*;
+pub use data_specification::*;
+pub use is_finite::*;
+pub use is_well_typed::*;
+pub use name_resolution::*;
+pub use non_empty::*;
+pub use standard_sorts::*;
diff --git a/crates/typecheck/src/name_resolution.rs b/crates/typecheck/src/name_resolution.rs
new file mode 100644
index 000000000..bbddc0256
--- /dev/null
+++ b/crates/typecheck/src/name_resolution.rs
@@ -0,0 +1,75 @@
+use merc_collections::IndexedSet;
+use merc_syntax::DefId;
+use merc_syntax::SortExpression;
+use merc_syntax::UntypedDataSpecification;
+use merc_syntax::apply_sort_expression;
+
+use crate::WellTypedError;
+
+/// Ensure that all DefIds in the data specification are resolved. Returns an
+/// indexed set that indicates the mapping from sort identifiers to their
+/// DefIds.
+pub fn resolve_names(spec: &mut UntypedDataSpecification) -> Result<IndexedSet<String>, WellTypedError> {
+    // Every sort declaration should have a unique name.
+    let mut sorts = IndexedSet::new();
+
+    // Assign unique IDs to all sort declarations
+    for (i, sort) in spec.sort_declarations.iter_mut().enumerate() {
+        sort.id = Some(DefId::new(i));
+
+        if !sorts.insert(sort.identifier.clone()).1 {
+            return Err(WellTypedError::DuplicateSortDeclaration {
+                sort: sort.identifier.clone(),
+            });
+        }
+    }
+
+    // Resolve all sorts.
+    map_sorts_in_spec(spec, |sort| resolve_sort_id(sort, &sorts))?;
+
+    Ok(sorts)
+}
+
+// Apply a mapping function to every sort in the specification.
+pub fn map_sorts_in_spec<E, F>(spec: &mut UntypedDataSpecification, mut f: F) -> Result<(), E>
+where
+    F: FnMut(&SortExpression) -> Result<SortExpression, E>,
+{
+    for sort in &mut spec.sort_declarations {
+        if let Some(expr) = &sort.expr {
+            // Only apply to type aliases.
+            sort.expr = Some(f(expr)?);
+        }
+    }
+
+    for constructor in &mut spec.constructor_declarations {
+        constructor.sort = f(&constructor.sort)?;
+    }
+
+    for map in &mut spec.map_declarations {
+        map.sort = f(&map.sort)?;
+    }
+
+    for equation in &mut spec.equation_declarations {
+        for var in &mut equation.variables {
+            var.sort = f(&var.sort)?;
+        }
+    }
+
+    Ok(())
+}
+
+/// Replaces sort references of `identifier` in `sort` by the given `result_sort`.
+fn resolve_sort_id(sort: &SortExpression, resolved: &IndexedSet<String>) -> Result<SortExpression, WellTypedError> {
+    apply_sort_expression(sort.clone(), |expr| {
+        if let SortExpression::Reference(name) = expr {
+            if let Some(id) = resolved.index(name) {
+                return Ok(Some(SortExpression::Resolved(name.clone(), DefId::new(*id))));
+            }
+
+            return Err(WellTypedError::UndefinedSort { sort: name.clone() });
+        }
+
+        Ok(None)
+    })
+}
diff --git a/crates/typecheck/src/non_empty.rs b/crates/typecheck/src/non_empty.rs
new file mode 100644
index 000000000..d31b98ef4
--- /dev/null
+++ b/crates/typecheck/src/non_empty.rs
@@ -0,0 +1,89 @@
+use std::collections::HashSet;
+
+use merc_syntax::DefId;
+use merc_syntax::IdDecl;
+use merc_syntax::SortExpression;
+use merc_syntax::UntypedDataSpecification;
+
+use crate::argument_sorts;
+use crate::target_sort;
+
+/// Returns true iff the sort is syntactically non-empty, i.e., there is at
+/// least one constructor for the target sort that has a non-empty sort.
+pub fn is_nonempty_sort(sort: &str, spec: &UntypedDataSpecification) -> bool {
+    debug_assert!(
+        spec.sort_declarations.iter().any(|id| id.id.is_some()),
+        "The sorts must be resolved"
+    );
+
+    let sort_id = spec
+        .sort_declarations
+        .iter()
+        .find(|id| id.identifier == sort)
+        .expect("The sort should be declared")
+        .id
+        .unwrap();
+
+    let mut seen = HashSet::new();
+    is_nonempty_sort_rec(sort_id, &spec.constructor_declarations, &mut seen)
+}
+
+/// The recursive definition of non-emptiness.
+fn is_nonempty_sort_rec(sort: DefId, constructors: &Vec<IdDecl>, seen: &mut HashSet<DefId>) -> bool {
+    if seen.contains(&sort) {
+        return false; // We have already seen this sort, so we have a cycle.
+    }
+
+    for constructor in constructors.iter().filter(|id| {
+        if let SortExpression::Resolved(_, id) = target_sort(&id.sort) {
+            *id == sort
+        } else {
+            unreachable!(
+                "The target sort of a constructor should always be a reference sort, but is not for {:?}",
+                id.sort
+            )
+        }
+    }) {
+        if argument_sorts(&constructor.sort).is_empty() {
+            return true; // We have found a constructor with no arguments, so the sort is non-empty.
+        }
+
+        seen.insert(sort); // Mark the current sort as seen to avoid cycles.
+
+        if argument_sorts(&constructor.sort).iter().all(|arg| match arg {
+            SortExpression::Resolved(_, id) => is_nonempty_sort_rec(*id, constructors, seen),
+            _ => true,
+        }) {
+            return true; // All argument sorts are non-empty, so the sort is non-empty.
+        }
+
+        seen.remove(&sort); // Unmark the current sort as seen to allow other paths to explore it.        
+    }
+
+    false
+}
+
+#[cfg(test)]
+mod tests {
+    use merc_syntax::UntypedDataSpecification;
+
+    use crate::DataSpecification;
+    use crate::WellTypedError;
+
+    #[test]
+    fn test_empty_data_spec() {
+        let spec = UntypedDataSpecification::parse(
+            "
+            sort D;
+            cons f: D -> D;
+        ",
+        )
+        .unwrap();
+
+        match DataSpecification::from_untyped(spec) {
+            Err(WellTypedError::EmptySort { sort }) if sort == "D" => {}
+            Err(other) => panic!("Unexpected {:?}", other),
+            _ => panic!("Unexpected from_untyped to fail"),
+        }
+    }
+}
diff --git a/crates/typecheck/src/standard_sorts.rs b/crates/typecheck/src/standard_sorts.rs
new file mode 100644
index 000000000..354636aec
--- /dev/null
+++ b/crates/typecheck/src/standard_sorts.rs
@@ -0,0 +1,146 @@
+use std::convert::Infallible;
+
+use indoc::formatdoc;
+
+use merc_syntax::ComplexSort;
+use merc_syntax::SortExpression;
+use merc_syntax::UntypedDataSpecification;
+use merc_syntax::apply_sort_expression;
+use merc_utilities::MercError;
+
+/// Returns a standard data specification containing the standard sorts and their associated constructors, mappings, and equations.
+pub fn basic_sort_data_specification() -> Result<UntypedDataSpecification, MercError> {
+    let mut result = UntypedDataSpecification::default();
+
+    // Append the relevant specifications for the sorts that are present in the specification.
+    result.merge(&UntypedDataSpecification::parse(include_str!(
+        "../../syntax/spec/bool.mcrl2"
+    ))?);
+    result.merge(&UntypedDataSpecification::parse(include_str!(
+        "../../syntax/spec/pos.mcrl2"
+    ))?);
+    result.merge(&UntypedDataSpecification::parse(include_str!(
+        "../../syntax/spec/int.mcrl2"
+    ))?);
+    result.merge(&UntypedDataSpecification::parse(include_str!(
+        "../../syntax/spec/nat.mcrl2"
+    ))?);
+    result.merge(&UntypedDataSpecification::parse(include_str!(
+        "../../syntax/spec/real.mcrl2"
+    ))?);
+
+    Ok(result)
+}
+
+/// Constructs a data specification for a standard sort;
+pub fn standard_sort(sort: &SortExpression) -> Result<UntypedDataSpecification, MercError> {
+    if let SortExpression::Complex(complex, sort) = sort {
+        let text = match complex {
+            ComplexSort::List => include_str!("../../syntax/spec/list.mcrl2"),
+            ComplexSort::Set => include_str!("../../syntax/spec/set.mcrl2"),
+            ComplexSort::FSet => include_str!("../../syntax/spec/fset.mcrl2"),
+            ComplexSort::Bag => include_str!("../../syntax/spec/bag.mcrl2"),
+            ComplexSort::FBag => include_str!("../../syntax/spec/fbag.mcrl2"),
+        };
+
+        let spec = UntypedDataSpecification::parse(text)?;
+
+        Ok(replace_sort(&spec, "S", sort))
+    } else if let SortExpression::Function { domain, range } = sort {
+        let text = include_str!("../../syntax/spec/function_update.mcrl2");
+
+        let spec = UntypedDataSpecification::parse(text)?;
+
+        // In the specification we define the function S -> T.
+        let spec = replace_sort(&spec, "S", domain);
+        let spec = replace_sort(&spec, "T", range);
+
+        Ok(spec)
+    } else {
+        unreachable!("The given sort {} is not a standard sort", sort);
+    }
+}
+
+/// Replaces the given identifier by the given sort expression in the given data
+/// specification.
+///
+/// # Details
+///
+/// This function can be used to instantiate polymorphic types, for example,
+/// replacing identifier `S` in the specification for `List(S)` by `Nat` to get
+/// a specification for `List(Nat)`.
+fn replace_sort(spec: &UntypedDataSpecification, identifier: &str, sort: &SortExpression) -> UntypedDataSpecification {
+    let mut result = spec.clone();
+
+    for constructor in &mut result.constructor_declarations {
+        constructor.sort = replace_sort_expression(&constructor.sort, identifier, sort);
+    }
+
+    for map in &mut result.map_declarations {
+        map.sort = replace_sort_expression(&map.sort, identifier, sort);
+    }
+
+    for equation in &mut result.equation_declarations {
+        for var in &mut equation.variables {
+            var.sort = replace_sort_expression(&var.sort, identifier, sort);
+        }
+    }
+
+    result
+}
+
+/// Replaces sort references of `identifier` in `sort` by the given `result_sort`.
+fn replace_sort_expression(sort: &SortExpression, identifier: &str, result_sort: &SortExpression) -> SortExpression {
+    apply_sort_expression(sort.clone(), |expr| -> Result<Option<SortExpression>, Infallible> {
+        if let SortExpression::Reference(id) = expr {
+            if id == identifier {
+                return Ok(Some(result_sort.clone()));
+            }
+        }
+
+        Ok(None)
+    })
+    .unwrap()
+}
+
+/// Generate a data specification for any sort based on the rules in Appendix `B`.
+pub fn basic_spec(sort: &str) -> Result<UntypedDataSpecification, MercError> {
+    Ok(UntypedDataSpecification::parse(&formatdoc! {"
+        map ==, !=, <, <=, >=, >: {sort} # {sort} -> Bool;
+            if: Bool # {sort} # {sort} -> {sort};
+
+        var x, y: {sort};
+            b: Bool;
+
+        eqm x == x = true;
+            x != y = !(x == y);
+            if(true, x, y)  = x;
+            if(false, x, y) = y;
+            if(b, x, y)      = if (b, x, y);
+            if(x == y, x, y) = y;
+            x < x  = false;
+            x <= x = true;
+            x > y  = y < x;
+            x >= y = y <= x;
+    "})?)
+}
+
+/// Generates a data specification for a structured sort, the rules are given in Appendix `B.10`.
+pub fn structured_sort_spec(
+    name: &str,
+    structured_sort: &SortExpression,
+) -> Result<UntypedDataSpecification, MercError> {
+    if let SortExpression::Struct { inner: _ } = structured_sort {
+        let name = format!("Struct{}", name);
+
+        let spec = formatdoc!(
+            "sort {name}
+        
+        "
+        );
+
+        UntypedDataSpecification::parse(&spec)
+    } else {
+        unreachable!("structured_sort_spec should only be called on structured sorts");
+    }
+}
diff --git a/crates/unsafety/src/protection_set.rs b/crates/unsafety/src/protection_set.rs
index ba0d5203c..024a985a1 100644
--- a/crates/unsafety/src/protection_set.rs
+++ b/crates/unsafety/src/protection_set.rs
@@ -310,8 +310,8 @@ mod tests {
     use merc_utilities::random_test;
     use merc_utilities::test_logger;
 
-    use crate::ProtectionIndex;
-    use crate::ProtectionSet;
+    use super::ProtectionIndex;
+    use super::ProtectionSet;
 
     #[test]
     #[cfg_attr(miri, ignore)]