diff --git a/.github/workflows/develop.yml b/.github/workflows/develop.yml
index 23ae120f712..117e4c975d5 100644
--- a/.github/workflows/develop.yml
+++ b/.github/workflows/develop.yml
@@ -37,3 +37,56 @@ jobs:
           if git add --update && git commit --no-edit --allow-empty --message "Set Version: $(cat package/version)"; then
             git push origin master
           fi
+
+  post-performance-tests:
+    name: 'Performace Tests'
+    runs-on: [self-hosted, linux, normal]
+    continue-on-error: true
+    steps:
+      - uses: actions/checkout@v3
+      - name: 'Set up Docker Test Image'
+        env:
+          BASE_OS: ubuntu
+          BASE_DISTRO: jammy
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          BENCHER_API_TOKEN: ${{ secrets.BENCHER_API_TOKEN }}
+          BENCHER_PROJECT: k-framework
+          BENCHER_ADAPTER: json
+        run: |
+          set -euxo pipefail
+          workspace=$(pwd)
+          docker run --name k-posting-profiling-tests-${GITHUB_SHA}                                   \
+            --rm -it --detach                                                  \
+            -e BENCHER_API_TOKEN=$BENCHER_API_TOKEN                            \
+            -e BENCHER_PROJECT=$BENCHER_PROJECT                                \
+            -e BENCHER_ADAPTER=$BENCHER_ADAPTER                                \
+            -e GITHUB_HEAD_REF=$GITHUB_HEAD_REF                                \
+            -e GITHUB_BASE_REF=$GITHUB_BASE_REF                                \
+            -e GITHUB_TOKEN=$GITHUB_TOKEN                                      \
+            -e GITHUB_ACTIONS=true                                             \
+            -e GITHUB_EVENT_NAME=$GITHUB_EVENT_NAME                            \
+            -e GITHUB_REPOSITORY=$GITHUB_REPOSITORY                            \
+            -e GITHUB_REF=$GITHUB_REF                                          \
+            --workdir /opt/workspace                                           \
+            -v "${workspace}:/opt/workspace"                                   \
+            ${BASE_OS}:${BASE_DISTRO}
+      - name: 'Setting up dependencies'
+        run: |
+          set -euxo pipefail
+          docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c './k-distribution/tests/profiling/setup_profiling.sh SKIP_K_BUILD'
+      - name: 'Getting Performance Tests Results'
+        run: |
+          set -euxo pipefail
+          docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c './k-distribution/tests/profiling/post_results_to_develop.py'
+      - name: 'Posting Performance Tests Results'
+        run: |
+          set -euxo pipefail
+          docker exec -t k-posting-profiling-tests-${GITHUB_SHA} /bin/bash -c 'bencher run            \
+            --if-branch "develop" --else-if-branch "master"                    \
+            --file .profiling-results.json --err --ci-only-on-alert            \
+            --github-actions "${GITHUB_TOKEN}" 'echo "Exporting report"'
+      - name: 'Tear down Docker'
+        if: always()
+        run: |
+          docker stop --time=0 k-posting-profiling-tests-${GITHUB_SHA}
+          docker container rm --force k-posting-profiling-tests-${GITHUB_SHA} || true
diff --git a/bencher_0.3.10_amd64.deb b/bencher_0.3.10_amd64.deb
deleted file mode 100644
index dd0f8675b14..00000000000
Binary files a/bencher_0.3.10_amd64.deb and /dev/null differ
diff --git a/flake.nix b/flake.nix
index 6a4ab2587a0..a4d75d82f22 100644
--- a/flake.nix
+++ b/flake.nix
@@ -8,7 +8,6 @@
       # NB booster-backend will bring in another dependency on haskell-backend,
       # but the two are not necessarily the same (different more often than not).
       # We get two transitive dependencies on haskell-nix.
-      inputs.k-framework.follows = "";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
     };
     llvm-backend.url = "github:runtimeverification/llvm-backend";
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
index 3201868b13e..5c20d442625 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
+++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
@@ -9,13 +9,16 @@
 @RequestScoped
 public class HaskellKRunOptions {
 
-    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", hidden = true)
+    @Parameter(names="--haskell-backend-command", descriptionKey = "command",
+            description="Command to run the Haskell backend execution engine.", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 
-    @Parameter(names="--haskell-backend-home", description="Directory where the Haskell backend source installation resides.", hidden = true)
+    @Parameter(names="--haskell-backend-home", descriptionKey = "directory",
+            description="Directory where the Haskell backend source installation resides.", hidden = true)
     public String haskellBackendHome = System.getenv("KORE_HOME");
 
-    @Parameter(names="--default-claim-type", converter = SentenceTypeConverter.class, description="Default type for claims. Values: [all-path|one-path].")
+    @Parameter(names="--default-claim-type", descriptionKey = "type", converter = SentenceTypeConverter.class,
+            description="Default type for claims. Values: [all-path|one-path].")
     public ModuleToKORE.SentenceType defaultClaimType = ModuleToKORE.SentenceType.ALL_PATH;
 
     public static class SentenceTypeConverter extends BaseEnumConverter<ModuleToKORE.SentenceType> {
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
index 035a1fa53cc..69a9c8b4b2c 100644
--- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
+++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
@@ -7,7 +7,7 @@
 @RequestScoped
 public class HaskellKompileOptions {
 
-    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", hidden = true)
+    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", descriptionKey = "command", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 
     @Parameter(names="--no-haskell-binary", description="Use the textual KORE format in the haskell backend instead of the binary KORE format. This is a development option, but may be necessary on MacOS due to known issues with the binary format.")
diff --git a/k-distribution/src/main/scripts/lib/k b/k-distribution/src/main/scripts/lib/k
index 0a8d9ed0094..34f4bf3b639 100755
--- a/k-distribution/src/main/scripts/lib/k
+++ b/k-distribution/src/main/scripts/lib/k
@@ -5,6 +5,7 @@ ulimit -s "$(ulimit -H -s)"
 K_BASE="$(cd "$(dirname "${BASH_SOURCE[0]}")/../" && pwd)"
 GIT_DESCRIBE="${K_BASE}/kframework/git-describe.out"
 TIMESTAMP="${K_BASE}/kframework/timestamp.out"
+version=
 
 for flag in "$@"; do
     if [[ "$flag" == "--version" ]]; then
diff --git a/k-distribution/src/main/scripts/lib/k-util.sh b/k-distribution/src/main/scripts/lib/k-util.sh
index f10145c5e2f..34d723f97cb 100644
--- a/k-distribution/src/main/scripts/lib/k-util.sh
+++ b/k-distribution/src/main/scripts/lib/k-util.sh
@@ -33,7 +33,7 @@ k_util_usage() {
   --no-exc-wrap     Do not wrap messages to 80 chars (keep long lines).
   --profile         Print coarse process timing information. Format printed:
                     exit-code wall-time user-time system-time command args*
-  --temp-dir        Put temp files in this location. Default: /tmp/.<tool>-xxx
+  --temp-dir PATH   Put temp files in this location. Default: /tmp/.<tool>-xxx
   -v, --verbose     Print significant sub-commands executed.
 HERE
 }
diff --git a/k-distribution/tests/profiling/Makefile b/k-distribution/tests/profiling/Makefile
index 30bbec6c2cd..fe4d8116925 100644
--- a/k-distribution/tests/profiling/Makefile
+++ b/k-distribution/tests/profiling/Makefile
@@ -1,4 +1,4 @@
-EXCLUDE=Makefile kprofiling.mak setup_profiling.sh
+EXCLUDE=Makefile kprofiling.mak setup_profiling.sh post_results_to_develop.py
 SUBDIRS=$(filter-out $(EXCLUDE), $(wildcard *))
 
 SUBCLEAN=$(addsuffix .clean,$(SUBDIRS))
diff --git a/k-distribution/tests/profiling/post_results_to_develop.py b/k-distribution/tests/profiling/post_results_to_develop.py
new file mode 100755
index 00000000000..37104b56def
--- /dev/null
+++ b/k-distribution/tests/profiling/post_results_to_develop.py
@@ -0,0 +1,73 @@
+#!/usr/bin/env python3
+import json
+import subprocess
+
+COMMIT_SHA=''
+FROM_BRANCH=''
+TO_BRANCH='develop'
+
+def execute_command(command):
+    # Try to run the command
+    try:
+        result = subprocess.run(command,stdout=subprocess.PIPE,
+                                stderr=subprocess.PIPE, text=True)
+
+        # Check for errors
+        if result.returncode != 0:
+            print("Error:", result.stderr)
+            exit(1)
+
+    except subprocess.CalledProcessError as e:
+        # Handle any errors or exceptions here
+        print("Error:", e)
+        exit(1)
+
+    return result.stdout
+
+# git command to get the last commit in develop
+commit_command = [ 'git', 'log', '--format=\"%H\"', '-n', '1' ]
+COMMIT_SHA = execute_command(commit_command).strip('\"').strip('\"\n')
+
+# curl command to get the branch name of last commit in develop
+API_URL = 'https://api.github.com/repos/runtimeverification/k/commits/' \
+        + COMMIT_SHA + '/pulls'
+branch_command = ['curl', '-L', '-H', 'Accept:', 'application/vnd.github+json',
+                  '-H', '\"Authorization', 'Bearer', '${GITHUB_TOKEN}\"', '-H',
+                  '\"X-GitHub-Api-Version:', '2022-11-28\"', API_URL]
+FROM_BRANCH = json.loads(execute_command(branch_command))[0]['head']['label']
+
+print("Exporting last bencher report from", FROM_BRANCH, "to", TO_BRANCH)
+
+# This command will generate a JSON file with a list containing the last reports
+# sorted in descendenting order for the project.
+bencher_command = ["bencher", "report", "list", "--project", "k-framework",
+                   "--sort", "date_time", "--direction", "desc", "--per-page",
+                   "255"]
+data = json.loads(execute_command(bencher_command))
+
+# Collect all elemnts where the key 'project' is 'k_framework'
+k_framework = [item for item in data if item['project']['slug'] == 'k-framework'
+               and item['branch']['slug'] == FROM_BRANCH]
+
+# Append the last 6 reports to the list, they correspond to the last performance
+# execution on the last commit in FROM_BRANCH
+def get_name_and_value(item):
+    return item['metric_kind']['slug'], item['benchmarks'][0]['metric']['value']
+
+data = {}
+for i in range(0,6):
+    item = k_framework[i]
+    results = item['results']
+    benchmark_name = results[0][0]['benchmarks'][0]['name']
+    metric_name_memory, value_memory = get_name_and_value(results[0][0])
+    metric_name_size, value_size = get_name_and_value(results[0][1])
+
+    branch = item['branch']
+    print("Appended:", benchmark_name, "created in", item['created'],
+          "on branch", branch['name'], "with version", branch['version']['number'])
+
+    data.update({benchmark_name: {metric_name_size: {"value": value_size},
+                                  metric_name_memory: {"value": value_memory}}
+                 })
+
+json.dump(data, open('.profiling-results.json', 'w'), indent=4)
diff --git a/k-distribution/tests/profiling/setup_profiling.sh b/k-distribution/tests/profiling/setup_profiling.sh
index e8a0cfc8398..1fa3000f8f4 100755
--- a/k-distribution/tests/profiling/setup_profiling.sh
+++ b/k-distribution/tests/profiling/setup_profiling.sh
@@ -6,8 +6,11 @@ export DEBIAN_FRONTEND=noninteractive
 export BENCHER_VERSION="0.3.10"
 apt-get update
 apt-get upgrade --yes
-apt-get install --yes make time sudo wget
-apt-get install --yes ./kframework.deb
+apt-get install --yes python3 git curl make time sudo wget
+# Build K if no flag was given and don't execute if flag was given
+if [ $# -eq 0 ]; then
+    apt-get install --yes ./kframework.deb
+fi
 
 wget https://github.com/bencherdev/bencher/releases/download/v"${BENCHER_VERSION}"/bencher_"${BENCHER_VERSION}"_amd64.deb
 sudo dpkg -i bencher_"${BENCHER_VERSION}"_amd64.deb
diff --git a/kernel/src/main/java/org/kframework/kast/KastOptions.java b/kernel/src/main/java/org/kframework/kast/KastOptions.java
index 8ea28def485..2aaa084b516 100644
--- a/kernel/src/main/java/org/kframework/kast/KastOptions.java
+++ b/kernel/src/main/java/org/kframework/kast/KastOptions.java
@@ -101,20 +101,23 @@ public File bisonOutputFile() {
         return files.get().resolveWorkingDirectory(parameters.get(0));
     }
 
-    @Parameter(names="--bison-file", description="C file containing functions to link into bison parser.", hidden = true)
+    @Parameter(names="--bison-file", descriptionKey = "file", hidden = true,
+            description="C file containing functions to link into bison parser.")
     public String bisonFile;
 
-    @Parameter(names="--bison-stack-max-depth", description="Maximum size of bison parsing stack (default: 10000).", hidden = true)
+    @Parameter(names="--bison-stack-max-depth", descriptionKey = "size", hidden = true,
+            description="Maximum size of bison parsing stack.")
     public long bisonStackMaxDepth = 10000;
 
-    @Parameter(names={"--expression", "-e"}, description="An expression to parse passed on the command " +
-    "line. It is an error to provide both this option and a file to parse.")
+    @Parameter(names={"--expression", "-e"}, descriptionKey = "expression",
+            description="An expression to parse passed on the command line. It is an error to provide both this " +
+                    "option and a file to parse.")
     private String expression;
 
-    @Parameter(names={"--sort", "-s"}, converter=SortTypeConverter.class, description="The start sort for the default parser. " +
-            "The default is the sort of $PGM from the configuration. A sort may also be specified " +
-            "with the 'KRUN_SORT' environment variable, in which case it is used if the option is " +
-            "not specified on the command line.")
+    @Parameter(names={"--sort", "-s"}, descriptionKey = "sort", converter=SortTypeConverter.class,
+            description="The start sort for the default parser. The default is the sort of $PGM from the configuration. " +
+                    "A sort may also be specified with the 'KRUN_SORT' environment variable, in which case it is used " +
+                    "if the option is not specified on the command line.")
     public Sort sort;
 
     public static class SortTypeConverter implements IStringConverter<Sort> {
@@ -125,17 +128,20 @@ public Sort convert(String arg) {
         }
     }
 
-    @Parameter(names={"--module", "-m"}, description="Parse text in the specified module. Defaults to the syntax module of the definition.")
+    @Parameter(names={"--module", "-m"}, descriptionKey = "name",
+            description="Parse text in the specified module. Defaults to the syntax module of the definition.")
     public String module;
 
     @Parameter(names="--expand-macros", description="Also expand macros in the parsed string.")
     public boolean expandMacros = false;
 
-    @Parameter(names={"--input", "-i"}, converter=InputModeConverter.class,
+    @Parameter(names={"--input", "-i"}, descriptionKey = "mode", converter=InputModeConverter.class,
             description="How to read kast input in. <mode> is either [program|binary|kast|json|kore|rule].")
     public InputModes input = InputModes.PROGRAM;
 
-    @Parameter(names={"--steps"}, description="Apply specified kompilation steps to the parsed term. Only for --input rule. Use --steps help for a detailed description of available steps.")
+    @Parameter(names={"--steps"}, descriptionKey = "steps",
+            description="Apply specified kompilation steps to the parsed term. Only for --input rule. " +
+                    "Use --steps help for a detailed description of available steps.")
     public List<KastFrontEnd.KompileSteps> steps = Lists.newArrayList(KastFrontEnd.KompileSteps.anonVars);
 
     public static class InputModeConverter extends BaseEnumConverter<InputModes> {
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
index 1e40080a1be..8d494435b6d 100644
--- a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
+++ b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
@@ -49,10 +49,12 @@ GlobalOptions getGlobalOptions_UseOnlyInGuiceProvider() {
     public OutputDirectoryOptions outputDirectory = new OutputDirectoryOptions();
 
     // Common options
-    @Parameter(names="--backend", description="Choose a backend. <backend> is one of [llvm|haskell|kore]. Each creates the kompiled K definition.")
+    @Parameter(names="--backend", description="Choose a backend. <backend> is one of [llvm|haskell|kore]. Each creates the kompiled K definition.", descriptionKey = "backend")
     public String backend = Backends.LLVM;
 
-    @Parameter(names="--main-module", description="Specify main module in which a program starts to execute. This information is used by 'krun'. The default is the name of the given K definition file without the extension (.k).")
+    @Parameter(names="--main-module", descriptionKey = "name",
+            description="Specify main module in which a program starts to execute. This information is used by 'krun'. " +
+            "The default is the name of the given K definition file without the extension (.k).")
     private String mainModule;
 
     public String mainModule(FileUtil files) {
@@ -62,7 +64,8 @@ public String mainModule(FileUtil files) {
         return mainModule;
     }
 
-    @Parameter(names="--syntax-module", description="Specify main module for syntax. This information is used by 'krun'. (Default: <main-module>-SYNTAX).")
+    @Parameter(names="--syntax-module", descriptionKey = "name",
+            description="Specify main module for syntax. This information is used by 'krun'. (Default: <main-module>-SYNTAX).")
     private String syntaxModule;
 
     public String syntaxModule(FileUtil files) {
@@ -75,7 +78,7 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--coverage", description="Generate coverage data when executing semantics.")
     public boolean coverage;
 
-    @Parameter(names="--hook-namespaces", listConverter=StringListConverter.class, description="<string> is a whitespace-separated list of namespaces to include in the hooks defined in the definition", hidden = true)
+    @Parameter(names="--hook-namespaces", listConverter=StringListConverter.class, description="<string> is a whitespace-separated list of namespaces to include in the hooks defined in the definition", descriptionKey = "string", hidden = true)
     public List<String> hookNamespaces = Collections.emptyList();
 
     @Parameter(names="-O1", description="Optimize in ways that improve performance and code size, but interfere with debugging and increase compilation time slightly.")
@@ -96,8 +99,7 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--read-only-kompiled-directory", description="Files in the generated kompiled directory should be read-only to other frontend tools.", hidden = true)
     public boolean readOnlyKompiledDirectory = false;
 
-    @Parameter(names="--concrete-rules", description="List of rule labels to be considered concrete, in addition to " +
-            "rules marked with `[concrete]` attribute")
+    @Parameter(names="--concrete-rules", description="List of rule labels to be considered concrete, in addition to rules marked with `[concrete]` attribute", descriptionKey = "labels")
     public List<String> extraConcreteRuleLabels = Collections.emptyList();
 
     @ParametersDelegate
@@ -115,10 +117,10 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--gen-glr-bison-parser", description="Emit GLR bison parser for the PGM configuration variable within the syntax module of your definition into the kompiled definition.")
     public boolean genGlrBisonParser;
 
-    @Parameter(names="--bison-file", description="C file containing functions to link into bison parser.", hidden = true)
+    @Parameter(names="--bison-file", description="C file containing functions to link into bison parser.", descriptionKey = "file", hidden = true)
     public String bisonFile;
 
-    @Parameter(names="--bison-stack-max-depth", description="Maximum size of bison parsing stack (default: 10000).", hidden = true)
+    @Parameter(names="--bison-stack-max-depth", description="Maximum size of bison parsing stack.", descriptionKey = "size", hidden = true)
     public long bisonStackMaxDepth = 10000;
 
     @Parameter(names="--bison-parser-library", description="Generate a shared library rather than an executable for Bison parsers", hidden = true)
@@ -129,10 +131,10 @@ public String syntaxModule(FileUtil files) {
     @Parameter(names="--top-cell", description="Choose the top configuration cell when more than one is provided. Does nothing if only one top cell exists.")
     public String topCell;
 
-    @Parameter(names="--debug-type-inference", description="Filename and source line of rule to debug type inference for. This is generally an option used only by maintainers.", hidden = true)
+    @Parameter(names="--debug-type-inference", description="Filename and source line of rule to debug type inference for. This is generally an option used only by maintainers.", descriptionKey = "file", hidden = true)
     public String debugTypeInference;
 
-    @Parameter(names={"--post-process"}, description="JSON KAST => JSON KAST converter to run on definition after kompile pipeline.", hidden = true)
+    @Parameter(names={"--post-process"}, description="JSON KAST => JSON KAST converter to run on definition after kompile pipeline.", descriptionKey = "command", hidden = true)
     public String postProcess;
 
     // TODO(dwightguth): remove this when it is no longer needed
diff --git a/kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java b/kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java
index fb8246c1f01..f77bb3f154e 100644
--- a/kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java
+++ b/kernel/src/main/java/org/kframework/kompile/KompileUsageFormatter.java
@@ -195,12 +195,16 @@ public void appendAllParametersDetails(StringBuilder out, int indentCount, Strin
             WrappedParameter parameter = pd.getParameter();
             String description = pd.getDescription();
             boolean hasDescription = !description.isEmpty();
+            String descriptionKey = pd.getParameter().getParameter().descriptionKey();
+            descriptionKey = descriptionKey.isEmpty() ? "" : " <" + descriptionKey + ">";
 
             // First line, command name
             out.append(indent)
                     .append("  ")
                     .append(parameter.required() ? "* " : "  ")
-                    .append(pd.getNames())
+                    .append(pd.getLongestName())
+                    .append(descriptionKey)
+                    .append(Arrays.stream(pd.getParameter().names()).count() > 1 ? ", " + pd.getParameter().names()[1] + descriptionKey : "")
                     .append("\n");
 
             if (hasDescription) {
diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
index 3854f0d2fbb..b5b59d83917 100644
--- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
+++ b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java
@@ -55,33 +55,40 @@ public synchronized File specFile(FileUtil files) {
     @ParametersDelegate
     public PrintOptions print = new PrintOptions();
 
-    @Parameter(names="--branching-allowed", arity = 1, description="Number of branching events allowed before a forcible stop.")
+    @Parameter(names="--branching-allowed", descriptionKey = "number", arity = 1,
+            description="Number of branching events allowed before a forcible stop.")
     public int branchingAllowed = Integer.MAX_VALUE;
 
-    @Parameter(names={"--spec-module", "-sm"}, description="Name of module containing specification to prove")
+    @Parameter(names={"--spec-module", "-sm"}, descriptionKey = "name",
+            description="Name of module containing specification to prove")
     public String specModule;
 
-    @Parameter(names="--depth", description="The maximum number of computational steps to prove")
+    @Parameter(names="--depth", descriptionKey = "number",
+            description="The maximum number of computational steps to prove")
     public Integer depth;
 
-    @Parameter(names="--trusted", description="Mark this comma separated list of claims as [trusted]")
+    @Parameter(names="--trusted", descriptionKey = "labels",
+            description="Mark this comma separated list of claims as [trusted]")
     public List<String> trusted = null;
 
-    @Parameter(names="--exclude", description="Exclude this comma separated list of claims")
+    @Parameter(names="--exclude", descriptionKey = "labels", description="Exclude this comma separated list of claims")
     public List<String> exclude = null;
 
-    @Parameter(names="--claims", description="Only keep this comma separated list of claims")
+    @Parameter(names="--claims", descriptionKey = "labels", description="Only keep this comma separated list of claims")
     public List<String> claims = null;
 
-    @Parameter(names="--debugger", description="Launch proof in an interactive debugger. Currently only supported by the Haskell backend.")
+    @Parameter(names="--debugger",
+            description="Launch proof in an interactive debugger. Currently only supported by the Haskell backend.")
     public boolean debugger;
 
-    @Parameter(names="--debug-script", description="Run script passed in specified file when the debugger starts. Used with --debugger.")
+    @Parameter(names="--debug-script", descriptionKey = "file",
+            description="Run script passed in specified file when the debugger starts. Used with --debugger.")
     public String debugScript;
 
     @Parameter(names="--emit-json", description="Emit JSON serialized main definition for proving.")
     public boolean emitJson = false;
 
-    @Parameter(names="--emit-json-spec", description="If set, emit the JSON serialization of the spec module to the specified file.")
+    @Parameter(names="--emit-json-spec", descriptionKey = "file",
+            description="If set, emit the JSON serialization of the spec module to the specified file.")
     public String emitJsonSpec = null;
 }
diff --git a/kernel/src/main/java/org/kframework/main/GlobalOptions.java b/kernel/src/main/java/org/kframework/main/GlobalOptions.java
index d8ec2d7eeac..f0ae7d82c66 100644
--- a/kernel/src/main/java/org/kframework/main/GlobalOptions.java
+++ b/kernel/src/main/java/org/kframework/main/GlobalOptions.java
@@ -121,13 +121,13 @@ public boolean includesExceptionType(ExceptionType e) {
     @Parameter(names="--debug-warnings", description="Print debugging output messages and error/warning stack traces")
     public boolean debugWarnings = false;
 
-    @Parameter(names={"--warnings", "-w"}, converter=WarningsConverter.class, description="Warning level. Values: [all|normal|none]")
+    @Parameter(names={"--warnings", "-w"}, converter=WarningsConverter.class, description="Warning level. Values: [all|normal|none]", descriptionKey = "level")
     public Warnings warnings = Warnings.NORMAL;
 
-    @Parameter(names="-W", description="Enable specific warning categories. Values: [non-exhaustive-match|undeleted-temp-dir|missing-hook-java|missing-syntax-module|invalid-exit-code|deprecated-backend|invalid-config-var|future-error|unused-var|proof-lint|useless-rule|unresolved-function-symbol|malformed-markdown|invalidated-cache|unused-symbol|removed-anywhere]", converter=ExceptionTypeConverter.class)
+    @Parameter(names="-W", description="Enable specific warning categories. Values: [non-exhaustive-match|undeleted-temp-dir|missing-hook-java|missing-syntax-module|invalid-exit-code|deprecated-backend|invalid-config-var|future-error|unused-var|proof-lint|useless-rule|unresolved-function-symbol|malformed-markdown|invalidated-cache|unused-symbol|removed-anywhere]", descriptionKey = "warning", converter=ExceptionTypeConverter.class)
     public List<ExceptionType> enableWarnings = Collections.emptyList();
 
-    @Parameter(names="-Wno", description="Disable specific warning categories.", converter=ExceptionTypeConverter.class)
+    @Parameter(names="-Wno", description="Disable specific warning categories.", descriptionKey = "warning", converter=ExceptionTypeConverter.class)
     public List<ExceptionType> disableWarnings = Collections.emptyList();
 
     @Parameter(names={"--warnings-to-errors", "-w2e"}, description="Convert warnings to errors.")
@@ -139,13 +139,13 @@ public boolean includesExceptionType(ExceptionType e) {
                     "The wait time is the argument of this option, in format like 10ms/10s/10m/10h. " +
                     "Useful if K is interrupted by Ctrl+C, because it allows the backend to detect " +
                     "interruption and print diagnostics information. Currently interruption detection is implemented " +
-                    "in Java Backend. If K is invoked from KServer (e.g. Nailgun), the option is ignored.", hidden = true)
+                    "in Java Backend. If K is invoked from KServer (e.g. Nailgun), the option is ignored.", descriptionKey = "time", hidden = true)
     public Duration shutdownWaitTime;
 
     @Parameter(names = {"--timeout"}, converter = DurationConverter.class,
             description = "If option is set, timeout for this process, in format like 10ms/10s/10m/10h. " +
                     "Using this option is preferred compared to bash timeout command, which has known limitations " +
-                    "when invoked from scripts.", hidden = true)
+                    "when invoked from scripts.", descriptionKey = "duration", hidden = true)
     public Duration timeout;
 
     @Parameter(names={"--no-exc-wrap"}, description="Do not wrap exception messages to 80 chars. Keep long lines.", hidden = true)
@@ -155,6 +155,6 @@ public boolean debug() {
         return debug || debugWarnings;
     }
 
-    @Parameter(names={"--temp-dir"}, description="Put temp files in this location. Default is /tmp/.<tool>-xxx")
+    @Parameter(names={"--temp-dir"}, description="Put temp files in this location. Default is /tmp/.<tool>-xxx", descriptionKey = "path")
     public String tempDir = null;
 }
diff --git a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
index 9524069c865..c74146e45ea 100644
--- a/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
+++ b/kernel/src/main/java/org/kframework/unparser/PrintOptions.java
@@ -31,7 +31,8 @@ public PrintOptions(OutputModes output) {
     public PrintOptions(Void v) {
     }
 
-    @Parameter(names = "--color", description = "Use colors in output. Default is on.", converter=ColorModeConverter.class)
+    @Parameter(names = "--color", description = "Use colors in output. Default is on.", descriptionKey = "mode",
+            converter=ColorModeConverter.class)
     private ColorSetting color;
 
     public ColorSetting color(boolean ttyStdout, Map<String, String> env) {
@@ -65,10 +66,11 @@ public Class<ColorSetting> enumClass() {
         }
     }
 
-    @Parameter(names="--output-file", description="Store output in the file instead of displaying it.")
+    @Parameter(names="--output-file", description="Store output in the file instead of displaying it.",
+            descriptionKey = "file")
     public String outputFile;
 
-    @Parameter(names={"--output", "-o"}, converter=OutputModeConverter.class,
+    @Parameter(names={"--output", "-o"}, descriptionKey = "mode", converter=OutputModeConverter.class,
             description="How to display krun results. <mode> is either [pretty|program|kast|binary|json|latex|kore|none].")
     public OutputModes output = OutputModes.PRETTY;
 
@@ -84,16 +86,20 @@ public Class<OutputModes> enumClass() {
         }
     }
 
-    @Parameter(names={"--output-omit"}, listConverter=StringListConverter.class, description="KLabels to omit from the output.")
+    @Parameter(names={"--output-omit"}, descriptionKey = "KLabels", listConverter=StringListConverter.class,
+            description="KLabels to omit from the output.")
     public List<String> omittedKLabels = new ArrayList<String>();
 
-    @Parameter(names={"--output-tokenize"}, listConverter=StringListConverter.class, description="KLabels to tokenize underneath (reducing output size).")
+    @Parameter(names={"--output-tokenize"}, descriptionKey = "KLabels", listConverter=StringListConverter.class,
+            description="KLabels to tokenize underneath (reducing output size).")
     public List<String> tokenizedKLabels = new ArrayList<String>();
 
-    @Parameter(names={"--output-flatten"}, listConverter=StringListConverter.class, description="(Assoc) KLabels to flatten into one list.")
+    @Parameter(names={"--output-flatten"}, descriptionKey = "KLabels", listConverter=StringListConverter.class,
+            description="(Assoc) KLabels to flatten into one list.")
     public List<String> flattenedKLabels = new ArrayList<String>();
 
-    @Parameter(names={"--output-tokast"}, listConverter=StringListConverter.class, description="KLabels to output as KAST tokens.")
+    @Parameter(names={"--output-tokast"}, descriptionKey = "KLabels", listConverter=StringListConverter.class,
+            description="KLabels to output as KAST tokens.")
     public List<String> tokastKLabels = new ArrayList<String>();
 
     @Parameter(names={"--no-alpha-renaming"}, listConverter=StringListConverter.class, description="Do not alpha rename anonymous variables in output.")
diff --git a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
index fcd6b5a587e..8f9ed1b7b41 100644
--- a/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/DefinitionLoadingOptions.java
@@ -14,10 +14,10 @@ public DefinitionLoadingOptions(Void v) {}
 
     @Parameter(names={"--directory", "-d"}, description="[DEPRECATED] Path to the directory in which the kompiled " +
             "K definition resides. The default is the unique, only directory with the suffix '-kompiled' " +
-            "in the current directory.", hidden = true)
+            "in the current directory.", descriptionKey = "path", hidden = true)
     public String directory;
 
-    @Parameter(names={"--definition"}, description="Exact path to the kompiled directory.")
+    @Parameter(names={"--definition"}, description="Exact path to the kompiled directory.", descriptionKey = "path")
     public String inputDirectory;
 
     public DefinitionLoadingOptions(String dir) {
diff --git a/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java b/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java
index 74df0c44539..82f98421bc4 100644
--- a/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/InnerParsingOptions.java
@@ -18,6 +18,6 @@ public InnerParsingOptions() {}
     @Inject
     public InnerParsingOptions(Void v) {}
 
-    @Parameter(names="--profile-rule-parsing", description="Generate time in milliseconds to parse each rule in the semantics.", hidden = true)
+    @Parameter(names="--profile-rule-parsing", description="Store in this file time taken in ms to parse each rule in the semantics.", descriptionKey = "file", hidden = true)
     public String profileRules;
 }
diff --git a/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java b/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java
index bcd1d83c958..f5f5b4c6b25 100644
--- a/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/OuterParsingOptions.java
@@ -43,12 +43,12 @@ public synchronized File mainDefinitionFile(FileUtil files) {
     }
 
 
-    @Parameter(names="-I", description="Add a directory to the search path for requires statements.")
+    @Parameter(names="-I", description="Add a directory to the search path for requires statements.", descriptionKey = "path")
     public List<String> includes = new ArrayList<>();
 
     @Parameter(names="--no-prelude", description="Do not implicitly require prelude.md.", hidden = true)
     public boolean noPrelude = false;
 
-    @Parameter(names="--md-selector", description="Preprocessor: for .md files, select only the md code blocks that match the selector expression. Ex:'k&(!a|b)'.")
+    @Parameter(names="--md-selector", description="Preprocessor: for .md files, select only the md code blocks that match the selector expression. Ex:'k&(!a|b)'.", descriptionKey = "expression")
     public String mdSelector = "k";
 }
diff --git a/kernel/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java b/kernel/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java
index 750494b3e15..6d2fb6bc82b 100644
--- a/kernel/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java
@@ -13,9 +13,13 @@ public OutputDirectoryOptions() {}
     @Inject
     public OutputDirectoryOptions(Void v) {}
 
-    @Parameter(names={"--directory", "-d"}, description="[DEPRECATED] Path to the directory in which the output resides. An output can be either a kompiled K definition or a document which depends on the type of backend. The default is the directory containing the main definition file.", hidden = true)
+    @Parameter(names={"--directory", "-d"},
+            description="[DEPRECATED] Path to the directory in which the output resides. An output can be either a " +
+                    "kompiled K definition or a document which depends on the type of backend. The default is the " +
+                    "directory containing the main definition file.", descriptionKey = "path", hidden = true)
     public String directory;
 
-    @Parameter(names={"--output-definition", "-o"}, description="Path to the exact directory in which the output resides.")
+    @Parameter(names={"--output-definition", "-o"},
+            description="Path to the exact directory in which the output resides.", descriptionKey = "path")
     public String outputDirectory;
 }
diff --git a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
index db6fde3fbc4..b1acb132943 100644
--- a/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
+++ b/kernel/src/main/java/org/kframework/utils/options/SMTOptions.java
@@ -14,7 +14,8 @@ public SMTOptions() {}
     @Inject
     public SMTOptions(Void v) {}
 
-    @Parameter(names="--smt", converter=SMTSolverConverter.class, description="SMT solver to use for checking constraints. <solver> is one of [z3|none].", hidden = true)
+    @Parameter(names="--smt", descriptionKey = "executable", converter=SMTSolverConverter.class,
+            description="SMT solver to use for checking constraints. <executable> is one of [z3|none].", hidden = true)
     public SMTSolver smt = SMTSolver.Z3;
 
     public static class SMTSolverConverter extends BaseEnumConverter<SMTSolver> {
@@ -29,25 +30,30 @@ public Class<SMTSolver> enumClass() {
         }
     }
 
-    @Parameter(names="--ignore-missing-smtlib-warning", description="Suppress warning when SMTLib translation fails.", hidden = true)
+    @Parameter(names="--ignore-missing-smtlib-warning",
+            description="Suppress warning when SMTLib translation fails.", hidden = true)
     public boolean ignoreMissingSMTLibWarning = false;
 
-    @Parameter(names="--floats-as-po", description="Abstracts floating-point values as a partial order relation.", hidden = true)
+    @Parameter(names="--floats-as-po",
+            description="Abstracts floating-point values as a partial order relation.", hidden = true)
     public boolean floatsAsPO = false;
 
     @Parameter(names="--maps-as-int-array", description="Abstracts map values as an array of ints.", hidden = true)
     public boolean mapAsIntArray = false;
 
-    @Parameter(names={"--smt-prelude", "--smt_prelude"}, description="Path to the SMT prelude file.", hidden = true)
+    @Parameter(names={"--smt-prelude", "--smt_prelude"},
+            description="Path to the SMT prelude file.", descriptionKey = "path", hidden = true)
     public String smtPrelude;
 
-    @Parameter(names="--smt-timeout", description="Timeout for calls to the SMT solver, in milliseconds.", hidden = true)
+    @Parameter(names="--smt-timeout", descriptionKey = "milliseconds",
+            description="Timeout for calls to the SMT solver, in milliseconds.", hidden = true)
     public Integer smtTimeout = null;
 
     @Parameter(names="--z3-jni", description="Invokes Z3 as JNI library. Default is external process. " +
             "JNI is slightly faster, but can potentially lead to JVM crash.", hidden = true)
     public boolean z3JNI = false;
 
-    @Parameter(names="--z3-tactic", description="The solver tactic to use to check satisfiability in Z3.", hidden = true)
+    @Parameter(names="--z3-tactic", descriptionKey = "solver",
+            description="The path to solver tactic to use to check satisfiability in Z3.", hidden = true)
     public String z3Tactic;
 }
diff --git a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala b/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala
index c61f5bb76f8..0dc7637b627 100644
--- a/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala
+++ b/kore/src/main/scala/org/kframework/parser/kore/parser/TextToKore.scala
@@ -545,6 +545,7 @@ class TextToKore(b: Builders = DefaultBuilders) {
                     (p1: kore.Pattern, p2: kore.Pattern) => b.Or(s, p1, p2)
                 }
               case c => // variable or application
+                scanner.putback(c)
                 val id = parseId() // previousParsingLevel is set here
                 consumeWithLeadingWhitespaces("{")
                 val params = parseList(() => parseSort(parsingLevel = previousParsingLevel), ',', '}')
@@ -579,6 +580,7 @@ class TextToKore(b: Builders = DefaultBuilders) {
                     (p1: kore.Pattern, p2: kore.Pattern) => b.Or(s, p1, p2)
                 }
               case c => // variable or application
+                scanner.putback(c)
                 val id = parseId() // previousParsingLevel is set here
                 consumeWithLeadingWhitespaces("{")
                 val params = parseList(() => parseSort(parsingLevel = previousParsingLevel), ',', '}')
diff --git a/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala b/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala
index d6143b94ad5..4cee235b858 100644
--- a/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala
+++ b/kore/src/test/scala/org/kframework/parser/kore/parser/TextToKoreTest.scala
@@ -31,4 +31,17 @@ class TextToKoreTest {
     Assert.assertEquals(b.And(int, b.DomainValue(int, "1"), b.And(int, b.DomainValue(int, "2"), b.DomainValue(int, "3"))), ast2)
   }
 
+  @Test def testAssocApplication(): Unit = {
+    val parser = new TextToKore()
+    val int = b.CompoundSort("SortInt", Seq())
+
+    val koreLeft = "\\left-assoc{}(Lbl'Unds'Map'Unds{}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"1\")))"
+    val astLeft = parser.parsePattern(koreLeft)
+    Assert.assertEquals(b.Application(b.SymbolOrAlias("Lbl'Unds'Map'Unds", Seq()), Seq(b.DomainValue(int, "1"), b.DomainValue(int, "1"))), astLeft)
+
+    val koreRight = "\\right-assoc{}(Lbl'Unds'Map'Unds{}(\\dv{SortInt{}}(\"1\"), \\dv{SortInt{}}(\"1\")))"
+    val astRight = parser.parsePattern(koreRight)
+    Assert.assertEquals(b.Application(b.SymbolOrAlias("Lbl'Unds'Map'Unds", Seq()), Seq(b.DomainValue(int, "1"), b.DomainValue(int, "1"))), astRight)
+  }
+
 }
diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
index ceab9d5c8a3..e81ce93f110 100644
--- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
+++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMKompileOptions.java
@@ -15,7 +15,7 @@ public class LLVMKompileOptions {
     @Parameter(names="--enable-llvm-debug", description="Enable debugging support for the LLVM backend.")
     public boolean debug = false;
 
-    @Parameter(names="-ccopt", description="Add a command line option to the compiler invocation for the llvm backend.", listConverter=SingletonListConverter.class, hidden = true)
+    @Parameter(names="-ccopt", description="Add a command line option to the compiler invocation for the llvm backend.", descriptionKey = "options", listConverter=SingletonListConverter.class, hidden = true)
     public List<String> ccopts = new ArrayList<>();
 
     public static class SingletonListConverter implements IStringConverter<List<String>> {
@@ -25,13 +25,13 @@ public List<String> convert(String str) {
         }
     }
 
-    @Parameter(names="--heuristic", description="A string of single characters representing a sequence of heuristics to use during pattern matching compilation. Valid choices are f, d, b, a, l, r, n, p, q, _, N, L, R.", hidden = true)
+    @Parameter(names="--heuristic", description="A string of single characters representing a sequence of heuristics to use during pattern matching compilation. Valid choices are f, d, b, a, l, r, n, p, q, _, N, L, R.", descriptionKey = "heuristics", hidden = true)
     public String heuristic = "qbaL";
 
     @Parameter(names="--iterated", description="Generate iterated pattern matching optimization; time-consuming but significantly reduces matching time.", hidden = true)
     public boolean iterated = false;
 
-    @Parameter(names="--iterated-threshold", description="Threshold heuristic to use when choosing which axioms to optimize. A value of 0 turns the optimization off; a value of 1 turns the optimization on for every axiom. Values in between (expressed as a fraction of two integers, e.g. 1/2), control the aggressiveness of the optimization. Higher values increase compilation times extremely, but also increase the effectiveness of the optimization. Consider decreasing this threshold if compilation is too slow.", hidden = true)
+    @Parameter(names="--iterated-threshold", description="Threshold heuristic to use when choosing which axioms to optimize. A value of 0 turns the optimization off; a value of 1 turns the optimization on for every axiom. Values in between (expressed as a fraction of two integers, e.g. 1/2), control the aggressiveness of the optimization. Higher values increase compilation times extremely, but also increase the effectiveness of the optimization. Consider decreasing this threshold if compilation is too slow.", descriptionKey = "value", hidden = true)
     public String iteratedThreshold = "1/2";
 
     @Parameter(names="--no-llvm-kompile", description="Do not invoke llvm-kompile. Useful if you want to do it yourself when building with the LLVM backend.", hidden = true)
@@ -40,9 +40,9 @@ public List<String> convert(String str) {
     @Parameter(names="--enable-search", description="By default, to reduce compilation time, `krun --search` is disabled on the LLVM backend. Pass this flag to enable it.")
     public boolean enableSearch;
 
-    @Parameter(names="--llvm-kompile-type", description="Specifies the llvm backend's output type. Valid choices are main (build an interpreter), library (build an interpreter, but don't link a main function), search (same as main, but the interpreter does search instead of single-path execution), static (same as library, but no '-l' flags are passed during linking. Used for making a partially linked object file) and python (build a Python bindings module for this definition)", hidden = true)
+    @Parameter(names="--llvm-kompile-type", description="Specifies the llvm backend's output type. Valid choices are main (build an interpreter), library (build an interpreter, but don't link a main function), search (same as main, but the interpreter does search instead of single-path execution), static (same as library, but no '-l' flags are passed during linking. Used for making a partially linked object file) and python (build a Python bindings module for this definition)", descriptionKey = "type", hidden = true)
     public String llvmKompileType = "main";
 
-    @Parameter(names="--llvm-kompile-output", description="Name of the output binary from the llvm backend.", hidden = true)
+    @Parameter(names="--llvm-kompile-output", description="Name of the output binary from the llvm backend.", descriptionKey = "file", hidden = true)
     public String llvmKompileOutput = null;
 }
diff --git a/web/toc.md b/web/toc.md
index 38dc616eccc..64f77e088d3 100644
--- a/web/toc.md
+++ b/web/toc.md
@@ -41,6 +41,24 @@ output:
     - [Lesson 1.20: K Backends and the Haskell Backend](/k-distribution/k-tutorial/1_basic/20_backends/README.md)
     - [Lesson 1.21: Unification and Symbolic Execution](/k-distribution/k-tutorial/1_basic/21_symbolic_execution/README.md)
     - [Lesson 1.22: K Deductive Verification](/k-distribution/k-tutorial/1_basic/22_proofs/README.md)
+  - [Section 2: Intermediate K Concepts](/k-distribution/k-tutorial/2_intermediate/README.md)
+    - [Lesson 2.1: Macros, Aliases, and Anywhere Rules](/k-distribution/k-tutorial/2_intermediate/01_macros/README.md)
+    - [Lesson 2.2: Fresh Constants](/k-distribution/k-tutorial/2_intermediate/02_fresh_constants/README.md)
+    - [Lesson 2.3: KLabels and Abstract Syntax](/k-distribution/k-tutorial/2_intermediate/03_klabels/README.md)
+    - [Lesson 2.4: Overloaded Symbols](/k-distribution/k-tutorial/2_intermediate/04_overloading/README.md)
+    - [Lesson 2.5: Matching Logic Connectives and #Or Patterns](/k-distribution/k-tutorial/2_intermediate/05_matching_logic/README.md)
+    - [Lesson 2.6: Function Context](/k-distribution/k-tutorial/2_intermediate/06_function_context/README.md)
+    - [Lesson 2.7: Record Productions and Named Nonterminals](/k-distribution/k-tutorial/2_intermediate/07_record_productions/README.md)
+    - [Lesson 2.8: #fun and #let](/k-distribution/k-tutorial/2_intermediate/08_fun_and_let/README.md)
+    - [Lesson 2.9: #as Patterns](/k-distribution/k-tutorial/2_intermediate/09_as/README.md)
+    - [Lesson 2.10: The Matching Operators, :=K and :/=K](/k-distribution/k-tutorial/2_intermediate/10_matching_operator/README.md)
+    - [Lesson 2.11: Uncommon Evaluation Order Concepts](/k-distribution/k-tutorial/2_intermediate/11_evaluation_order/README.md)
+    - [Lesson 2.12: IEEE 754 Floating Point and Fixed Width Integers](/k-distribution/k-tutorial/2_intermediate/12_floats_and_machine_ints/README.md)
+    - [Lesson 2.13: Alpha-renaming-aware Substitution](/k-distribution/k-tutorial/2_intermediate/13_substitution/README.md)
+    - [Lesson 2.14: File I/O](/k-distribution/k-tutorial/2_intermediate/14_io/README.md)
+    - [Lesson 2.15: String Buffers and Byte Sequences](/k-distribution/k-tutorial/2_intermediate/15_string_buffers_and_bytes/README.md)
+    - [Lesson 2.16: The Intermediate Language of K, KORE](/k-distribution/k-tutorial/2_intermediate/16_kore/README.md)
+    - [Lesson 2.17: Debugging Proofs using the Haskell Backend REPL](/k-distribution/k-tutorial/2_intermediate/17_debugging_proofs/README.md)
 - [K User Manual](/docs/user_manual.md)
 - [K Cheat Sheet](/docs/cheat_sheet.md)
 - [K Tool Reference](/docs/ktools.md)