30 files changed, 1508 insertions, 282 deletions

diff --git a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
index 43351d3e..08f7a585 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/subprojects/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -17,7 +17,8 @@ enum ModuleKind:
 
 Statement:
         ImportStatement | Assertion | ClassDeclaration | EnumDeclaration |
-        DatatypeDeclaration | PredicateDefinition | /* FunctionDefinition | RuleDefinition | */
+        DatatypeDeclaration | AggregatorDeclaration | PredicateDefinition |
+        /* FunctionDefinition | RuleDefinition | */
         ScopeDeclaration | NodeDeclaration;
 
 ImportStatement:
@@ -40,6 +41,9 @@ EnumLiteral returns Node:
 DatatypeDeclaration:
         "extern" "datatype" name=Identifier ".";
 
+AggregatorDeclaration:
+        "extern" "aggregator" name=Identifier ".";
+
 enum ReferenceKind:
         REFERENCE="refers" | CONTAINMENT="contains" | CONTAINER="container";
 
@@ -71,7 +75,6 @@ Conjunction:
 //
 //Case:
 //      Conjunction ({Match.condition=current} "->" value=Expr)?;
-
 //RuleDefinition:
 //      "rule"
 //      name=Identifier
@@ -106,11 +109,18 @@ Expr:
         AssignmentExpr;
 
 AssignmentExpr returns Expr:
-        ComparisonExpr ({AssignmentExpr.left=current}"is" right=ComparisonExpr)*;
+        BooleanExpr ({AssignmentExpr.left=current} "is" right=BooleanExpr)*;
+
+enum BooleanBinaryOp returns BinaryOp:
+        AND="&&" | OR="||" | XOR="^^";
+
+BooleanExpr returns Expr:
+        ComparisonExpr ({ArithmeticBinaryExpr.left=current}
+        op=BooleanBinaryOp right=ComparisonExpr)*;
 
 enum ComparisonOp:
-        LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="==" | NOT_EQ="!=" |
-        IN="in" | SUBSUMES=":>" | SUBSUMED_BY="<:" | ABS_EQ="===" | ABS_NOT_EQ="!==";
+        LESS="<" | LESS_EQ="<=" | GREATER=">" | GREATER_EQ=">=" | EQ="===" | NOT_EQ="!==" |
+        IN="in" | NODE_EQ="==" | NODE_NOT_EQ="!=";
 
 ComparisonExpr returns Expr:
         LatticeExpr ({ComparisonExpr.left=current}
@@ -120,12 +130,8 @@ enum LatticeBinaryOp:
         MEET="/\\" | JOIN="\\/";
 
 LatticeExpr returns Expr:
-        RangeExpr ({LatticeBinaryExpr.left=current}
-        op=LatticeBinaryOp right=RangeExpr)*;
-
-RangeExpr returns Expr:
-        AdditiveExpr ({RangeExpr.left=current} ".." ("*" | right=AdditiveExpr))* |
-        {RangeExpr} "*" ".." ("*" | right=AdditiveExpr);
+        AdditiveExpr ({LatticeBinaryExpr.left=current}
+        op=LatticeBinaryOp right=AdditiveExpr)*;
 
 enum AdditiveOp returns BinaryOp:
         ADD="+" | SUB="-";
@@ -145,11 +151,14 @@ enum ExponentialOp returns BinaryOp:
         POW="**";
 
 ExponentialExpr returns Expr:
-        UnaryExpr ({ArithmeticBinaryExpr.left=current}
+        RangeExpr ({ArithmeticBinaryExpr.left=current}
         op=ExponentialOp right=ExponentialExpr)?;
 
+RangeExpr returns Expr:
+        UnaryExpr ({RangeExpr.left=current} ".." right=UnaryExpr)*;
+
 UnaryExpr returns Expr:
-        ArithmeticUnaryExpr | ModalExpr | NegationExpr |
+        ArithmeticUnaryExpr | NegationExpr |
         CountExpr | AggregationExpr | CastExpr;
 
 enum UnaryOp:
@@ -158,23 +167,15 @@ enum UnaryOp:
 ArithmeticUnaryExpr:
         op=UnaryOp body=UnaryExpr;
 
-enum Modality:
-        MAY="may" | MUST="must" | CURRENT="current";
-
-ModalExpr:
-        modality=Modality body=UnaryExpr;
-
 NegationExpr:
         "!" body=UnaryExpr;
 
 CountExpr:
         "count" body=UnaryExpr;
 
-enum AggregationOp:
-        SUM="sum" | PROD="prod" | MIN="min" | MAX="max";
-
 AggregationExpr:
-        op=AggregationOp "{" value=Expr "|" condition=ComparisonExpr "}";
+        aggregator=[AggregatorDeclaration|QualifiedName]
+        "{" value=Expr "|" condition=ComparisonExpr "}";
 
 CastExpr returns Expr:
         CastExprBody ({CastExpr.body=current} "as" targetType=[Relation|QualifiedName])?;
@@ -191,7 +192,7 @@ VariableOrNodeExpr:
         variableOrNode=[VariableOrNode|QualifiedName];
 
 Constant:
-        RealConstant | IntConstant | StringConstant | LogicConstant;
+        RealConstant | IntConstant | StringConstant | InfiniteConstant | LogicConstant;
 
 IntConstant:
         intValue=INT;
@@ -202,6 +203,9 @@ RealConstant:
 StringConstant:
         stringValue=STRING;
 
+InfiniteConstant:
+        {InfiniteConstant} "*";
+
 enum LogicValue:
         TRUE="true" | FALSE="false" | UNKNOWN="unknown" | ERROR="error";
 
@@ -276,8 +280,8 @@ Identifier:
         NonContainmentIdentifier | "contains" | "container";
 
 NonContainmentIdentifier:
-        ID | "atom" | "multi" | "contained" |
-        "sum" | "prod" | "min" | "max" | "problem" | "module";
+        ID | "atom" | "multi" | "contained" | "problem" | "module" |
+        "datatype" | "aggregator";
 
 Real returns ecore::EDouble:
         EXPONENTIAL | INT "." (INT | EXPONENTIAL);
diff --git a/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java b/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java
index f7039027..955a89f9 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/ProblemRuntimeModule.java
@@ -30,9 +30,8 @@ import org.eclipse.xtext.validation.IResourceValidator;
 import org.eclipse.xtext.xbase.annotations.validation.DerivedStateAwareResourceValidator;
 import tools.refinery.language.conversion.ProblemValueConverterService;
 import tools.refinery.language.linking.ProblemLinkingService;
-import tools.refinery.language.naming.ProblemDelegateQualifiedNameProvider;
-import tools.refinery.language.naming.ProblemQualifiedNameConverter;
 import tools.refinery.language.naming.ProblemQualifiedNameProvider;
+import tools.refinery.language.naming.ProblemQualifiedNameConverter;
 import tools.refinery.language.parser.ProblemEcoreElementFactory;
 import tools.refinery.language.parser.antlr.TokenSourceInjectingProblemParser;
 import tools.refinery.language.resource.ProblemLocationInFileProvider;
@@ -68,12 +67,6 @@ public class ProblemRuntimeModule extends AbstractProblemRuntimeModule {
                 return ProblemQualifiedNameConverter.class;
         }
 
-        public void configureIQualifiedNameProviderDelegate(Binder binder) {
-                binder.bind(IQualifiedNameProvider.class)
-                                .annotatedWith(Names.named(ProblemQualifiedNameProvider.NAMED_DELEGATE))
-                                .to(ProblemDelegateQualifiedNameProvider.class);
-        }
-
         @Override
         public Class<? extends IQualifiedNameProvider> bindIQualifiedNameProvider() {
                 return ProblemQualifiedNameProvider.class;
diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/AbstractTermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/AbstractTermInterpreter.java
new file mode 100644
index 00000000..2530b707
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/AbstractTermInterpreter.java
@@ -0,0 +1,131 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.expressions;
+
+import tools.refinery.language.model.problem.BinaryOp;
+import tools.refinery.language.model.problem.UnaryOp;
+import tools.refinery.language.typesystem.AggregatorName;
+import tools.refinery.language.typesystem.DataExprType;
+
+import java.util.*;
+
+// This class is used to configure term interpreters by clients with various arguments.
+@SuppressWarnings("SameParameterValue")
+public abstract class AbstractTermInterpreter implements TermInterpreter {
+        private final Map<DataExprType, DataExprType> negations = new HashMap<>();
+        private final Map<UnaryKey, DataExprType> unaryOperators = new HashMap<>();
+        private final Set<DataExprType> comparisons = new HashSet<>();
+        private final Set<DataExprType> ranges = new HashSet<>();
+        private final Map<BinaryKey, DataExprType> binaryOperators = new HashMap<>();
+        private final Set<CastKey> casts = new HashSet<>();
+        private final Map<AggregatorKey, DataExprType> aggregators = new HashMap<>();
+
+        protected AbstractTermInterpreter() {
+        }
+
+        protected void addNegation(DataExprType type, DataExprType result) {
+                negations.put(type, result);
+        }
+
+        protected void addNegation(DataExprType type) {
+                addNegation(type, type);
+        }
+
+        protected void addUnaryOperator(UnaryOp op, DataExprType type, DataExprType result) {
+                unaryOperators.put(new UnaryKey(op, type), result);
+        }
+
+        protected void addUnaryOperator(UnaryOp op, DataExprType type) {
+                addUnaryOperator(op, type, type);
+        }
+
+        protected void addComparison(DataExprType type) {
+                comparisons.add(type);
+        }
+
+        protected void addRange(DataExprType type) {
+                ranges.add(type);
+        }
+
+        protected void addBinaryOperator(BinaryOp op, DataExprType leftType, DataExprType rightType, DataExprType result) {
+                binaryOperators.put(new BinaryKey(op, leftType, rightType), result);
+        }
+
+        protected void addBinaryOperator(BinaryOp op, DataExprType type) {
+                addBinaryOperator(op, type, type, type);
+        }
+
+        protected void addCast(DataExprType fromType, DataExprType toType) {
+                if (fromType.equals(toType)) {
+                        throw new IllegalArgumentException("The fromType and toType of a cast operator must be different");
+                }
+                casts.add(new CastKey(fromType, toType));
+        }
+
+        protected void addAggregator(AggregatorName aggregator, DataExprType type, DataExprType result) {
+                aggregators.put(new AggregatorKey(aggregator, type), result);
+        }
+
+        protected void addAggregator(AggregatorName aggregator, DataExprType type) {
+                addAggregator(aggregator, type, type);
+        }
+
+        @Override
+        public Optional<DataExprType> getNegationType(DataExprType type) {
+                return Optional.ofNullable(negations.get(type));
+        }
+
+        @Override
+        public Optional<DataExprType> getUnaryOperationType(UnaryOp op, DataExprType type) {
+                if (unaryOperators.isEmpty()) {
+                        return Optional.empty();
+                }
+                return Optional.ofNullable(unaryOperators.get(new UnaryKey(op, type)));
+        }
+
+        @Override
+        public boolean isComparisonSupported(DataExprType type) {
+                return comparisons.contains(type);
+        }
+
+        @Override
+        public boolean isRangeSupported(DataExprType type) {
+                return ranges.contains(type);
+        }
+
+        @Override
+        public Optional<DataExprType> getBinaryOperationType(BinaryOp op, DataExprType leftType, DataExprType rightType) {
+                if (binaryOperators.isEmpty()) {
+                        return Optional.empty();
+                }
+                return Optional.ofNullable(binaryOperators.get(new BinaryKey(op, leftType, rightType)));
+        }
+
+        @Override
+        public Optional<DataExprType> getAggregationType(AggregatorName aggregator, DataExprType type) {
+                if (aggregators.isEmpty()) {
+                        return Optional.empty();
+                }
+                return Optional.ofNullable(aggregators.get(new AggregatorKey(aggregator, type)));
+        }
+
+        @Override
+        public boolean isCastSupported(DataExprType fromType, DataExprType toType) {
+                return casts.contains(new CastKey(fromType, toType));
+        }
+
+        private record UnaryKey(UnaryOp op, DataExprType type) {
+        }
+
+        private record BinaryKey(BinaryOp op, DataExprType leftType, DataExprType rightType) {
+        }
+
+        private record CastKey(DataExprType fromType, DataExprType toType) {
+        }
+
+        private record AggregatorKey(AggregatorName aggregator, DataExprType type) {
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/BuiltinTermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/BuiltinTermInterpreter.java
new file mode 100644
index 00000000..412ed8ba
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/BuiltinTermInterpreter.java
@@ -0,0 +1,54 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.expressions;
+
+import tools.refinery.language.library.BuiltinLibrary;
+import tools.refinery.language.model.problem.BinaryOp;
+import tools.refinery.language.model.problem.UnaryOp;
+import tools.refinery.language.typesystem.AggregatorName;
+import tools.refinery.language.typesystem.DataExprType;
+
+public final class BuiltinTermInterpreter extends AbstractTermInterpreter {
+        public static final DataExprType BOOLEAN_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "boolean");
+        public static final DataExprType INT_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "int");
+        public static final DataExprType REAL_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "real");
+        public static final DataExprType STRING_TYPE = new DataExprType(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "string");
+        public static final AggregatorName MIN_AGGREGATOR = new AggregatorName(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "min");
+        public static final AggregatorName MAX_AGGREGATOR = new AggregatorName(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "max");
+        public static final AggregatorName SUM_AGGREGATOR = new AggregatorName(BuiltinLibrary.BUILTIN_LIBRARY_NAME, "sum");
+
+        public BuiltinTermInterpreter() {
+                addNegation(BOOLEAN_TYPE);
+                addBinaryOperator(BinaryOp.AND, BOOLEAN_TYPE);
+                addBinaryOperator(BinaryOp.OR, BOOLEAN_TYPE);
+                addBinaryOperator(BinaryOp.XOR, BOOLEAN_TYPE);
+
+                addUnaryOperator(UnaryOp.PLUS, INT_TYPE);
+                addUnaryOperator(UnaryOp.MINUS, INT_TYPE);
+                addComparison(INT_TYPE);
+                addRange(INT_TYPE);
+                addBinaryOperator(BinaryOp.ADD, INT_TYPE);
+                addBinaryOperator(BinaryOp.SUB, INT_TYPE);
+                addBinaryOperator(BinaryOp.MUL, INT_TYPE);
+                addAggregator(MIN_AGGREGATOR, INT_TYPE);
+                addAggregator(MAX_AGGREGATOR, INT_TYPE);
+                addAggregator(SUM_AGGREGATOR, INT_TYPE);
+
+                addUnaryOperator(UnaryOp.PLUS, REAL_TYPE);
+                addUnaryOperator(UnaryOp.MINUS, REAL_TYPE);
+                addCast(INT_TYPE, REAL_TYPE);
+                addComparison(REAL_TYPE);
+                addRange(REAL_TYPE);
+                addBinaryOperator(BinaryOp.ADD, REAL_TYPE);
+                addBinaryOperator(BinaryOp.SUB, REAL_TYPE);
+                addBinaryOperator(BinaryOp.MUL, REAL_TYPE);
+                addBinaryOperator(BinaryOp.DIV, REAL_TYPE);
+                addBinaryOperator(BinaryOp.POW, REAL_TYPE);
+                addAggregator(MIN_AGGREGATOR, REAL_TYPE);
+                addAggregator(MAX_AGGREGATOR, REAL_TYPE);
+                addAggregator(SUM_AGGREGATOR, REAL_TYPE);
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/CompositeTermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/CompositeTermInterpreter.java
new file mode 100644
index 00000000..b337e5dd
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/CompositeTermInterpreter.java
@@ -0,0 +1,99 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.expressions;
+
+import tools.refinery.language.model.problem.BinaryOp;
+import tools.refinery.language.model.problem.UnaryOp;
+import tools.refinery.language.typesystem.AggregatorName;
+import tools.refinery.language.typesystem.DataExprType;
+
+import java.util.List;
+import java.util.Optional;
+
+public class CompositeTermInterpreter implements TermInterpreter {
+        private final List<TermInterpreter> interpreters;
+
+    public CompositeTermInterpreter(List<TermInterpreter> interpreters) {
+        this.interpreters = interpreters;
+    }
+
+        @Override
+        public Optional<DataExprType> getNegationType(DataExprType type) {
+                for (var interpreter : interpreters) {
+                        var result = interpreter.getNegationType(type);
+                        if (result.isPresent()) {
+                                return result;
+                        }
+                }
+                return Optional.empty();
+        }
+
+        @Override
+        public Optional<DataExprType> getUnaryOperationType(UnaryOp op, DataExprType type) {
+                for (var interpreter : interpreters) {
+                        var result = interpreter.getUnaryOperationType(op, type);
+                        if (result.isPresent()) {
+                                return result;
+                        }
+                }
+                return Optional.empty();
+        }
+
+        @Override
+        public boolean isComparisonSupported(DataExprType type) {
+                for (var interpreter : interpreters) {
+                        var result = interpreter.isComparisonSupported(type);
+                        if (result) {
+                                return true;
+                        }
+                }
+                return false;
+        }
+
+        @Override
+        public boolean isRangeSupported(DataExprType type) {
+                for (var interpreter : interpreters) {
+                        var result = interpreter.isRangeSupported(type);
+                        if (result) {
+                                return true;
+                        }
+                }
+                return false;
+        }
+
+        @Override
+        public Optional<DataExprType> getBinaryOperationType(BinaryOp op, DataExprType leftType, DataExprType rightType) {
+                for (var interpreter : interpreters) {
+                        var result = interpreter.getBinaryOperationType(op, leftType, rightType);
+                        if (result.isPresent()) {
+                                return result;
+                        }
+                }
+                return Optional.empty();
+        }
+
+        @Override
+        public boolean isCastSupported(DataExprType fromType, DataExprType toType) {
+                for (var interpreter : interpreters) {
+                        var result = interpreter.isCastSupported(fromType, toType);
+                        if (result) {
+                                return true;
+                        }
+                }
+                return false;
+        }
+
+        @Override
+        public Optional<DataExprType> getAggregationType(AggregatorName aggregator, DataExprType type) {
+                for (var interpreter : interpreters) {
+                        var result = interpreter.getAggregationType(aggregator, type);
+                        if (result.isPresent()) {
+                                return result;
+                        }
+                }
+                return Optional.empty();
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/expressions/TermInterpreter.java b/subprojects/language/src/main/java/tools/refinery/language/expressions/TermInterpreter.java
new file mode 100644
index 00000000..122785f2
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/expressions/TermInterpreter.java
@@ -0,0 +1,29 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.expressions;
+
+import tools.refinery.language.model.problem.BinaryOp;
+import tools.refinery.language.model.problem.UnaryOp;
+import tools.refinery.language.typesystem.AggregatorName;
+import tools.refinery.language.typesystem.DataExprType;
+
+import java.util.Optional;
+
+public interface TermInterpreter {
+        Optional<DataExprType> getNegationType(DataExprType type);
+
+        Optional<DataExprType> getUnaryOperationType(UnaryOp op, DataExprType type);
+
+        boolean isComparisonSupported(DataExprType type);
+
+        boolean isRangeSupported(DataExprType type);
+
+        Optional<DataExprType> getBinaryOperationType(BinaryOp op, DataExprType leftType, DataExprType rightType);
+
+        boolean isCastSupported(DataExprType fromType, DataExprType toType);
+
+        Optional<DataExprType> getAggregationType(AggregatorName aggregator, DataExprType type);
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemDelegateQualifiedNameProvider.java b/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemDelegateQualifiedNameProvider.java
deleted file mode 100644
index b3931401..00000000
--- a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemDelegateQualifiedNameProvider.java
+++ /dev/null
@@ -1,44 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.language.naming;
-
-import com.google.inject.Inject;
-import org.eclipse.xtext.naming.DefaultDeclarativeQualifiedNameProvider;
-import org.eclipse.xtext.naming.IQualifiedNameConverter;
-import org.eclipse.xtext.naming.QualifiedName;
-import tools.refinery.language.model.problem.Problem;
-import tools.refinery.language.scoping.imports.ImportAdapter;
-import tools.refinery.language.utils.ProblemUtil;
-
-public class ProblemDelegateQualifiedNameProvider extends DefaultDeclarativeQualifiedNameProvider {
-        @Inject
-        private IQualifiedNameConverter qualifiedNameConverter;
-
-        protected QualifiedName qualifiedName(Problem problem) {
-                var qualifiedNameString = problem.getName();
-                if (qualifiedNameString != null) {
-                        return NamingUtil.stripRootPrefix(qualifiedNameConverter.toQualifiedName(qualifiedNameString));
-                }
-                if (!ProblemUtil.isModule(problem)) {
-                        return null;
-                }
-                var resource = problem.eResource();
-                if (resource == null) {
-                        return null;
-                }
-                var resourceUri = resource.getURI();
-                if (resourceUri == null) {
-                        return null;
-                }
-                var resourceSet = resource.getResourceSet();
-                if (resourceSet == null) {
-                        return null;
-                }
-                var adapter = ImportAdapter.getOrInstall(resourceSet);
-                // If a module has no explicitly specified name, return the qualified name it was resolved under.
-                return adapter.getQualifiedName(resourceUri);
-        }
-}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java b/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java
index 5b682058..2a4df4d0 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/naming/ProblemQualifiedNameProvider.java
@@ -6,36 +6,44 @@
 package tools.refinery.language.naming;
 
 import com.google.inject.Inject;
-import com.google.inject.name.Named;
-import org.eclipse.emf.ecore.EObject;
-import org.eclipse.xtext.naming.IQualifiedNameProvider;
+import com.google.inject.Singleton;
+import org.eclipse.xtext.naming.DefaultDeclarativeQualifiedNameProvider;
+import org.eclipse.xtext.naming.IQualifiedNameConverter;
 import org.eclipse.xtext.naming.QualifiedName;
-import org.eclipse.xtext.util.IResourceScopeCache;
-import org.eclipse.xtext.util.Tuples;
-import tools.refinery.language.resource.ProblemResourceDescriptionStrategy;
-
-public class ProblemQualifiedNameProvider extends IQualifiedNameProvider.AbstractImpl {
-        private static final String PREFIX = "tools.refinery.language.naming.ProblemQualifiedNameProvider.";
-        public static final String NAMED_DELEGATE = PREFIX + "NAMED_DELEGATE";
-        public static final String CACHE_KEY = PREFIX + "CACHE_KEY";
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.scoping.imports.ImportAdapterProvider;
+import tools.refinery.language.utils.ProblemUtil;
 
+@Singleton
+public class ProblemQualifiedNameProvider extends DefaultDeclarativeQualifiedNameProvider {
         @Inject
-        @Named(NAMED_DELEGATE)
-        private IQualifiedNameProvider delegate;
+        private IQualifiedNameConverter qualifiedNameConverter;
 
         @Inject
-        private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE;
-
-        @Override
-        public QualifiedName getFullyQualifiedName(EObject obj) {
-                return cache.get(Tuples.pair(obj, CACHE_KEY), obj.eResource(), () -> computeFullyQualifiedName(obj));
-        }
+        private ImportAdapterProvider importAdapterProvider;
 
-        public QualifiedName computeFullyQualifiedName(EObject obj) {
-                var qualifiedName = delegate.getFullyQualifiedName(obj);
-                if (qualifiedName != null && ProblemResourceDescriptionStrategy.shouldExport(obj)) {
-                        return NamingUtil.addRootPrefix(qualifiedName);
+        protected QualifiedName qualifiedName(Problem problem) {
+                var qualifiedNameString = problem.getName();
+                if (qualifiedNameString != null) {
+                        return NamingUtil.stripRootPrefix(qualifiedNameConverter.toQualifiedName(qualifiedNameString));
+                }
+                if (!ProblemUtil.isModule(problem)) {
+                        return null;
+                }
+                var resource = problem.eResource();
+                if (resource == null) {
+                        return null;
+                }
+                var resourceUri = resource.getURI();
+                if (resourceUri == null) {
+                        return null;
+                }
+                var resourceSet = resource.getResourceSet();
+                if (resourceSet == null) {
+                        return null;
                 }
-                return qualifiedName;
+                var adapter = importAdapterProvider.getOrInstall(resourceSet);
+                // If a module has no explicitly specified name, return the qualified name it was resolved under.
+                return adapter.getQualifiedName(resourceUri);
         }
 }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java
index 3dcf6b1f..8fd60364 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/resource/ProblemResourceDescriptionStrategy.java
@@ -8,7 +8,6 @@ package tools.refinery.language.resource;
 import com.google.common.collect.ImmutableMap;
 import com.google.inject.Inject;
 import com.google.inject.Singleton;
-import com.google.inject.name.Named;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.xtext.EcoreUtil2;
 import org.eclipse.xtext.naming.IQualifiedNameConverter;
@@ -19,10 +18,9 @@ import org.eclipse.xtext.resource.IEObjectDescription;
 import org.eclipse.xtext.resource.impl.DefaultResourceDescriptionStrategy;
 import org.eclipse.xtext.util.IAcceptor;
 import tools.refinery.language.documentation.DocumentationCommentParser;
-import tools.refinery.language.naming.ProblemQualifiedNameProvider;
-import tools.refinery.language.scoping.imports.ImportCollector;
 import tools.refinery.language.model.problem.*;
 import tools.refinery.language.naming.NamingUtil;
+import tools.refinery.language.scoping.imports.ImportCollector;
 import tools.refinery.language.utils.ProblemUtil;
 
 import java.util.Map;
@@ -32,13 +30,15 @@ import java.util.stream.Collectors;
 public class ProblemResourceDescriptionStrategy extends DefaultResourceDescriptionStrategy {
         private static final String DATA_PREFIX = "tools.refinery.language.resource.ProblemResourceDescriptionStrategy.";
 
-        public static final String ARITY = DATA_PREFIX + "ARITY";
+        public static final String TYPE_LIKE = DATA_PREFIX + "ARITY";
+        public static final String TYPE_LIKE_TRUE = "true";
         public static final String ERROR_PREDICATE = DATA_PREFIX + "ERROR_PREDICATE";
         public static final String ERROR_PREDICATE_TRUE = "true";
         public static final String SHADOWING_KEY = DATA_PREFIX + "SHADOWING_KEY";
         public static final String SHADOWING_KEY_PROBLEM = "problem";
         public static final String SHADOWING_KEY_NODE = "node";
         public static final String SHADOWING_KEY_RELATION = "relation";
+        public static final String SHADOWING_KEY_AGGREGATOR = "aggregator";
         public static final String PREFERRED_NAME = DATA_PREFIX + "PREFERRED_NAME";
         public static final String PREFERRED_NAME_TRUE = "true";
         public static final String IMPORTS = DATA_PREFIX + "IMPORTS";
@@ -51,8 +51,7 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti
         private IQualifiedNameConverter qualifiedNameConverter;
 
         @Inject
-        @Named(ProblemQualifiedNameProvider.NAMED_DELEGATE)
-        private IQualifiedNameProvider delegateQualifiedNameProvider;
+        private IQualifiedNameProvider qualifiedNameProvider;
 
         @Inject
         private ImportCollector importCollector;
@@ -123,7 +122,7 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti
                 if (problem == null) {
                         return QualifiedName.EMPTY;
                 }
-                var qualifiedName = delegateQualifiedNameProvider.getFullyQualifiedName(problem);
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(problem);
         return qualifiedName == null ? QualifiedName.EMPTY : qualifiedName;
     }
 
@@ -152,8 +151,11 @@ public class ProblemResourceDescriptionStrategy extends DefaultResourceDescripti
                         builder.put(SHADOWING_KEY, SHADOWING_KEY_NODE);
                 } else if (eObject instanceof Relation relation) {
                         builder.put(SHADOWING_KEY, SHADOWING_KEY_RELATION);
-                        int arity = ProblemUtil.getArity(relation);
-                        builder.put(ARITY, Integer.toString(arity));
+                        if (ProblemUtil.isTypeLike(relation)) {
+                                builder.put(TYPE_LIKE, TYPE_LIKE_TRUE);
+                        }
+                } else if (eObject instanceof AggregatorDeclaration) {
+                        builder.put(SHADOWING_KEY, SHADOWING_KEY_AGGREGATOR);
                 }
                 if (eObject instanceof PredicateDefinition predicateDefinition && predicateDefinition.isError()) {
                         builder.put(ERROR_PREDICATE, ERROR_PREDICATE_TRUE);
diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java
index 0067bf94..3b94423a 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemLocalScopeProvider.java
@@ -6,7 +6,6 @@
 package tools.refinery.language.scoping;
 
 import com.google.inject.Inject;
-import com.google.inject.name.Named;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.EReference;
 import org.eclipse.emf.ecore.resource.Resource;
@@ -17,14 +16,12 @@ import org.eclipse.xtext.resource.ISelectable;
 import org.eclipse.xtext.scoping.IScope;
 import org.eclipse.xtext.scoping.impl.AbstractGlobalScopeDelegatingScopeProvider;
 import org.eclipse.xtext.util.IResourceScopeCache;
-import tools.refinery.language.naming.ProblemQualifiedNameProvider;
 
 public class ProblemLocalScopeProvider extends AbstractGlobalScopeDelegatingScopeProvider {
         private static final String CACHE_KEY = "tools.refinery.language.scoping.ProblemLocalScopeProvider.CACHE_KEY";
 
         @Inject
-        @Named(ProblemQualifiedNameProvider.NAMED_DELEGATE)
-        private IQualifiedNameProvider delegateQualifiedNameProvider;
+        private IQualifiedNameProvider qualifiedNameProvider;
 
         @Inject
         private IResourceDescriptionsProvider resourceDescriptionsProvider;
@@ -59,7 +56,7 @@ public class ProblemLocalScopeProvider extends AbstractGlobalScopeDelegatingScop
                 if (rootElement == null) {
                         return new NoFullyQualifiedNamesSelectable(resourceDescription);
                 }
-                var rootName = delegateQualifiedNameProvider.getFullyQualifiedName(rootElement);
+                var rootName = qualifiedNameProvider.getFullyQualifiedName(rootElement);
                 if (rootName == null) {
                         return new NoFullyQualifiedNamesSelectable(resourceDescription);
                 }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java
index f83a7ebd..d94c9a13 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/ProblemScopeProvider.java
@@ -9,14 +9,12 @@
  */
 package tools.refinery.language.scoping;
 
-import com.google.inject.Inject;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.EReference;
 import org.eclipse.xtext.EcoreUtil2;
 import org.eclipse.xtext.scoping.IScope;
 import org.eclipse.xtext.scoping.Scopes;
 import tools.refinery.language.model.problem.*;
-import tools.refinery.language.utils.ProblemDesugarer;
 
 import java.util.Collection;
 import java.util.LinkedHashSet;
@@ -29,9 +27,6 @@ import java.util.LinkedHashSet;
  * on how and when to use it.
  */
 public class ProblemScopeProvider extends AbstractProblemScopeProvider {
-        @Inject
-        private ProblemDesugarer desugarer;
-
         @Override
         public IScope getScope(EObject context, EReference reference) {
                 var scope = super.getScope(context, reference);
diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java
index d7a5304f..753c8565 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapter.java
@@ -16,7 +16,12 @@ import org.eclipse.emf.ecore.resource.Resource;
 import org.eclipse.emf.ecore.resource.ResourceSet;
 import org.eclipse.emf.ecore.util.EcoreUtil;
 import org.eclipse.xtext.naming.QualifiedName;
+import tools.refinery.language.expressions.CompositeTermInterpreter;
+import tools.refinery.language.expressions.TermInterpreter;
+import tools.refinery.language.library.BuiltinLibrary;
 import tools.refinery.language.library.RefineryLibrary;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.utils.BuiltinSymbols;
 
 import java.io.File;
 import java.nio.file.Path;
@@ -25,15 +30,12 @@ import java.util.*;
 public class ImportAdapter extends AdapterImpl {
         private static final Logger LOG = Logger.getLogger(ImportAdapter.class);
         private static final List<RefineryLibrary> DEFAULT_LIBRARIES;
+        private static final List<TermInterpreter> DEFAULT_TERM_INTERPRETERS;
         private static final List<Path> DEFAULT_PATHS;
 
         static {
-                var serviceLoader = ServiceLoader.load(RefineryLibrary.class);
-                var defaultLibraries = new ArrayList<RefineryLibrary>();
-                for (var service : serviceLoader) {
-                        defaultLibraries.add(service);
-                }
-                DEFAULT_LIBRARIES = List.copyOf(defaultLibraries);
+                DEFAULT_LIBRARIES = loadServices(RefineryLibrary.class);
+                DEFAULT_TERM_INTERPRETERS = loadServices(TermInterpreter.class);
                 var pathEnv = System.getenv("REFINERY_LIBRARY_PATH");
                 if (pathEnv == null) {
                         DEFAULT_PATHS = List.of();
@@ -45,16 +47,29 @@ public class ImportAdapter extends AdapterImpl {
                 }
         }
 
-        private final List<RefineryLibrary> libraries;
-        private final List<Path> libraryPaths;
+        private static <T> List<T> loadServices(Class<T> serviceClass) {
+                var serviceLoader = ServiceLoader.load(serviceClass);
+                var services = new ArrayList<T>();
+                for (var service : serviceLoader) {
+                        services.add(service);
+                }
+                return List.copyOf(services);
+        }
+
+        private ResourceSet resourceSet;
+        private final List<RefineryLibrary> libraries = new ArrayList<>(DEFAULT_LIBRARIES);
+        private final List<TermInterpreter> termInterpreters = new ArrayList<>(DEFAULT_TERM_INTERPRETERS);
+        private final TermInterpreter termInterpreter = new CompositeTermInterpreter(termInterpreters);
+        private final List<Path> libraryPaths = new ArrayList<>(DEFAULT_PATHS);
         private final Cache<QualifiedName, QualifiedName> failedResolutions =
                         CacheBuilder.newBuilder().maximumSize(100).build();
         private final Map<QualifiedName, URI> qualifiedNameToUriMap = new LinkedHashMap<>();
         private final Map<URI, QualifiedName> uriToQualifiedNameMap = new LinkedHashMap<>();
+        private Problem builtinProblem;
+        private BuiltinSymbols builtinSymbols;
 
-        private ImportAdapter(ResourceSet resourceSet) {
-                libraries = new ArrayList<>(DEFAULT_LIBRARIES);
-                libraryPaths = new ArrayList<>(DEFAULT_PATHS);
+        void setResourceSet(ResourceSet resourceSet) {
+                this.resourceSet = resourceSet;
                 for (var resource : resourceSet.getResources()) {
                         resourceAdded(resource);
                 }
@@ -69,6 +84,14 @@ public class ImportAdapter extends AdapterImpl {
                 return libraries;
         }
 
+        public List<TermInterpreter> getTermInterpreters() {
+                return termInterpreters;
+        }
+
+        public TermInterpreter getTermInterpreter() {
+                return termInterpreter;
+        }
+
         public List<Path> getLibraryPaths() {
                 return libraryPaths;
         }
@@ -190,16 +213,26 @@ public class ImportAdapter extends AdapterImpl {
                 }
         }
 
-        public static ImportAdapter getOrInstall(ResourceSet resourceSet) {
-                var adapter = getAdapter(resourceSet);
-                if (adapter == null) {
-                        adapter = new ImportAdapter(resourceSet);
-                        resourceSet.eAdapters().add(adapter);
+        public Problem getBuiltinProblem() {
+                if (builtinProblem == null) {
+                        var builtinResource = resourceSet.getResource(BuiltinLibrary.BUILTIN_LIBRARY_URI, true);
+                        if (builtinResource == null) {
+                                throw new IllegalStateException("Failed to load builtin resource");
+                        }
+                        var contents = builtinResource.getContents();
+                        if (contents.isEmpty()) {
+                                throw new IllegalStateException("builtin resource is empty");
+                        }
+                        builtinProblem = (Problem) contents.getFirst();
+                        EcoreUtil.resolveAll(builtinResource);
                 }
-                return adapter;
+                return builtinProblem;
         }
 
-        private static ImportAdapter getAdapter(ResourceSet resourceSet) {
-        return (ImportAdapter) EcoreUtil.getAdapter(resourceSet.eAdapters(), ImportAdapter.class);
+        public BuiltinSymbols getBuiltinSymbols() {
+                if (builtinSymbols == null) {
+                        builtinSymbols = new BuiltinSymbols(getBuiltinProblem());
+                }
+                return builtinSymbols;
         }
 }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapterProvider.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapterProvider.java
new file mode 100644
index 00000000..5ab3a851
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportAdapterProvider.java
@@ -0,0 +1,68 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.scoping.imports;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import com.google.inject.Singleton;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.resource.Resource;
+import org.eclipse.emf.ecore.resource.ResourceSet;
+import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.jetbrains.annotations.NotNull;
+import tools.refinery.language.expressions.TermInterpreter;
+import tools.refinery.language.utils.BuiltinSymbols;
+
+@Singleton
+public class ImportAdapterProvider {
+        @Inject
+        private Provider<ImportAdapter> delegateProvider;
+
+        public BuiltinSymbols getBuiltinSymbols(@NotNull EObject context) {
+                var adapter = getOrInstall(context);
+                return adapter.getBuiltinSymbols();
+        }
+
+        public BuiltinSymbols getBuiltinSymbols(@NotNull Resource context) {
+                var adapter = getOrInstall(context);
+                return adapter.getBuiltinSymbols();
+        }
+
+        public TermInterpreter getTermInterpreter(@NotNull EObject context) {
+                var adapter = getOrInstall(context);
+                return adapter.getTermInterpreter();
+        }
+
+        public ImportAdapter getOrInstall(@NotNull EObject context) {
+                var resource = context.eResource();
+                if (resource == null) {
+                        throw new IllegalArgumentException("context is not in a resource");
+                }
+                return getOrInstall(resource);
+        }
+
+        public ImportAdapter getOrInstall(@NotNull Resource context) {
+                var resourceSet = context.getResourceSet();
+                if (resourceSet == null) {
+                        throw new IllegalArgumentException("context is not in a resource set");
+                }
+                return getOrInstall(resourceSet);
+        }
+
+        public ImportAdapter getOrInstall(@NotNull ResourceSet resourceSet) {
+                var adapter = getAdapter(resourceSet);
+                if (adapter == null) {
+                        adapter = delegateProvider.get();
+                        adapter.setResourceSet(resourceSet);
+                        resourceSet.eAdapters().add(adapter);
+                }
+                return adapter;
+        }
+
+        public static ImportAdapter getAdapter(@NotNull ResourceSet resourceSet) {
+                return (ImportAdapter) EcoreUtil.getAdapter(resourceSet.eAdapters(), ImportAdapter.class);
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java
index ac5a92ba..f3ab54ae 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/scoping/imports/ImportCollector.java
@@ -46,6 +46,9 @@ public class ImportCollector {
         @Inject
         private Provider<LoadOnDemandResourceDescriptionProvider> loadOnDemandProvider;
 
+        @Inject
+        private ImportAdapterProvider importAdapterProvider;
+
         public ImportCollection getDirectImports(Resource resource) {
                 return cache.get(DIRECT_IMPORTS_KEY, resource, () -> this.computeDirectImports(resource));
         }
@@ -58,7 +61,7 @@ public class ImportCollector {
                 if (resourceSet == null) {
                         return ImportCollection.EMPTY;
                 }
-                var adapter = ImportAdapter.getOrInstall(resourceSet);
+                var adapter = importAdapterProvider.getOrInstall(resourceSet);
                 var collection = new ImportCollection();
                 collectAutomaticImports(collection, adapter);
                 collectExplicitImports(problem, collection, adapter);
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/AggregatorName.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/AggregatorName.java
new file mode 100644
index 00000000..5939865a
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/AggregatorName.java
@@ -0,0 +1,19 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+import org.eclipse.xtext.naming.QualifiedName;
+
+public record AggregatorName(QualifiedName qualifiedName) {
+        public AggregatorName(QualifiedName prefix, String name) {
+                this(prefix.append(name));
+        }
+
+        @Override
+        public String toString() {
+                return qualifiedName.isEmpty() ? "" : qualifiedName.getLastSegment();
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/DataExprType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/DataExprType.java
new file mode 100644
index 00000000..9bc3e6aa
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/DataExprType.java
@@ -0,0 +1,19 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+import org.eclipse.xtext.naming.QualifiedName;
+
+public record DataExprType(QualifiedName qualifiedName) implements FixedType {
+        public DataExprType(QualifiedName prefix, String name) {
+                this(prefix.append(name));
+        }
+
+        @Override
+        public String toString() {
+                return qualifiedName.isEmpty() ? "" : qualifiedName.getLastSegment();
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java
new file mode 100644
index 00000000..9e44063d
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ExprType.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+public sealed interface ExprType permits FixedType, MutableType {
+        NodeType NODE = new NodeType();
+        LiteralType LITERAL = new LiteralType();
+        InvalidType INVALID = new InvalidType();
+
+        FixedType getActualType();
+
+        ExprType unwrapIfSet();
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java
new file mode 100644
index 00000000..1b2ded48
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/FixedType.java
@@ -0,0 +1,18 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+public sealed interface FixedType extends ExprType permits NodeType, LiteralType, InvalidType, DataExprType {
+        @Override
+        default FixedType getActualType() {
+                return this;
+        }
+
+        @Override
+        default FixedType unwrapIfSet() {
+                return this;
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/InvalidType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/InvalidType.java
new file mode 100644
index 00000000..c18612bc
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/InvalidType.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+public final class InvalidType implements FixedType {
+        InvalidType() {
+        }
+
+        @Override
+        public String toString() {
+                return "invalid";
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/LiteralType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/LiteralType.java
new file mode 100644
index 00000000..7fd33553
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/LiteralType.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+public final class LiteralType implements FixedType {
+        LiteralType() {
+        }
+
+        @Override
+        public String toString() {
+                return "constraint";
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/MutableType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/MutableType.java
new file mode 100644
index 00000000..78fdf884
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/MutableType.java
@@ -0,0 +1,32 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+public final class MutableType implements ExprType {
+        private DataExprType actualType;
+
+        @Override
+        public FixedType getActualType() {
+                return actualType == null ? INVALID : actualType;
+        }
+
+        public void setActualType(DataExprType actualType) {
+                if (this.actualType != null) {
+                        throw new IllegalStateException("Actual type was already set");
+                }
+                this.actualType = actualType;
+        }
+
+        @Override
+        public ExprType unwrapIfSet() {
+                return actualType == null ? this : actualType;
+        }
+
+        @Override
+        public String toString() {
+                return getActualType().toString();
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/NodeType.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/NodeType.java
new file mode 100644
index 00000000..1baff212
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/NodeType.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+public final class NodeType implements FixedType {
+        NodeType() {
+        }
+
+        @Override
+        public String toString() {
+                return "node";
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/ProblemTypeAnalyzer.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ProblemTypeAnalyzer.java
new file mode 100644
index 00000000..fcf99ad8
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/ProblemTypeAnalyzer.java
@@ -0,0 +1,32 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import com.google.inject.Singleton;
+import org.eclipse.xtext.util.IResourceScopeCache;
+import tools.refinery.language.model.problem.Problem;
+
+@Singleton
+public class ProblemTypeAnalyzer {
+        private static final String CACHE_KEY = "tools.refinery.language.typesystem.ProblemTypeAnalyzer.CACHE_KEY";
+
+        @Inject
+        private IResourceScopeCache resourceScopeCache;
+
+        @Inject
+        private Provider<TypedModule> typedModuleProvider;
+
+        public TypedModule getOrComputeTypes(Problem problem) {
+                var resource = problem.eResource();
+                return resourceScopeCache.get(CACHE_KEY, resource, () -> {
+                        var typedModule = typedModuleProvider.get();
+                        typedModule.setProblem(problem);
+                        return typedModule;
+                });
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/Signature.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/Signature.java
new file mode 100644
index 00000000..8e72c185
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/Signature.java
@@ -0,0 +1,11 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+import java.util.List;
+
+public record Signature(List<FixedType> parameterTypes, FixedType resultType) {
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java
new file mode 100644
index 00000000..3e25a0f5
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/SignatureProvider.java
@@ -0,0 +1,107 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+import com.google.inject.Inject;
+import com.google.inject.Singleton;
+import org.eclipse.xtext.naming.IQualifiedNameProvider;
+import org.eclipse.xtext.util.IResourceScopeCache;
+import tools.refinery.language.model.problem.*;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+
+@Singleton
+public class SignatureProvider {
+        private static final String PREFIX = "tools.refinery.language.typesystem.SignatureProvider.";
+        private static final String SIGNATURE_CACHE = PREFIX + "SIGNATURE_CACHE";
+        private static final String DATATYPE_CACHE = PREFIX + "DATATYPE_CACHE";
+        private static final String AGGREGATOR_CACHE = PREFIX + "AGGREGATOR_CACHE";
+
+        @Inject
+        private IQualifiedNameProvider qualifiedNameProvider;
+
+        @Inject
+        private IResourceScopeCache cache;
+
+        public Signature getSignature(Relation relation) {
+                var signatures = cache.get(SIGNATURE_CACHE, relation.eResource(), () -> new HashMap<Relation, Signature>());
+                return signatures.computeIfAbsent(relation, this::computeSignature);
+        }
+
+        public int getArity(Relation relation) {
+                return getSignature(relation).parameterTypes().size();
+        }
+
+        private Signature computeSignature(Relation relation) {
+                return new Signature(getParameterTypes(relation), getResultType(relation));
+        }
+
+        private List<FixedType> getParameterTypes(Relation relation) {
+                return switch (relation) {
+                        case ClassDeclaration ignored -> List.of(ExprType.NODE);
+                        case EnumDeclaration ignored -> List.of(ExprType.NODE);
+                        case DatatypeDeclaration datatypeDeclaration -> List.of(getDataType(datatypeDeclaration));
+                        case ReferenceDeclaration referenceDeclaration -> {
+                                if (referenceDeclaration.getReferenceType() instanceof DatatypeDeclaration) {
+                                        yield List.of(ExprType.NODE);
+                                }
+                                yield List.of(ExprType.NODE, ExprType.NODE);
+                        }
+                        case ParametricDefinition parametricDefinition -> {
+                                var parameters = parametricDefinition.getParameters();
+                                var exprTypes = new ArrayList<FixedType>(parameters.size());
+                                for (var parameter : parameters) {
+                                        if (parameter.getParameterType() instanceof DatatypeDeclaration datatypeDeclaration) {
+                                                exprTypes.add(getDataType(datatypeDeclaration));
+                                        } else {
+                                                exprTypes.add(ExprType.NODE);
+                                        }
+                                }
+                                yield List.copyOf(exprTypes);
+                        }
+                        default -> throw new IllegalArgumentException("Unknown Relation: " + relation);
+                };
+        }
+
+        private FixedType getResultType(Relation relation) {
+                if (relation instanceof ReferenceDeclaration referenceDeclaration &&
+                                referenceDeclaration.getReferenceType() instanceof DatatypeDeclaration datatypeDeclaration) {
+                        return getDataType(datatypeDeclaration);
+                }
+                return ExprType.LITERAL;
+        }
+
+        public DataExprType getDataType(DatatypeDeclaration datatypeDeclaration) {
+                var dataTypes = cache.get(DATATYPE_CACHE, datatypeDeclaration.eResource(),
+                                () -> new HashMap<DatatypeDeclaration, DataExprType>());
+                return dataTypes.computeIfAbsent(datatypeDeclaration, this::computeDataType);
+        }
+
+        private DataExprType computeDataType(DatatypeDeclaration datatypeDeclaration) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(datatypeDeclaration);
+                if (qualifiedName == null) {
+                        throw new IllegalArgumentException("Datatype declaration has no qualified name: " + datatypeDeclaration);
+                }
+                return new DataExprType(qualifiedName);
+        }
+
+        public AggregatorName getAggregatorName(AggregatorDeclaration aggregatorDeclaration) {
+                var dataTypes = cache.get(AGGREGATOR_CACHE, aggregatorDeclaration.eResource(),
+                                () -> new HashMap<AggregatorDeclaration, AggregatorName>());
+                return dataTypes.computeIfAbsent(aggregatorDeclaration, this::computeAggregatorName);
+        }
+
+        private AggregatorName computeAggregatorName(AggregatorDeclaration aggregatorDeclaration) {
+                var qualifiedName = qualifiedNameProvider.getFullyQualifiedName(aggregatorDeclaration);
+                if (qualifiedName == null) {
+                        throw new IllegalArgumentException(
+                                        "Aggregator declaration has no qualified name: " + aggregatorDeclaration);
+                }
+                return new AggregatorName(qualifiedName);
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java b/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java
new file mode 100644
index 00000000..de923e0d
--- /dev/null
+++ b/subprojects/language/src/main/java/tools/refinery/language/typesystem/TypedModule.java
@@ -0,0 +1,568 @@
+/*
+ * SPDX-FileCopyrightText: 2024 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.language.typesystem;
+
+import com.google.inject.Inject;
+import org.eclipse.emf.common.util.Diagnostic;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.emf.ecore.EStructuralFeature;
+import org.eclipse.xtext.validation.CheckType;
+import org.eclipse.xtext.validation.FeatureBasedDiagnostic;
+import tools.refinery.language.expressions.BuiltinTermInterpreter;
+import tools.refinery.language.expressions.TermInterpreter;
+import tools.refinery.language.model.problem.*;
+import tools.refinery.language.scoping.imports.ImportAdapterProvider;
+import tools.refinery.language.validation.ProblemValidator;
+
+import java.util.*;
+
+public class TypedModule {
+        private static final String OPERAND_TYPE_ERROR_MESSAGE = "Cannot determine operand type.";
+
+        @Inject
+        private SignatureProvider signatureProvider;
+
+        @Inject
+        private ImportAdapterProvider importAdapterProvider;
+
+        private TermInterpreter interpreter;
+        private final Map<Variable, List<AssignmentExpr>> assignments = new LinkedHashMap<>();
+        private final Map<Variable, FixedType> variableTypes = new HashMap<>();
+        private final Map<Expr, ExprType> expressionTypes = new HashMap<>();
+        private final Set<Variable> variablesToProcess = new LinkedHashSet<>();
+        private final List<FeatureBasedDiagnostic> diagnostics = new ArrayList<>();
+
+        void setProblem(Problem problem) {
+                interpreter = importAdapterProvider.getTermInterpreter(problem);
+                gatherAssignments(problem);
+                checkTypes(problem);
+        }
+
+        private void gatherAssignments(Problem problem) {
+                var iterator = problem.eAllContents();
+                while (iterator.hasNext()) {
+                        var eObject = iterator.next();
+                        if (!(eObject instanceof AssignmentExpr assignmentExpr)) {
+                                continue;
+                        }
+                        if (assignmentExpr.getLeft() instanceof VariableOrNodeExpr variableOrNodeExpr &&
+                                        variableOrNodeExpr.getVariableOrNode() instanceof Variable variable) {
+                                var assignmentList = assignments.computeIfAbsent(variable, ignored -> new ArrayList<>(1));
+                                assignmentList.add(assignmentExpr);
+                        }
+                        iterator.prune();
+                }
+        }
+
+        private void checkTypes(Problem problem) {
+                for (var statement : problem.getStatements()) {
+                        switch (statement) {
+                        case PredicateDefinition predicateDefinition -> checkTypes(predicateDefinition);
+                        case Assertion assertion -> checkTypes(assertion);
+                        default -> {
+                                // Nothing to type check.
+                        }
+                        }
+                }
+        }
+
+        private void checkTypes(PredicateDefinition predicateDefinition) {
+                for (var conjunction : predicateDefinition.getBodies()) {
+                        for (var literal : conjunction.getLiterals()) {
+                                coerceIntoLiteral(literal);
+                        }
+                }
+        }
+
+        private void checkTypes(Assertion assertion) {
+                var relation = assertion.getRelation();
+                var value = assertion.getValue();
+                if (relation == null) {
+                        return;
+                }
+                var type = signatureProvider.getSignature(relation).resultType();
+                if (type == ExprType.LITERAL) {
+                        if (value == null) {
+                                return;
+                        }
+                        expectType(value, BuiltinTermInterpreter.BOOLEAN_TYPE);
+                        return;
+                }
+                if (value == null) {
+                        var message = "Assertion value of type %s is required.".formatted(type);
+                        error(message, assertion, ProblemPackage.Literals.ASSERTION__RELATION, 0, ProblemValidator.TYPE_ERROR);
+                }
+                expectType(value, type);
+        }
+
+        public List<FeatureBasedDiagnostic> getDiagnostics() {
+                return diagnostics;
+        }
+
+        public FixedType getVariableType(Variable variable) {
+                // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant
+                // way, which would cause a ConcurrentModificationException with computeIfAbsent.
+                @SuppressWarnings("squid:S3824")
+                var type = variableTypes.get(variable);
+                //noinspection Java8MapApi
+                if (type == null) {
+                        type = computeVariableType(variable);
+                        variableTypes.put(variable, type);
+                }
+                return type;
+        }
+
+        private FixedType computeVariableType(Variable variable) {
+                if (variable instanceof Parameter) {
+                        return computeUnassignedVariableType(variable);
+                }
+                var assignmnentList = assignments.get(variable);
+                if (assignmnentList == null || assignmnentList.isEmpty()) {
+                        return computeUnassignedVariableType(variable);
+                }
+                if (variablesToProcess.contains(variable)) {
+                        throw new IllegalStateException("Circular reference to variable: " + variable.getName());
+                }
+                if (assignmnentList.size() > 1) {
+                        var message = "Multiple assignments for variable '%s'.".formatted(variable.getName());
+                        for (var assignment : assignmnentList) {
+                                error(message, assignment, ProblemPackage.Literals.BINARY_EXPR__LEFT, 0,
+                                                ProblemValidator.INVALID_ASSIGNMENT_ISSUE);
+                        }
+                        return ExprType.INVALID;
+                }
+                var assignment = assignmnentList.getFirst();
+                variablesToProcess.add(variable);
+                try {
+                        var assignedType = getExpressionType(assignment.getRight());
+                        if (assignedType instanceof MutableType) {
+                                var message = "Cannot determine type of variable '%s'.".formatted(variable.getName());
+                                error(message, assignment, ProblemPackage.Literals.BINARY_EXPR__RIGHT, 0, ProblemValidator.TYPE_ERROR);
+                                return ExprType.INVALID;
+                        }
+                        if (assignedType instanceof DataExprType dataExprType) {
+                                return dataExprType;
+                        }
+                        if (assignedType != ExprType.INVALID) {
+                                var message = "Expected data expression for variable '%s', got %s instead."
+                                                .formatted(variable.getName(), assignedType);
+                                error(message, assignment, ProblemPackage.Literals.BINARY_EXPR__RIGHT, 0, ProblemValidator.TYPE_ERROR);
+                        }
+                        return ExprType.INVALID;
+                } finally {
+                        variablesToProcess.remove(variable);
+                }
+        }
+
+        private FixedType computeUnassignedVariableType(Variable variable) {
+                if (variable instanceof Parameter parameter &&
+                                parameter.getParameterType() instanceof DatatypeDeclaration datatypeDeclaration) {
+                        return signatureProvider.getDataType(datatypeDeclaration);
+                }
+                // Parameters without an explicit datatype annotation are node variables.
+                return ExprType.NODE;
+        }
+
+        public ExprType getExpressionType(Expr expr) {
+                // We can't use computeIfAbsent here, because translating referenced queries calls this method in a reentrant
+                // way, which would cause a ConcurrentModificationException with computeIfAbsent.
+                @SuppressWarnings("squid:S3824")
+                var type = expressionTypes.get(expr);
+                //noinspection Java8MapApi
+                if (type == null) {
+                        type = computeExpressionType(expr);
+                        expressionTypes.put(expr, type);
+                }
+                return type.unwrapIfSet();
+        }
+
+        private ExprType computeExpressionType(Expr expr) {
+                return switch (expr) {
+                        case LogicConstant logicConstant -> computeExpressionType(logicConstant);
+                        case IntConstant ignored -> BuiltinTermInterpreter.INT_TYPE;
+                        case RealConstant ignored -> BuiltinTermInterpreter.REAL_TYPE;
+                        case StringConstant ignored -> BuiltinTermInterpreter.STRING_TYPE;
+                        case InfiniteConstant ignored -> new MutableType();
+                        case VariableOrNodeExpr variableOrNodeExpr -> computeExpressionType(variableOrNodeExpr);
+                        case AssignmentExpr assignmentExpr -> computeExpressionType(assignmentExpr);
+                        case Atom atom -> computeExpressionType(atom);
+                        case NegationExpr negationExpr -> computeExpressionType(negationExpr);
+                        case ArithmeticUnaryExpr arithmeticUnaryExpr -> computeExpressionType(arithmeticUnaryExpr);
+                        case CountExpr countExpr -> computeExpressionType(countExpr);
+                        case AggregationExpr aggregationExpr -> computeExpressionType(aggregationExpr);
+                        case ComparisonExpr comparisonExpr -> computeExpressionType(comparisonExpr);
+                        case LatticeBinaryExpr latticeBinaryExpr -> computeExpressionType(latticeBinaryExpr);
+                        case RangeExpr rangeExpr -> computeExpressionType(rangeExpr);
+                        case ArithmeticBinaryExpr arithmeticBinaryExpr -> computeExpressionType(arithmeticBinaryExpr);
+                        case CastExpr castExpr -> computeExpressionType(castExpr);
+                        default -> {
+                                error("Unknown expression: " + expr.getClass().getSimpleName(), expr, null, 0,
+                                                ProblemValidator.UNKNOWN_EXPRESSION_ISSUE);
+                                yield ExprType.INVALID;
+                        }
+                };
+        }
+
+        private ExprType computeExpressionType(LogicConstant expr) {
+                return switch (expr.getLogicValue()) {
+                        case TRUE, FALSE -> BuiltinTermInterpreter.BOOLEAN_TYPE;
+                        case UNKNOWN, ERROR -> new MutableType();
+                        case null -> ExprType.INVALID;
+                };
+        }
+
+        private ExprType computeExpressionType(VariableOrNodeExpr expr) {
+                var target = expr.getVariableOrNode();
+                if (target == null || target.eIsProxy()) {
+                        return ExprType.INVALID;
+                }
+                return switch (target) {
+                        case Node ignored -> ExprType.NODE;
+                        case Variable variable -> {
+                                if (variablesToProcess.contains(variable)) {
+                                        var message = "Circular reference to variable '%s'.".formatted(variable.getName());
+                                        error(message, expr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0,
+                                                        ProblemValidator.INVALID_ASSIGNMENT_ISSUE);
+                                        yield ExprType.INVALID;
+                                }
+                                yield getVariableType(variable);
+                        }
+                        default -> {
+                                error("Unknown variable: " + target.getName(), expr,
+                                                ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE, 0,
+                                                ProblemValidator.UNKNOWN_EXPRESSION_ISSUE);
+                                yield ExprType.INVALID;
+                        }
+                };
+        }
+
+        private ExprType computeExpressionType(AssignmentExpr expr) {
+                // Force the left side to type check. Since the left side is a variable, it will force the right side to also
+                // type check in order to infer the variable type.
+                return getExpressionType(expr.getLeft()) == ExprType.INVALID ? ExprType.INVALID : ExprType.LITERAL;
+        }
+
+        private ExprType computeExpressionType(Atom atom) {
+                var relation = atom.getRelation();
+                if (relation == null || relation.eIsProxy()) {
+                        return ExprType.INVALID;
+                }
+                if (relation instanceof DatatypeDeclaration) {
+                        var message = "Invalid call to data type. Use 'as %s' for casting.".formatted(
+                                        relation.getName());
+                        error(message, atom, ProblemPackage.Literals.ATOM__RELATION, 0, ProblemValidator.TYPE_ERROR);
+                }
+                var signature = signatureProvider.getSignature(relation);
+                var parameterTypes = signature.parameterTypes();
+                var arguments = atom.getArguments();
+                int size = Math.min(parameterTypes.size(), arguments.size());
+                boolean ok = parameterTypes.size() == arguments.size();
+                for (int i = 0; i < size; i++) {
+                        var parameterType = parameterTypes.get(i);
+                        var argument = arguments.get(i);
+                        if (!expectType(argument, parameterType)) {
+                                // Avoid short-circuiting to let us type check all arguments.
+                                ok = false;
+                        }
+                }
+                return ok ? signature.resultType() : ExprType.INVALID;
+        }
+
+        private ExprType computeExpressionType(NegationExpr negationExpr) {
+                var body = negationExpr.getBody();
+                if (body == null) {
+                        return ExprType.INVALID;
+                }
+                var actualType = getExpressionType(body);
+                if (actualType == ExprType.LITERAL) {
+                        // Negation of literals yields another (non-enumerable) literal.
+                        return ExprType.LITERAL;
+                }
+                if (actualType == DataExprType.INVALID) {
+                        return ExprType.INVALID;
+                }
+                if (actualType instanceof MutableType) {
+                        error(OPERAND_TYPE_ERROR_MESSAGE, body, null, 0, ProblemValidator.TYPE_ERROR);
+                        return ExprType.INVALID;
+                }
+                if (actualType instanceof DataExprType dataExprType) {
+                        var result = interpreter.getNegationType(dataExprType);
+                        if (result.isPresent()) {
+                                return result.get();
+                        }
+                }
+                var message = "Data type %s does not support negation.".formatted(actualType);
+                error(message, negationExpr, null, 0, ProblemValidator.TYPE_ERROR);
+                return ExprType.INVALID;
+        }
+
+        private ExprType computeExpressionType(ArithmeticUnaryExpr expr) {
+                var op = expr.getOp();
+                var body = expr.getBody();
+                if (op == null || body == null) {
+                        return ExprType.INVALID;
+                }
+                var actualType = getExpressionType(body);
+                if (actualType == DataExprType.INVALID) {
+                        return ExprType.INVALID;
+                }
+                if (actualType instanceof MutableType) {
+                        error(OPERAND_TYPE_ERROR_MESSAGE, body, null, 0, ProblemValidator.TYPE_ERROR);
+                        return ExprType.INVALID;
+                }
+                if (actualType instanceof DataExprType dataExprType) {
+                        var result = interpreter.getUnaryOperationType(op, dataExprType);
+                        if (result.isPresent()) {
+                                return result.get();
+                        }
+                }
+                var message = "Unsupported operator for data type %s.".formatted(actualType);
+                error(message, expr, null, 0, ProblemValidator.TYPE_ERROR);
+                return ExprType.INVALID;
+        }
+
+        private ExprType computeExpressionType(CountExpr countExpr) {
+                return coerceIntoLiteral(countExpr.getBody()) ? BuiltinTermInterpreter.INT_TYPE : ExprType.INVALID;
+        }
+
+        private ExprType computeExpressionType(AggregationExpr expr) {
+                var aggregator = expr.getAggregator();
+                if (aggregator == null || aggregator.eIsProxy()) {
+                        return null;
+                }
+                // Avoid short-circuiting to let us type check both the value and the condition.
+                boolean ok = coerceIntoLiteral(expr.getCondition());
+                var value = expr.getValue();
+                var actualType = getExpressionType(value);
+                if (actualType == ExprType.INVALID) {
+                        return ExprType.INVALID;
+                }
+                if (actualType instanceof MutableType) {
+                        error(OPERAND_TYPE_ERROR_MESSAGE, value, null, 0, ProblemValidator.TYPE_ERROR);
+                        return ExprType.INVALID;
+                }
+                if (actualType instanceof DataExprType dataExprType) {
+                        var aggregatorName = signatureProvider.getAggregatorName(aggregator);
+                        var result = interpreter.getAggregationType(aggregatorName, dataExprType);
+                        if (result.isPresent()) {
+                                return ok ? result.get() : ExprType.INVALID;
+                        }
+                }
+                var message = "Unsupported aggregator for type %s.".formatted(actualType);
+                error(message, expr, ProblemPackage.Literals.AGGREGATION_EXPR__AGGREGATOR, 0, ProblemValidator.TYPE_ERROR);
+                return ExprType.INVALID;
+        }
+
+        private ExprType computeExpressionType(ComparisonExpr expr) {
+                var left = expr.getLeft();
+                var right = expr.getRight();
+                var op = expr.getOp();
+                if (op == ComparisonOp.NODE_EQ || op == ComparisonOp.NODE_NOT_EQ) {
+                        // Avoid short-circuiting to let us type check both arguments.
+                        boolean leftOk = expectType(left, ExprType.NODE);
+                        boolean rightOk = expectType(right, ExprType.NODE);
+                        return leftOk && rightOk ? ExprType.LITERAL : ExprType.INVALID;
+                }
+                if (!(getCommonDataType(expr) instanceof DataExprType commonType)) {
+                        return ExprType.INVALID;
+                }
+                // Data equality and inequality are always supported for data types.
+                if (op != ComparisonOp.EQ && op != ComparisonOp.NOT_EQ && !interpreter.isComparisonSupported(commonType)) {
+                        var message = "Data type %s does not support comparison.".formatted(commonType);
+                        error(message, expr, null, 0, ProblemValidator.TYPE_ERROR);
+                        return ExprType.INVALID;
+                }
+                return BuiltinTermInterpreter.BOOLEAN_TYPE;
+        }
+
+        private ExprType computeExpressionType(LatticeBinaryExpr expr) {
+                // Lattice operations are always supported for data types.
+                return getCommonDataType(expr);
+        }
+
+        private ExprType computeExpressionType(RangeExpr expr) {
+                var left = expr.getLeft();
+                var right = expr.getRight();
+                if (left instanceof InfiniteConstant && right instanceof InfiniteConstant) {
+                        // `*..*` is equivalent to `unknown` if neither subexpression have been typed yet.
+                        var mutableType = new MutableType();
+                        if (expressionTypes.putIfAbsent(left, mutableType) == null &&
+                                        expressionTypes.put(right, mutableType) == null) {
+                                return mutableType;
+                        }
+                }
+                if (!(getCommonDataType(expr) instanceof DataExprType commonType)) {
+                        return ExprType.INVALID;
+                }
+                if (!interpreter.isRangeSupported(commonType)) {
+                        var message = "Data type %s does not support ranges.".formatted(commonType);
+                        error(message, expr, null, 0, ProblemValidator.TYPE_ERROR);
+                        return ExprType.INVALID;
+                }
+                return commonType;
+        }
+
+        private ExprType computeExpressionType(ArithmeticBinaryExpr expr) {
+                var op = expr.getOp();
+                var left = expr.getLeft();
+                var right = expr.getRight();
+                if (op == null || left == null || right == null) {
+                        return ExprType.INVALID;
+                }
+                // Avoid short-circuiting to let us type check both arguments.
+                var leftType = getExpressionType(left);
+                var rightType = getExpressionType(right);
+                if (leftType == ExprType.INVALID || rightType == ExprType.INVALID) {
+                        return ExprType.INVALID;
+                }
+                if (rightType instanceof MutableType rightMutableType) {
+                        if (leftType instanceof DataExprType leftExprType) {
+                                rightMutableType.setActualType(leftExprType);
+                                rightType = leftExprType;
+                        } else {
+                                error(OPERAND_TYPE_ERROR_MESSAGE, right, null, 0, ProblemValidator.TYPE_ERROR);
+                                return ExprType.INVALID;
+                        }
+                }
+                if (leftType instanceof MutableType leftMutableType) {
+                        if (rightType instanceof DataExprType rightExprType) {
+                                leftMutableType.setActualType(rightExprType);
+                                leftType = rightExprType;
+                        } else {
+                                error(OPERAND_TYPE_ERROR_MESSAGE, left, null, 0, ProblemValidator.TYPE_ERROR);
+                                return ExprType.INVALID;
+                        }
+                }
+                if (leftType instanceof DataExprType leftExprType && rightType instanceof DataExprType rightExprType) {
+                        var result = interpreter.getBinaryOperationType(op, leftExprType, rightExprType);
+                        if (result.isPresent()) {
+                                return result.get();
+                        }
+                }
+                var messageBuilder = new StringBuilder("Unsupported operator for ");
+                if (leftType.equals(rightType)) {
+                        messageBuilder.append("data type ").append(leftType);
+                } else {
+                        messageBuilder.append("data types ").append(leftType).append(" and ").append(rightType);
+                }
+                messageBuilder.append(".");
+                error(messageBuilder.toString(), expr, null, 0, ProblemValidator.TYPE_ERROR);
+                return ExprType.INVALID;
+        }
+
+        private ExprType computeExpressionType(CastExpr expr) {
+                var body = expr.getBody();
+                var targetRelation = expr.getTargetType();
+                if (body == null || !(targetRelation instanceof DatatypeDeclaration targetDeclaration)) {
+                        return null;
+                }
+                var actualType = getExpressionType(body);
+                if (actualType == ExprType.INVALID) {
+                        return ExprType.INVALID;
+                }
+                var targetType = signatureProvider.getDataType(targetDeclaration);
+                if (actualType instanceof MutableType mutableType) {
+                        // Type ascription for polymorphic literal (e.g., `unknown as int` for the set of all integers).
+                        mutableType.setActualType(targetType);
+                        return targetType;
+                }
+                if (actualType.equals(targetType)) {
+                        return targetType;
+                }
+                if (actualType instanceof DataExprType dataExprType && interpreter.isCastSupported(dataExprType, targetType)) {
+                        return targetType;
+                }
+                var message = "Casting from %s to %s is not supported.".formatted(actualType, targetType);
+                error(message, expr, null, 0, ProblemValidator.TYPE_ERROR);
+                return ExprType.INVALID;
+        }
+
+        private FixedType getCommonDataType(BinaryExpr expr) {
+                var commonType = getCommonType(expr);
+                if (!(commonType instanceof DataExprType) && commonType != ExprType.INVALID) {
+                        var message = "Expected data expression, got %s instead.".formatted(commonType);
+                        error(message, expr, null, 0, ProblemValidator.TYPE_ERROR);
+                        return ExprType.INVALID;
+                }
+                return commonType;
+        }
+
+        private FixedType getCommonType(BinaryExpr expr) {
+                var left = expr.getLeft();
+                var right = expr.getRight();
+                if (left == null || right == null) {
+                        return ExprType.INVALID;
+                }
+                var leftType = getExpressionType(left);
+                if (leftType instanceof FixedType fixedLeftType) {
+                        return expectType(right, fixedLeftType) ? fixedLeftType : ExprType.INVALID;
+                } else {
+                        var rightType = getExpressionType(right);
+                        if (rightType instanceof FixedType fixedRightType) {
+                                return expectType(left, leftType, fixedRightType) ? fixedRightType : ExprType.INVALID;
+                        } else {
+                                error(OPERAND_TYPE_ERROR_MESSAGE, left, null, 0, ProblemValidator.TYPE_ERROR);
+                                error(OPERAND_TYPE_ERROR_MESSAGE, right, null, 0, ProblemValidator.TYPE_ERROR);
+                                return ExprType.INVALID;
+                        }
+                }
+        }
+
+        private boolean coerceIntoLiteral(Expr expr) {
+                if (expr == null) {
+                        return false;
+                }
+                var actualType = getExpressionType(expr);
+                if (actualType == ExprType.LITERAL) {
+                        return true;
+                }
+                return expectType(expr, actualType, BuiltinTermInterpreter.BOOLEAN_TYPE);
+        }
+
+        private boolean expectType(Expr expr, FixedType expectedType) {
+                if (expr == null) {
+                        return false;
+                }
+                var actualType = getExpressionType(expr);
+                return expectType(expr, actualType, expectedType);
+        }
+
+        private boolean expectType(Expr expr, ExprType actualType, FixedType expectedType) {
+                if (expectedType == ExprType.INVALID) {
+                        // Silence any further errors is the expected type failed to compute.
+                        return false;
+                }
+                if (actualType.equals(expectedType)) {
+                        return true;
+                }
+                if (actualType == ExprType.INVALID) {
+                        // We have already emitted an error previously.
+                        return false;
+                }
+                if (actualType instanceof MutableType mutableType && expectedType instanceof DataExprType dataExprType) {
+                        mutableType.setActualType(dataExprType);
+                        return true;
+                }
+                var builder = new StringBuilder()
+                                .append("Expected ")
+                                .append(expectedType)
+                                .append(" expression");
+                if (!(actualType instanceof MutableType)) {
+                        builder.append(", got ")
+                                        .append(actualType)
+                                        .append(" instead");
+                }
+                builder.append(".");
+                error(builder.toString(), expr, null, 0, ProblemValidator.TYPE_ERROR);
+                return false;
+        }
+
+        private void error(String message, EObject object, EStructuralFeature feature, int index, String code,
+                                           String... issueData) {
+                diagnostics.add(new FeatureBasedDiagnostic(Diagnostic.ERROR, message, object, feature, index,
+                                CheckType.NORMAL, code, issueData));
+        }
+}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java b/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java
index c87fa044..72f23e85 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/utils/BuiltinSymbols.java
@@ -1,5 +1,5 @@
 /*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
  *
  * SPDX-License-Identifier: EPL-2.0
  */
@@ -7,7 +7,56 @@ package tools.refinery.language.utils;
 
 import tools.refinery.language.model.problem.*;
 
-public record BuiltinSymbols(Problem problem, ClassDeclaration node, PredicateDefinition equals,
-                                                         PredicateDefinition exists, ClassDeclaration contained, PredicateDefinition contains,
-                                                         PredicateDefinition invalidContainer) {
+public final class BuiltinSymbols {
+    private final Problem problem;
+    private final ClassDeclaration node;
+    private final PredicateDefinition equals;
+    private final PredicateDefinition exists;
+    private final ClassDeclaration contained;
+    private final PredicateDefinition contains;
+    private final PredicateDefinition invalidContainer;
+
+    public BuiltinSymbols(Problem problem) {
+        this.problem = problem;
+                node = getDeclaration(ClassDeclaration.class, "node");
+                equals = getDeclaration(PredicateDefinition.class, "equals");
+                exists = getDeclaration(PredicateDefinition.class, "exists");
+                contained = getDeclaration(ClassDeclaration.class, "contained");
+                contains = getDeclaration(PredicateDefinition.class, "contains");
+                invalidContainer = getDeclaration(PredicateDefinition.class, "invalidContainer");
+    }
+
+    public Problem problem() {
+        return problem;
+    }
+
+    public ClassDeclaration node() {
+        return node;
+    }
+
+    public PredicateDefinition equals() {
+        return equals;
+    }
+
+    public PredicateDefinition exists() {
+        return exists;
+    }
+
+    public ClassDeclaration contained() {
+        return contained;
+    }
+
+    public PredicateDefinition contains() {
+        return contains;
+    }
+
+    public PredicateDefinition invalidContainer() {
+        return invalidContainer;
+    }
+
+        private <T extends Statement & NamedElement> T getDeclaration(Class<T> type, String name) {
+                return problem.getStatements().stream().filter(type::isInstance).map(type::cast)
+                                .filter(declaration -> name.equals(declaration.getName())).findFirst()
+                                .orElseThrow(() -> new IllegalArgumentException("Built-in declaration " + name + " was not found"));
+        }
 }
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java
deleted file mode 100644
index d45c8083..00000000
--- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemDesugarer.java
+++ /dev/null
@@ -1,98 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2024 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.language.utils;
-
-import com.google.inject.Inject;
-import com.google.inject.Singleton;
-import org.eclipse.emf.ecore.EObject;
-import org.eclipse.emf.ecore.resource.Resource;
-import org.eclipse.xtext.util.IResourceScopeCache;
-import org.eclipse.xtext.util.Tuples;
-import tools.refinery.language.library.BuiltinLibrary;
-import tools.refinery.language.model.problem.*;
-
-import java.util.*;
-
-@Singleton
-public class ProblemDesugarer {
-        @Inject
-        private IResourceScopeCache cache = IResourceScopeCache.NullImpl.INSTANCE;
-
-        public Optional<Problem> getBuiltinProblem(EObject context) {
-                return Optional.ofNullable(context).map(EObject::eResource).flatMap(resource ->
-                                cache.get("builtinProblem", resource, () -> doGetBuiltinProblem(resource)));
-        }
-
-        private Optional<Problem> doGetBuiltinProblem(Resource resource) {
-                return Optional.ofNullable(resource).map(Resource::getResourceSet)
-                                .map(resourceSet -> resourceSet.getResource(BuiltinLibrary.BUILTIN_LIBRARY_URI, true))
-                                .map(Resource::getContents).filter(contents -> !contents.isEmpty()).map(List::getFirst)
-                                .filter(Problem.class::isInstance).map(Problem.class::cast);
-        }
-
-        public Optional<BuiltinSymbols> getBuiltinSymbols(EObject context) {
-                return getBuiltinProblem(context).map(builtin ->
-                                cache.get("builtinSymbols", builtin.eResource(), () -> doGetBuiltinSymbols(builtin)));
-        }
-
-        private BuiltinSymbols doGetBuiltinSymbols(Problem builtin) {
-                var node = doGetDeclaration(builtin, ClassDeclaration.class, "node");
-                var equals = doGetDeclaration(builtin, PredicateDefinition.class, "equals");
-                var exists = doGetDeclaration(builtin, PredicateDefinition.class, "exists");
-                var contained = doGetDeclaration(builtin, ClassDeclaration.class, "contained");
-                var contains = doGetDeclaration(builtin, PredicateDefinition.class, "contains");
-                var invalidContainer = doGetDeclaration(builtin, PredicateDefinition.class, "invalidContainer");
-                return new BuiltinSymbols(builtin, node, equals, exists, contained, contains, invalidContainer);
-        }
-
-        private <T extends Statement & NamedElement> T doGetDeclaration(Problem builtin, Class<T> type, String name) {
-                return builtin.getStatements().stream().filter(type::isInstance).map(type::cast)
-                                .filter(declaration -> name.equals(declaration.getName())).findFirst()
-                                .orElseThrow(() -> new IllegalArgumentException("Built-in declaration " + name + " was not found"));
-        }
-
-        public Collection<ClassDeclaration> getSuperclassesAndSelf(ClassDeclaration classDeclaration) {
-                return cache.get(Tuples.create(classDeclaration, "superclassesAndSelf"), classDeclaration.eResource(),
-                                () -> doGetSuperclassesAndSelf(classDeclaration));
-        }
-
-        private Collection<ClassDeclaration> doGetSuperclassesAndSelf(ClassDeclaration classDeclaration) {
-                var builtinSymbols = getBuiltinSymbols(classDeclaration);
-                Set<ClassDeclaration> found = new HashSet<>();
-                builtinSymbols.ifPresent(symbols -> found.add(symbols.node()));
-                Deque<ClassDeclaration> queue = new ArrayDeque<>();
-                queue.addLast(classDeclaration);
-                while (!queue.isEmpty()) {
-                        ClassDeclaration current = queue.removeFirst();
-                        if (!found.contains(current)) {
-                                found.add(current);
-                                for (Relation superType : current.getSuperTypes()) {
-                                        if (superType instanceof ClassDeclaration superDeclaration) {
-                                                queue.addLast(superDeclaration);
-                                        }
-                                }
-                        }
-                }
-                return found;
-        }
-
-        public Collection<ReferenceDeclaration> getAllReferenceDeclarations(ClassDeclaration classDeclaration) {
-                return cache.get(Tuples.create(classDeclaration, "allReferenceDeclarations"), classDeclaration.eResource(),
-                                () -> doGetAllReferenceDeclarations(classDeclaration));
-        }
-
-        private Collection<ReferenceDeclaration> doGetAllReferenceDeclarations(ClassDeclaration classDeclaration) {
-                Set<ReferenceDeclaration> referenceDeclarations = new HashSet<>();
-                for (ClassDeclaration superclass : getSuperclassesAndSelf(classDeclaration)) {
-            referenceDeclarations.addAll(superclass.getFeatureDeclarations());
-                }
-                return referenceDeclarations;
-        }
-
-        public boolean isContainmentReference(ReferenceDeclaration referenceDeclaration) {
-                return referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT;
-        }
-}
diff --git a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java
index 6d6d65da..9daa8f61 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/utils/ProblemUtil.java
@@ -98,18 +98,19 @@ public final class ProblemUtil {
                 return true;
         }
 
-        public static int getArity(Relation relation) {
+        public static boolean isTypeLike(Relation relation) {
                 if (relation instanceof ClassDeclaration || relation instanceof EnumDeclaration ||
                                 relation instanceof DatatypeDeclaration) {
-                        return 1;
-                }
-                if (relation instanceof ReferenceDeclaration) {
-                        return 2;
+                        return true;
                 }
                 if (relation instanceof PredicateDefinition predicateDefinition) {
-                        return predicateDefinition.getParameters().size();
+                        return predicateDefinition.getParameters().size() == 1;
                 }
-                throw new IllegalArgumentException("Unknown Relation: " + relation);
+                return false;
+        }
+
+        public static boolean isContainmentReference(ReferenceDeclaration referenceDeclaration) {
+                return referenceDeclaration.getKind() == ReferenceKind.CONTAINMENT;
         }
 
         public static boolean isContainerReference(ReferenceDeclaration referenceDeclaration) {
diff --git a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java
index 7f45bc20..745e2d2b 100644
--- a/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java
+++ b/subprojects/language/src/main/java/tools/refinery/language/validation/ProblemValidator.java
@@ -10,6 +10,7 @@
 package tools.refinery.language.validation;
 
 import com.google.inject.Inject;
+import org.eclipse.emf.common.util.Diagnostic;
 import org.eclipse.emf.ecore.EObject;
 import org.eclipse.emf.ecore.EReference;
 import org.eclipse.xtext.EcoreUtil2;
@@ -18,11 +19,15 @@ import org.eclipse.xtext.validation.Check;
 import org.jetbrains.annotations.Nullable;
 import tools.refinery.language.model.problem.*;
 import tools.refinery.language.naming.NamingUtil;
-import tools.refinery.language.scoping.imports.ImportAdapter;
-import tools.refinery.language.utils.ProblemDesugarer;
+import tools.refinery.language.scoping.imports.ImportAdapterProvider;
+import tools.refinery.language.typesystem.ProblemTypeAnalyzer;
+import tools.refinery.language.typesystem.SignatureProvider;
 import tools.refinery.language.utils.ProblemUtil;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.LinkedHashMap;
+import java.util.LinkedHashSet;
+import java.util.Set;
 
 /**
  * This class contains custom validation rules.
@@ -32,47 +37,39 @@ import java.util.*;
  */
 public class ProblemValidator extends AbstractProblemValidator {
         private static final String ISSUE_PREFIX = "tools.refinery.language.validation.ProblemValidator.";
-
         public static final String UNEXPECTED_MODULE_NAME_ISSUE = ISSUE_PREFIX + "UNEXPECTED_MODULE_NAME";
-
         public static final String INVALID_IMPORT_ISSUE = ISSUE_PREFIX + "INVALID_IMPORT";
-
         public static final String SINGLETON_VARIABLE_ISSUE = ISSUE_PREFIX + "SINGLETON_VARIABLE";
-
         public static final String NODE_CONSTANT_ISSUE = ISSUE_PREFIX + "NODE_CONSTANT_ISSUE";
-
         public static final String DUPLICATE_NAME_ISSUE = ISSUE_PREFIX + "DUPLICATE_NAME";
-
         public static final String INVALID_MULTIPLICITY_ISSUE = ISSUE_PREFIX + "INVALID_MULTIPLICITY";
-
         public static final String ZERO_MULTIPLICITY_ISSUE = ISSUE_PREFIX + "ZERO_MULTIPLICITY";
-
         public static final String MISSING_OPPOSITE_ISSUE = ISSUE_PREFIX + "MISSING_OPPOSITE";
-
         public static final String INVALID_OPPOSITE_ISSUE = ISSUE_PREFIX + "INVALID_OPPOSITE";
-
         public static final String INVALID_SUPERTYPE_ISSUE = ISSUE_PREFIX + "INVALID_SUPERTYPE";
-
         public static final String INVALID_REFERENCE_TYPE_ISSUE = ISSUE_PREFIX + "INVALID_REFERENCE_TYPE";
-
         public static final String INVALID_ARITY_ISSUE = ISSUE_PREFIX + "INVALID_ARITY";
-
         public static final String INVALID_TRANSITIVE_CLOSURE_ISSUE = ISSUE_PREFIX + "INVALID_TRANSITIVE_CLOSURE";
-
         public static final String INVALID_VALUE_ISSUE = ISSUE_PREFIX + "INVALID_VALUE";
-
         public static final String UNSUPPORTED_ASSERTION_ISSUE = ISSUE_PREFIX + "UNSUPPORTED_ASSERTION";
-
+        public static final String UNKNOWN_EXPRESSION_ISSUE = ISSUE_PREFIX + "UNKNOWN_EXPRESSION";
         public static final String INVALID_ASSIGNMENT_ISSUE = ISSUE_PREFIX + "INVALID_ASSIGNMENT";
+        public static final String TYPE_ERROR = ISSUE_PREFIX + "TYPE_ERROR";
 
         @Inject
         private ReferenceCounter referenceCounter;
 
         @Inject
-        private ProblemDesugarer desugarer;
+        private IQualifiedNameConverter qualifiedNameConverter;
 
         @Inject
-        private IQualifiedNameConverter qualifiedNameConverter;
+        private ImportAdapterProvider importAdapterProvider;
+
+        @Inject
+        private SignatureProvider signatureProvider;
+
+        @Inject
+        private ProblemTypeAnalyzer typeAnalyzer;
 
         @Check
         public void checkModuleName(Problem problem) {
@@ -88,7 +85,7 @@ public class ProblemValidator extends AbstractProblemValidator {
                 if (resourceSet == null) {
                         return;
                 }
-                var adapter = ImportAdapter.getOrInstall(resourceSet);
+                var adapter = importAdapterProvider.getOrInstall(resourceSet);
                 var expectedName = adapter.getQualifiedName(resource.getURI());
                 if (expectedName == null) {
                         return;
@@ -158,15 +155,19 @@ public class ProblemValidator extends AbstractProblemValidator {
         public void checkUniqueDeclarations(Problem problem) {
                 var relations = new ArrayList<Relation>();
                 var nodes = new ArrayList<Node>();
+                var aggregators = new ArrayList<AggregatorDeclaration>();
                 for (var statement : problem.getStatements()) {
                         if (statement instanceof Relation relation) {
                                 relations.add(relation);
                         } else if (statement instanceof NodeDeclaration nodeDeclaration) {
                                 nodes.addAll(nodeDeclaration.getNodes());
+                        } else if (statement instanceof AggregatorDeclaration aggregatorDeclaration) {
+                                aggregators.add(aggregatorDeclaration);
                         }
                 }
                 checkUniqueSimpleNames(relations);
                 checkUniqueSimpleNames(nodes);
+                checkUniqueSimpleNames(aggregators);
         }
 
         @Check
@@ -353,11 +354,14 @@ public class ProblemValidator extends AbstractProblemValidator {
 
         @Check
         public void checkAssertion(Assertion assertion) {
-                int argumentCount = assertion.getArguments().size();
-                if (!(assertion.getValue() instanceof LogicConstant)) {
-                        var message = "Assertion value must be one of 'true', 'false', 'unknown', or 'error'.";
-                        acceptError(message, assertion, ProblemPackage.Literals.ASSERTION__VALUE, 0, INVALID_VALUE_ISSUE);
+                var relation = assertion.getRelation();
+                if (relation instanceof DatatypeDeclaration) {
+                        var message = "Assertions for data types are not supported.";
+                        acceptError(message, assertion, ProblemPackage.Literals.ASSERTION__RELATION, 0,
+                                        UNSUPPORTED_ASSERTION_ISSUE);
+                        return;
                 }
+                int argumentCount = assertion.getArguments().size();
                 checkArity(assertion, ProblemPackage.Literals.ASSERTION__RELATION, argumentCount);
         }
 
@@ -376,7 +380,7 @@ public class ProblemValidator extends AbstractProblemValidator {
                         // Feature does not point to a {@link Relation}, we are probably already emitting another error.
                         return;
                 }
-                int arity = ProblemUtil.getArity(relation);
+                int arity = signatureProvider.getArity(relation);
                 if (arity == expectedArity) {
                         return;
                 }
@@ -387,11 +391,7 @@ public class ProblemValidator extends AbstractProblemValidator {
 
         @Check
         public void checkMultiObjectAssertion(Assertion assertion) {
-                var builtinSymbolsOption = desugarer.getBuiltinSymbols(assertion);
-                if (builtinSymbolsOption.isEmpty()) {
-                        return;
-                }
-                var builtinSymbols = builtinSymbolsOption.get();
+                var builtinSymbols = importAdapterProvider.getBuiltinSymbols(assertion);
                 var relation = assertion.getRelation();
                 boolean isExists = builtinSymbols.exists().equals(relation);
                 boolean isEquals = builtinSymbols.equals().equals(relation);
@@ -524,5 +524,37 @@ public class ProblemValidator extends AbstractProblemValidator {
                         acceptError(message, variableOrNodeExpr, ProblemPackage.Literals.VARIABLE_OR_NODE_EXPR__VARIABLE_OR_NODE,
                                         0, INVALID_ASSIGNMENT_ISSUE);
                 }
+                if (!(assignmentExpr.eContainer() instanceof Conjunction)) {
+                        var message = "Assignments may only appear as top-level expressions.";
+                        acceptError(message, assignmentExpr, null, 0, INVALID_ASSIGNMENT_ISSUE);
+                }
+        }
+
+        @Check
+        private void checkInfiniteConstant(InfiniteConstant infiniteConstant) {
+                if (!(infiniteConstant.eContainer() instanceof RangeExpr)) {
+                        var message = "Negative and positive infinity literals may only appear in '..' range expressions.";
+                        acceptError(message, infiniteConstant, null, 0, TYPE_ERROR);
+                }
+        }
+
+        @Check
+        private void checkTypes(Problem problem) {
+                var diagnostics = typeAnalyzer.getOrComputeTypes(problem).getDiagnostics();
+                for (var diagnostic : diagnostics) {
+                        switch (diagnostic.getSeverity()) {
+                        case Diagnostic.INFO -> info(diagnostic.getMessage(), diagnostic.getSourceEObject(),
+                                        diagnostic.getFeature(), diagnostic.getIndex(), diagnostic.getIssueCode(),
+                                        diagnostic.getIssueData());
+                        case Diagnostic.WARNING -> warning(diagnostic.getMessage(), diagnostic.getSourceEObject(),
+                                        diagnostic.getFeature(), diagnostic.getIndex(), diagnostic.getIssueCode(),
+                                        diagnostic.getIssueData());
+                        case Diagnostic.ERROR -> error(diagnostic.getMessage(), diagnostic.getSourceEObject(),
+                                        diagnostic.getFeature(), diagnostic.getIndex(), diagnostic.getIssueCode(),
+                                        diagnostic.getIssueData());
+                        default -> throw new IllegalStateException("Unknown severity %s of %s"
+                                        .formatted(diagnostic.getSeverity(), diagnostic));
+                        }
+                }
         }
 }