diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000000000000000000000000000000000000..ba1ab9c5716effe16d3cb7d8cf7ccca059bfaa06
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,35 @@
+All files in this development are distributed under the terms of the
+3-clause BSD license (https://opensource.org/licenses/BSD-3-Clause), included below.
+
+This development also includes files based on the Iris development
+(https://gitlab.mpi-sws.org/iris/iris) and licensed under the 3-clause BSD license:
+  Copyright: Iris developers and contributors
+
+This development also includes files based on the ReLoC development
+(https://gitlab.mpi-sws.org/iris/reloc) and licensed under the 3-clause BSD license:
+  Copyright: ReLoC developers and contributors
+
+
+------------------------------------------------------------------------------
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+    * Neither the name of the copyright holder nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/STRUCTURE.md b/STRUCTURE.md
index 07d1a0509079401d0e12bcd2f8884d74afc80d40..111567ff63d369f9d36c203e3c1a5fecfde4ed63 100644
--- a/STRUCTURE.md
+++ b/STRUCTURE.md
@@ -2,6 +2,11 @@
 
 This document roughly maps the lecture notes and exercises to the Coq development.
 
+## Basic structure
+Chapters 1-4 are included in the `theories/type_systems` folder.
+Chapters 5-10 are included in the `theories/program_logics` folder.
+All of the paths given below are to be understood relative to these folders.
+
 ## Chapter 1
 * The `warmup` folder contains a quick reminder of some concepts of Coq as well as an introduction to some features of `stdpp`.
 * The `stlc` folder contains an implementation of the untyped lambda-calculus and the simply-typed lambda-calculus, with different reduction semantics, including syntactic and semantic type safety proofs.
@@ -81,15 +86,15 @@ Special notes on some exercises:
 * Exercise 56 is not present in the Coq development.
 
 ## Chapter 5
-* The development for Chapter 5 can be found in the file `axiomatic/hoare.v`.
+* The development for Chapter 5 can be found in the file `hoare.v`.
 * Exercises are provided in-line with the material.
 
 ## Chapter 6
-* The development for Chapter 6 can be found in the file `axiomatic/ipm.v`.
+* The development for Chapter 6 can be found in the file `ipm.v`.
 * Exercises are provided in-line with the material.
 
 ## Chapter 7
-* The development for Chapter 7 can be found in the folder `axiomatic/logrel.v`, in files:
+* The development for Chapter 7 can be found in the folder `logrel.v`, in files:
   + `syntactic.v` defines a syntactic type system for our language.
   + `logrel.v` defines the logical relation and proves the fundamental theorem.
   + `adequacy.v` proves adequacy of the logical relation.
@@ -101,19 +106,19 @@ Special notes on some exercises:
 
 | Section | Coq entry point                                                   |
 |---------|-------------------------------------------------------------------|
-| 8.0     | `axiomatic/logrel/ghost_state.v`                                  |
-| 8.1     | `axiomatic/resource_algebras.v`                                   |
-| 8.2     | `axiomatic/resource_algebras.v`                                   |
-| 8.3     | `axiomatic/resource_algebras.v`                                   |
-| 8.4     | `axiomatic/reloc` and `axiomatic/fupd.v`                          |
+| 8.0     | `logrel/ghost_state.v`                                            |
+| 8.1     | `resource_algebras.v`                                             |
+| 8.2     | `resource_algebras.v`                                             |
+| 8.3     | `resource_algebras.v`                                             |
+| 8.4     | `reloc` and `fupd.v`                                              |
 
 In particular, for ReLoC/ the binary logical relation, the following files are of interest:
-- `axiomatic/reloc/ghost_state.v` defines the ghost theory (Section 8.4.3),
-- `axiomatic/fupd.v` introduces the fancy update modality (Section 8.4.2),
-- `axiomatic/reloc/src_rules.v` proves the ghost program rules (Section 8.4.1/8.4.3),
-- `axiomatic/reloc/logrel.v` defines the logical relation (Section 8.4.1),
-- `axiomatic/reloc/fundamental.v` proves the fundamental property (Section 8.4.4),
-- `axiomatic/reloc/adequacy.v` proves the contextual refinement result (Section 8.4.4).
+- `reloc/ghost_state.v` defines the ghost theory (Section 8.4.3),
+- `fupd.v` introduces the fancy update modality (Section 8.4.2),
+- `reloc/src_rules.v` proves the ghost program rules (Section 8.4.1/8.4.3),
+- `reloc/logrel.v` defines the logical relation (Section 8.4.1),
+- `reloc/fundamental.v` proves the fundamental property (Section 8.4.4),
+- `reloc/adequacy.v` proves the contextual refinement result (Section 8.4.4).
 
 Notes on exercises:
 * Exercise 116 (coming up with an interesting refinement and proving it) is not present in the Coq development.
@@ -126,10 +131,10 @@ Notes on exercises:
 
 | Section | Coq entry point                                                   |
 |---------|-------------------------------------------------------------------|
-| 10.0    | `axiomatic/concurrency.v`                                         |
-| 10.1    | `axiomatic/concurrency.v`                                         |
-| 10.2    | `axiomatic/concurrency.v`                                         |
-| 10.3    | `axiomatic/concurrent_logrel/`                                    |
+| 10.0    | `concurrency.v`                                                   |
+| 10.1    | `concurrency.v`                                                   |
+| 10.2    | `concurrency.v`                                                   |
+| 10.3    | `concurrent_logrel/`                                              |
 
 Notes on exercises:
 * The exercise for verifying the channel implementation (Section 10.3) is located in `axiomatic/concurrency.v`.
diff --git a/_CoqProject b/_CoqProject
index ddc04b64e2b2bf0d1addf8b06556a3f535f66cad..e67a908553d8de6c443872bfaa02c49a0c7c4ef2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,6 @@
--Q theories semantics
+-Q theories/lib semantics.lib
+-Q theories/program_logics  semantics.pl
+-Q theories/type_systems semantics.ts
 # We sometimes want to locally override notation, and there is no good way to do that with scopes.
 -arg -w -arg -notation-overridden
 # Cannot use non-canonical projections as it causes massive unification failures
@@ -14,129 +16,112 @@ theories/lib/debruijn.v
 theories/lib/facts.v
 
 # STLC
-theories/stlc/lang.v
-theories/stlc/notation.v
-theories/stlc/untyped.v
-theories/stlc/types.v
-theories/stlc/logrel.v
-theories/stlc/parallel_subst.v
+theories/type_systems/stlc/lang.v
+theories/type_systems/stlc/notation.v
+theories/type_systems/stlc/untyped.v
+theories/type_systems/stlc/types.v
+theories/type_systems/stlc/logrel.v
+theories/type_systems/stlc/parallel_subst.v
 
 # Extended STLC
-theories/stlc_extended/lang.v
-theories/stlc_extended/notation.v
-theories/stlc_extended/types.v
-theories/stlc_extended/bigstep.v
-theories/stlc_extended/parallel_subst.v
-theories/stlc_extended/logrel.v
+theories/type_systems/stlc_extended/lang.v
+theories/type_systems/stlc_extended/notation.v
+theories/type_systems/stlc_extended/types.v
+theories/type_systems/stlc_extended/bigstep.v
+theories/type_systems/stlc_extended/parallel_subst.v
+theories/type_systems/stlc_extended/logrel.v
 
 
 
 # System F
-theories/systemf/lang.v
-theories/systemf/notation.v
-theories/systemf/types.v
-theories/systemf/tactics.v
-theories/systemf/bigstep.v
-theories/systemf/church_encodings.v
-theories/systemf/parallel_subst.v
-theories/systemf/logrel.v
-theories/systemf/free_theorems.v
-theories/systemf/binary_logrel.v
-theories/systemf/existential_invariants.v
+theories/type_systems/systemf/lang.v
+theories/type_systems/systemf/notation.v
+theories/type_systems/systemf/types.v
+theories/type_systems/systemf/tactics.v
+theories/type_systems/systemf/bigstep.v
+theories/type_systems/systemf/church_encodings.v
+theories/type_systems/systemf/parallel_subst.v
+theories/type_systems/systemf/logrel.v
+theories/type_systems/systemf/free_theorems.v
+theories/type_systems/systemf/binary_logrel.v
+theories/type_systems/systemf/existential_invariants.v
 
 
 # SystemF-Mu
-theories/systemf_mu/lang.v
-theories/systemf_mu/notation.v
-theories/systemf_mu/types.v
-theories/systemf_mu/tactics.v
-theories/systemf_mu/pure.v
-theories/systemf_mu/untyped_encoding.v
-theories/systemf_mu/parallel_subst.v
-theories/systemf_mu/logrel.v
-theories/systemf_mu/z_combinator.v
+theories/type_systems/systemf_mu/lang.v
+theories/type_systems/systemf_mu/notation.v
+theories/type_systems/systemf_mu/types.v
+theories/type_systems/systemf_mu/tactics.v
+theories/type_systems/systemf_mu/pure.v
+theories/type_systems/systemf_mu/untyped_encoding.v
+theories/type_systems/systemf_mu/parallel_subst.v
+theories/type_systems/systemf_mu/logrel.v
+theories/type_systems/systemf_mu/z_combinator.v
 
 # SystemF + Mu + State
-theories/systemf_mu_state/locations.v
-theories/systemf_mu_state/lang.v
-theories/systemf_mu_state/notation.v
-theories/systemf_mu_state/types.v
-theories/systemf_mu_state/tactics.v
-theories/systemf_mu_state/execution.v
-theories/systemf_mu_state/parallel_subst.v
-theories/systemf_mu_state/logrel.v
-theories/systemf_mu_state/mutbit.v
+theories/type_systems/systemf_mu_state/locations.v
+theories/type_systems/systemf_mu_state/lang.v
+theories/type_systems/systemf_mu_state/notation.v
+theories/type_systems/systemf_mu_state/types.v
+theories/type_systems/systemf_mu_state/tactics.v
+theories/type_systems/systemf_mu_state/execution.v
+theories/type_systems/systemf_mu_state/parallel_subst.v
+theories/type_systems/systemf_mu_state/logrel.v
+theories/type_systems/systemf_mu_state/mutbit.v
 
 
 
 # Program logic library
-theories/axiomatic/program_logic/notation.v
-theories/axiomatic/program_logic/sequential_wp.v
-theories/axiomatic/program_logic/lifting.v
-theories/axiomatic/program_logic/ectx_lifting.v
-theories/axiomatic/program_logic/adequacy.v
-theories/axiomatic/heap_lang/primitive_laws.v
-theories/axiomatic/heap_lang/derived_laws.v
-theories/axiomatic/heap_lang/proofmode.v
-theories/axiomatic/heap_lang/adequacy.v
-theories/axiomatic/heap_lang/primitive_laws_nolater.v
+theories/program_logics/program_logic/notation.v
+theories/program_logics/program_logic/sequential_wp.v
+theories/program_logics/program_logic/lifting.v
+theories/program_logics/program_logic/ectx_lifting.v
+theories/program_logics/program_logic/adequacy.v
+theories/program_logics/heap_lang/primitive_laws.v
+theories/program_logics/heap_lang/derived_laws.v
+theories/program_logics/heap_lang/proofmode.v
+theories/program_logics/heap_lang/adequacy.v
+theories/program_logics/heap_lang/primitive_laws_nolater.v
 
 
 # Program logic chapter
-theories/axiomatic/hoare_lib.v
-theories/axiomatic/hoare.v
-theories/axiomatic/ipm.v
-theories/axiomatic/later_loeb.v
+theories/program_logics/hoare_lib.v
+theories/program_logics/hoare.v
+theories/program_logics/ipm.v
+theories/program_logics/later_loeb.v
 
-theories/axiomatic/invariant_lib.v
+theories/program_logics/invariant_lib.v
 # logrel
-theories/axiomatic/logrel/syntactic.v
-theories/axiomatic/logrel/notation.v
-theories/axiomatic/logrel/persistent_pred.v
-theories/axiomatic/logrel/logrel.v
-theories/axiomatic/logrel/adequacy.v
-theories/axiomatic/logrel/ghost_state_lib.v
-theories/axiomatic/logrel/ghost_state.v
+theories/program_logics/logrel/syntactic.v
+theories/program_logics/logrel/notation.v
+theories/program_logics/logrel/persistent_pred.v
+theories/program_logics/logrel/logrel.v
+theories/program_logics/logrel/adequacy.v
+theories/program_logics/logrel/ghost_state_lib.v
+theories/program_logics/logrel/ghost_state.v
 
 
 # resources
-theories/axiomatic/ra_lib.v
-#theories/axiomatic/resource_algebras.v
+theories/program_logics/ra_lib.v
+theories/program_logics/resource_algebras.v
 
-theories/axiomatic/fupd.v
+theories/program_logics/fupd.v
 
 # reloc
-theories/axiomatic/reloc/ghost_state.v
-theories/axiomatic/reloc/src_rules.v
-theories/axiomatic/reloc/persistent_bipred.v
-theories/axiomatic/reloc/notation.v
-theories/axiomatic/reloc/proofmode.v
-theories/axiomatic/reloc/syntactic.v
-theories/axiomatic/reloc/logrel.v
-theories/axiomatic/reloc/fundamental.v
-theories/axiomatic/reloc/adequacy.v
-theories/axiomatic/reloc/contextual_refinement.v
+theories/program_logics/reloc/ghost_state.v
+theories/program_logics/reloc/src_rules.v
+theories/program_logics/reloc/persistent_bipred.v
+theories/program_logics/reloc/notation.v
+theories/program_logics/reloc/proofmode.v
+theories/program_logics/reloc/syntactic.v
+theories/program_logics/reloc/logrel.v
+theories/program_logics/reloc/fundamental.v
+theories/program_logics/reloc/adequacy.v
+theories/program_logics/reloc/contextual_refinement.v
 
 # concurrency
-theories/axiomatic/concurrency.v
-theories/axiomatic/concurrent_logrel/syntactic.v
-theories/axiomatic/concurrent_logrel/logrel.v
-theories/axiomatic/concurrent_logrel/adequacy.v
+theories/program_logics/concurrency.v
+theories/program_logics/concurrent_logrel/syntactic.v
+theories/program_logics/concurrent_logrel/logrel.v
+theories/program_logics/concurrent_logrel/adequacy.v
 
-
-
-# By removing the # below, you can add the exercise sheets to make
-# theories/warmup/sheet0.v
-
-#theories/stlc/exercises01.v
-
-#theories/stlc/exercises02.v
-#
-#theories/systemf/exercises03.v
-#
-#
-#theories/stlc/cbn_logrel.v
-#theories/systemf/exercices04.v
-#theories/systemf/exercises05.v
-#theories/systemf_mu/exercises06.v
-#theories/systemf_mu_state/exercises07.v
diff --git a/theories/axiomatic/concurrency.v b/theories/program_logics/concurrency.v
similarity index 100%
rename from theories/axiomatic/concurrency.v
rename to theories/program_logics/concurrency.v
diff --git a/theories/axiomatic/concurrent_logrel/adequacy.v b/theories/program_logics/concurrent_logrel/adequacy.v
similarity index 93%
rename from theories/axiomatic/concurrent_logrel/adequacy.v
rename to theories/program_logics/concurrent_logrel/adequacy.v
index 1749ef77d1d6e4e6a54481851e0a6593f17ee850..f366ba73be48524cbaf26e856bc8dcf793cc0560 100644
--- a/theories/axiomatic/concurrent_logrel/adequacy.v
+++ b/theories/program_logics/concurrent_logrel/adequacy.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation primitive_laws adequacy.
-From semantics.axiomatic.concurrent_logrel Require Import syntactic logrel.
+From semantics.pl.concurrent_logrel Require Import syntactic logrel.
 From iris.prelude Require Import options.
 
 
diff --git a/theories/axiomatic/concurrent_logrel/logrel.v b/theories/program_logics/concurrent_logrel/logrel.v
similarity index 99%
rename from theories/axiomatic/concurrent_logrel/logrel.v
rename to theories/program_logics/concurrent_logrel/logrel.v
index 9d25f8843d68d792646d90d3989f2ecbe2c66681..aa4c85db9db2add869e75beb186521716c4982f1 100644
--- a/theories/axiomatic/concurrent_logrel/logrel.v
+++ b/theories/program_logics/concurrent_logrel/logrel.v
@@ -2,9 +2,9 @@ From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation primitive_laws proofmode.
 From iris.heap_lang Require Import metatheory.
 From iris.base_logic Require Import invariants mono_nat.
-From semantics.axiomatic.logrel Require Import notation persistent_pred.
-From semantics.axiomatic Require concurrency.
-From semantics.axiomatic.concurrent_logrel Require Import syntactic.
+From semantics.pl.logrel Require Import notation persistent_pred.
+From semantics.pl Require concurrency.
+From semantics.pl.concurrent_logrel Require Import syntactic.
 From iris.prelude Require Import options.
 
 
diff --git a/theories/axiomatic/concurrent_logrel/syntactic.v b/theories/program_logics/concurrent_logrel/syntactic.v
similarity index 99%
rename from theories/axiomatic/concurrent_logrel/syntactic.v
rename to theories/program_logics/concurrent_logrel/syntactic.v
index bc96c8b4ebb0c2749f05d8fad2a9aff1b8a9cce7..f894ba3d584e82c85c0f6ea00cc240f4cecd1ae6 100644
--- a/theories/axiomatic/concurrent_logrel/syntactic.v
+++ b/theories/program_logics/concurrent_logrel/syntactic.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Import lang notation.
 From iris.heap_lang Require Export metatheory.
-From semantics.axiomatic.logrel Require Import notation.
+From semantics.pl.logrel Require Import notation.
 From Autosubst Require Export Autosubst.
 From stdpp Require Import gmap.
 From iris.prelude Require Import options.
diff --git a/theories/axiomatic/fupd.v b/theories/program_logics/fupd.v
similarity index 91%
rename from theories/axiomatic/fupd.v
rename to theories/program_logics/fupd.v
index c3ff402dc8e3e89cbf24dcb592fa62e6c0b4b7a4..870b73cedc69b4af071e228e81bb7962f2187c43 100644
--- a/theories/axiomatic/fupd.v
+++ b/theories/program_logics/fupd.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
-From semantics.axiomatic Require Export invariant_lib.
-From semantics.axiomatic.program_logic Require Export notation.
-From semantics.axiomatic.heap_lang Require Export primitive_laws proofmode.
+From semantics.pl Require Export invariant_lib.
+From semantics.pl.program_logic Require Export notation.
+From semantics.pl.heap_lang Require Export primitive_laws proofmode.
 From iris.prelude Require Import options.
 
 
diff --git a/theories/axiomatic/heap_lang/adequacy.v b/theories/program_logics/heap_lang/adequacy.v
similarity index 85%
rename from theories/axiomatic/heap_lang/adequacy.v
rename to theories/program_logics/heap_lang/adequacy.v
index 979755a7419e20f5ca3b14bfe6a91329a1543b26..ed45a848f7efed590f36f4916ad1a1bf5d3c6ca2 100644
--- a/theories/axiomatic/heap_lang/adequacy.v
+++ b/theories/program_logics/heap_lang/adequacy.v
@@ -1,8 +1,8 @@
 From iris.algebra Require Import auth.
 From iris.proofmode Require Import proofmode.
-From semantics.axiomatic.program_logic Require Export sequential_wp adequacy.
+From semantics.pl.program_logic Require Export sequential_wp adequacy.
 From iris.heap_lang Require Import notation.
-From semantics.axiomatic.heap_lang Require Export proofmode.
+From semantics.pl.heap_lang Require Export proofmode.
 From iris.prelude Require Import options.
 
 Class heapGpreS Σ := HeapGpreS {
diff --git a/theories/axiomatic/heap_lang/derived_laws.v b/theories/program_logics/heap_lang/derived_laws.v
similarity index 98%
rename from theories/axiomatic/heap_lang/derived_laws.v
rename to theories/program_logics/heap_lang/derived_laws.v
index 0e52139c648412277575ca63a14f5958c87b415f..5bf05db5f3614486c3555818c496c55d3ef3b719 100644
--- a/theories/axiomatic/heap_lang/derived_laws.v
+++ b/theories/program_logics/heap_lang/derived_laws.v
@@ -8,7 +8,7 @@ From stdpp Require Import fin_maps.
 From iris.bi Require Import lib.fractional.
 From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Import tactics notation.
-From semantics.axiomatic.heap_lang Require Export primitive_laws.
+From semantics.pl.heap_lang Require Export primitive_laws.
 From iris.prelude Require Import options.
 
 (** The [array] connective is a version of [mapsto] that works
diff --git a/theories/axiomatic/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
similarity index 97%
rename from theories/axiomatic/heap_lang/primitive_laws.v
rename to theories/program_logics/heap_lang/primitive_laws.v
index a9602de9387447360317c5f47ecaa08964ff24f2..892c2d4a09b84789ed6cda58d8ba0742b5f00da6 100644
--- a/theories/axiomatic/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -4,11 +4,11 @@ the Iris lifting lemmas. *)
 From iris.proofmode Require Import proofmode.
 From iris.bi.lib Require Import fractional.
 From iris.base_logic.lib Require Export gen_heap.
-From semantics.axiomatic.program_logic Require Export sequential_wp.
-From semantics.axiomatic.program_logic Require Import ectx_lifting.
+From semantics.pl.program_logic Require Export sequential_wp.
+From semantics.pl.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export class_instances.
 From iris.heap_lang Require Import tactics notation.
-From semantics.axiomatic.program_logic Require Export notation.
+From semantics.pl.program_logic Require Export notation.
 From iris.prelude Require Import options.
 
 Class heapGS Σ := HeapGS {
diff --git a/theories/axiomatic/heap_lang/primitive_laws_nolater.v b/theories/program_logics/heap_lang/primitive_laws_nolater.v
similarity index 93%
rename from theories/axiomatic/heap_lang/primitive_laws_nolater.v
rename to theories/program_logics/heap_lang/primitive_laws_nolater.v
index e153591be398ae97aa7d02acc19598c74b01a7a1..cce84ffe3d2a79f621fe5bdc44c0737f6eb6f152 100644
--- a/theories/axiomatic/heap_lang/primitive_laws_nolater.v
+++ b/theories/program_logics/heap_lang/primitive_laws_nolater.v
@@ -1,10 +1,10 @@
 From stdpp Require Import fin_maps.
 From iris.proofmode Require Import proofmode.
 From iris.bi.lib Require Import fractional.
-From semantics.axiomatic.heap_lang Require Export primitive_laws derived_laws.
+From semantics.pl.heap_lang Require Export primitive_laws derived_laws.
 From iris.base_logic.lib Require Export gen_heap gen_inv_heap.
-From semantics.axiomatic.program_logic Require Export sequential_wp.
-From semantics.axiomatic.program_logic Require Import ectx_lifting.
+From semantics.pl.program_logic Require Export sequential_wp.
+From semantics.pl.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export class_instances.
 From iris.heap_lang Require Import tactics notation.
 From iris.prelude Require Import options.
diff --git a/theories/axiomatic/heap_lang/proofmode.v b/theories/program_logics/heap_lang/proofmode.v
similarity index 99%
rename from theories/axiomatic/heap_lang/proofmode.v
rename to theories/program_logics/heap_lang/proofmode.v
index 3f99cf359c7c51bf46fe4989cb25bc65d4dcd486..77631c1c92dacfb831a28f9b99aadc3c98b57879 100644
--- a/theories/axiomatic/heap_lang/proofmode.v
+++ b/theories/program_logics/heap_lang/proofmode.v
@@ -2,8 +2,8 @@ From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics.
 From iris.heap_lang Require Import notation.
-From semantics.axiomatic.heap_lang Require Export derived_laws.
-From semantics.axiomatic.program_logic Require Export notation.
+From semantics.pl.heap_lang Require Export derived_laws.
+From semantics.pl.program_logic Require Export notation.
 From iris.prelude Require Import options.
 Import uPred.
 
diff --git a/theories/axiomatic/hoare.v b/theories/program_logics/hoare.v
similarity index 99%
rename from theories/axiomatic/hoare.v
rename to theories/program_logics/hoare.v
index e269ba1b768463a7132ea608e4e60b3729f37695..48b28d9fac6c27e5d9da94c130b96f23a14160e7 100644
--- a/theories/axiomatic/hoare.v
+++ b/theories/program_logics/hoare.v
@@ -1,7 +1,7 @@
 From iris.prelude Require Import options.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
-From semantics.axiomatic Require Export hoare_lib.
+From semantics.pl Require Export hoare_lib.
 
 Import hoare.
 Implicit Types
diff --git a/theories/axiomatic/hoare_lib.v b/theories/program_logics/hoare_lib.v
similarity index 99%
rename from theories/axiomatic/hoare_lib.v
rename to theories/program_logics/hoare_lib.v
index 25ad19855c26af80cbaa8fa81b735692e9a55dce..f8f3007cb19f56bb6f3c5fd32b0dcd1ffddfed6b 100644
--- a/theories/axiomatic/hoare_lib.v
+++ b/theories/program_logics/hoare_lib.v
@@ -2,8 +2,8 @@ From iris.prelude Require Import options.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.base_logic Require Export invariants.
-From semantics.axiomatic.heap_lang Require Export primitive_laws_nolater.
-From semantics.axiomatic.heap_lang Require Import adequacy proofmode.
+From semantics.pl.heap_lang Require Export primitive_laws_nolater.
+From semantics.pl.heap_lang Require Import adequacy proofmode.
 
 
 Module hoare.
diff --git a/theories/axiomatic/invariant_lib.v b/theories/program_logics/invariant_lib.v
similarity index 85%
rename from theories/axiomatic/invariant_lib.v
rename to theories/program_logics/invariant_lib.v
index f650563862c1b4cac3844ce2683004cf6ba280f9..3c3be0ae867c8f111d8b2ba1170b8b7db32a073d 100644
--- a/theories/axiomatic/invariant_lib.v
+++ b/theories/program_logics/invariant_lib.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.base_logic Require Export invariants.
-From semantics.axiomatic.heap_lang Require Export primitive_laws_nolater.
-From semantics.axiomatic.heap_lang Require Import adequacy proofmode.
+From semantics.pl.heap_lang Require Export primitive_laws_nolater.
+From semantics.pl.heap_lang Require Import adequacy proofmode.
 
 (** Rules for impredicative invariants *)
 
diff --git a/theories/axiomatic/ipm.v b/theories/program_logics/ipm.v
similarity index 98%
rename from theories/axiomatic/ipm.v
rename to theories/program_logics/ipm.v
index 36441671d5a859d745f31795258165e023799744..d2876a5edfce953b1e915d3c3bbeff04e6ae1cef 100644
--- a/theories/axiomatic/ipm.v
+++ b/theories/program_logics/ipm.v
@@ -1,9 +1,9 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang primitive_laws notation.
 From iris.base_logic Require Import invariants.
-From semantics.axiomatic.heap_lang Require Import adequacy proofmode primitive_laws_nolater.
-From semantics.axiomatic Require Import hoare_lib.
-From semantics.axiomatic.program_logic Require Import notation.
+From semantics.pl.heap_lang Require Import adequacy proofmode primitive_laws_nolater.
+From semantics.pl Require Import hoare_lib.
+From semantics.pl.program_logic Require Import notation.
 
 (** ** Magic is in the air *)
 Import hoare.
diff --git a/theories/axiomatic/later_loeb.v b/theories/program_logics/later_loeb.v
similarity index 97%
rename from theories/axiomatic/later_loeb.v
rename to theories/program_logics/later_loeb.v
index 5c0cfd1bcd4c22904e9690438abe4b676451b554..6fbcae8471856a36ac721751cff02be6a03f81b7 100644
--- a/theories/axiomatic/later_loeb.v
+++ b/theories/program_logics/later_loeb.v
@@ -1,10 +1,10 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang primitive_laws notation.
 From iris.base_logic Require Import invariants.
-From semantics.axiomatic.heap_lang Require Import adequacy proofmode primitive_laws_nolater.
-From semantics.axiomatic Require Import hoare_lib.
-From semantics.axiomatic.program_logic Require Import notation.
-From semantics.axiomatic Require Import ipm.
+From semantics.pl.heap_lang Require Import adequacy proofmode primitive_laws_nolater.
+From semantics.pl Require Import hoare_lib.
+From semantics.pl.program_logic Require Import notation.
+From semantics.pl Require Import ipm.
 
 (** Step-indexing *)
 Import hoare ipm.
diff --git a/theories/axiomatic/logrel/adequacy.v b/theories/program_logics/logrel/adequacy.v
similarity index 87%
rename from theories/axiomatic/logrel/adequacy.v
rename to theories/program_logics/logrel/adequacy.v
index 6f936403252acf66106c1d1ab7b30da1058d0f49..8c3b4f4b41aef0e5b739721a8c5f67de2b4500e9 100644
--- a/theories/axiomatic/logrel/adequacy.v
+++ b/theories/program_logics/logrel/adequacy.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
-From semantics.axiomatic.heap_lang Require Import primitive_laws adequacy.
-From semantics.axiomatic.logrel Require Import syntactic logrel .
+From semantics.pl.heap_lang Require Import primitive_laws adequacy.
+From semantics.pl.logrel Require Import syntactic logrel .
 From iris.prelude Require Import options.
 
 
diff --git a/theories/axiomatic/logrel/ghost_state.v b/theories/program_logics/logrel/ghost_state.v
similarity index 96%
rename from theories/axiomatic/logrel/ghost_state.v
rename to theories/program_logics/logrel/ghost_state.v
index e1b7a4a80f438e05850bf53d5dc6822c366cf7d0..b6ab827dcb4031a3d414ec411ab1310134573710 100644
--- a/theories/axiomatic/logrel/ghost_state.v
+++ b/theories/program_logics/logrel/ghost_state.v
@@ -1,10 +1,10 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.base_logic.lib Require Import mono_nat.
-From semantics.axiomatic Require Import invariant_lib.
-From semantics.axiomatic.logrel Require notation syntactic logrel.
-From semantics.axiomatic Require Import ghost_state_lib.
-From semantics.axiomatic.heap_lang Require Import primitive_laws proofmode.
+From semantics.pl Require Import invariant_lib.
+From semantics.pl.logrel Require notation syntactic logrel.
+From semantics.pl Require Import ghost_state_lib.
+From semantics.pl.heap_lang Require Import primitive_laws proofmode.
 From iris.prelude Require Import options.
 Set Default Proof Using "Type*".
 
diff --git a/theories/axiomatic/logrel/ghost_state_lib.v b/theories/program_logics/logrel/ghost_state_lib.v
similarity index 98%
rename from theories/axiomatic/logrel/ghost_state_lib.v
rename to theories/program_logics/logrel/ghost_state_lib.v
index 0648d9bbee8bf2fea954f61271c82bc06f049ac0..d529e3438fe4bfaf3bb5ca765918fa7341bd90c0 100644
--- a/theories/axiomatic/logrel/ghost_state_lib.v
+++ b/theories/program_logics/logrel/ghost_state_lib.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.base_logic.lib Require Import mono_nat ghost_var ghost_map.
-From semantics.axiomatic Require Import invariant_lib.
-From semantics.axiomatic.heap_lang Require Import primitive_laws proofmode.
+From semantics.pl Require Import invariant_lib.
+From semantics.pl.heap_lang Require Import primitive_laws proofmode.
 From iris.algebra Require Import csum excl agree.
 From iris.prelude Require Import options.
 
diff --git a/theories/axiomatic/logrel/logrel.v b/theories/program_logics/logrel/logrel.v
similarity index 98%
rename from theories/axiomatic/logrel/logrel.v
rename to theories/program_logics/logrel/logrel.v
index 2fe47b20145f47ac2b349d36f0412efb487c9326..b413aa4331d2d99997b5afa58c79ef6b713a65f9 100644
--- a/theories/axiomatic/logrel/logrel.v
+++ b/theories/program_logics/logrel/logrel.v
@@ -1,10 +1,10 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.heap_lang Require Import metatheory.
-From semantics.axiomatic Require Export invariant_lib.
-From semantics.axiomatic.logrel Require Import notation persistent_pred.
-From semantics.axiomatic.logrel Require Import syntactic.
-From semantics.axiomatic.heap_lang Require Export primitive_laws proofmode.
+From semantics.pl Require Export invariant_lib.
+From semantics.pl.logrel Require Import notation persistent_pred.
+From semantics.pl.logrel Require Import syntactic.
+From semantics.pl.heap_lang Require Export primitive_laws proofmode.
 From iris.prelude Require Import options.
 
 
diff --git a/theories/axiomatic/logrel/notation.v b/theories/program_logics/logrel/notation.v
similarity index 100%
rename from theories/axiomatic/logrel/notation.v
rename to theories/program_logics/logrel/notation.v
diff --git a/theories/axiomatic/logrel/persistent_pred.v b/theories/program_logics/logrel/persistent_pred.v
similarity index 100%
rename from theories/axiomatic/logrel/persistent_pred.v
rename to theories/program_logics/logrel/persistent_pred.v
diff --git a/theories/axiomatic/reloc/syntactic.v b/theories/program_logics/logrel/syntactic.v
similarity index 99%
rename from theories/axiomatic/reloc/syntactic.v
rename to theories/program_logics/logrel/syntactic.v
index 735f1ac08fefb7478bc682483341c7d3f2e54050..05879a1485f8c8ee55fe02d4065e1252af6d51d0 100644
--- a/theories/axiomatic/reloc/syntactic.v
+++ b/theories/program_logics/logrel/syntactic.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Import lang notation.
 From iris.heap_lang Require Export metatheory.
-From semantics.axiomatic.reloc Require Import notation.
+From semantics.pl.logrel Require Import notation.
 From Autosubst Require Export Autosubst.
 From stdpp Require Import gmap.
 From iris.prelude Require Import options.
diff --git a/theories/axiomatic/program_logic/adequacy.v b/theories/program_logics/program_logic/adequacy.v
similarity index 99%
rename from theories/axiomatic/program_logic/adequacy.v
rename to theories/program_logics/program_logic/adequacy.v
index 54c01ee1ab156fff560b707d121b0be1ad5ea8ce..181524e8fbd597d70cf0383ac413b6224b8bc791 100644
--- a/theories/axiomatic/program_logic/adequacy.v
+++ b/theories/program_logics/program_logic/adequacy.v
@@ -1,7 +1,7 @@
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.proofmode Require Import proofmode.
 From iris.base_logic.lib Require Import wsat.
-From semantics.axiomatic.program_logic Require Export sequential_wp.
+From semantics.pl.program_logic Require Export sequential_wp.
 From iris.prelude Require Import options.
 Import uPred.
 
diff --git a/theories/axiomatic/program_logic/ectx_lifting.v b/theories/program_logics/program_logic/ectx_lifting.v
similarity index 82%
rename from theories/axiomatic/program_logic/ectx_lifting.v
rename to theories/program_logics/program_logic/ectx_lifting.v
index f9b2e19ea6b5e2d0f6bb101617bd98dff1399322..b05640ff5ad5b4f1758df5ae201b5a3e5f8796cf 100644
--- a/theories/axiomatic/program_logic/ectx_lifting.v
+++ b/theories/program_logics/program_logic/ectx_lifting.v
@@ -1,7 +1,7 @@
 (** Some derived lemmas for ectx-based languages *)
 From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Export ectx_language.
-From semantics.axiomatic.program_logic Require Export sequential_wp lifting.
+From semantics.pl.program_logic Require Export sequential_wp lifting.
 From iris.prelude Require Import options.
 
 Section wp.
@@ -45,30 +45,6 @@ Proof.
   iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 κ efs ?) "!> !>". by iApply "H".
 Qed.
 
-(*
-Lemma wp_lift_head_stuck E Φ e :
-  to_val e = None →
-  sub_redexes_are_values e →
-  (∀ σ ns κs nt, state_interp σ ns κs nt ={E,∅}=∗ ⌜head_stuck e σ⌝)
-  ⊢ WP e @ E ?{{ Φ }}.
-Proof.
-  iIntros (??) "H". iApply wp_lift_stuck; first done.
-  iIntros (σ ns κs nt) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
-Qed.
- *)
-
-(*
-Lemma wp_lift_pure_head_stuck E Φ e :
-  to_val e = None →
-  sub_redexes_are_values e →
-  (∀ σ, head_stuck e σ) →
-  ⊢ WP e @ E ?{{ Φ }}.
-Proof using Hinh.
-  iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
-  iIntros (σ ns κs nt) "_". iApply fupd_mask_intro; by auto with set_solver.
-Qed.
- *)
-
 Lemma wp_lift_head_step_fupd_nomask {s E1 E2 E3 Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E1}=∗
diff --git a/theories/axiomatic/program_logic/lifting.v b/theories/program_logics/program_logic/lifting.v
similarity index 98%
rename from theories/axiomatic/program_logic/lifting.v
rename to theories/program_logics/program_logic/lifting.v
index 063649e6b0435b046efa9e0a69a52ca21236b35c..c48a7bd4d3fa76c527045387554c0eb580833cf2 100644
--- a/theories/axiomatic/program_logic/lifting.v
+++ b/theories/program_logics/program_logic/lifting.v
@@ -2,7 +2,7 @@
 semantics to the program logic. *)
 
 From iris.proofmode Require Import proofmode.
-From semantics.axiomatic.program_logic Require Export sequential_wp.
+From semantics.pl.program_logic Require Export sequential_wp.
 From iris.prelude Require Import options.
 
 Section lifting.
diff --git a/theories/axiomatic/program_logic/notation.v b/theories/program_logics/program_logic/notation.v
similarity index 100%
rename from theories/axiomatic/program_logic/notation.v
rename to theories/program_logics/program_logic/notation.v
diff --git a/theories/axiomatic/program_logic/sequential_wp.v b/theories/program_logics/program_logic/sequential_wp.v
similarity index 99%
rename from theories/axiomatic/program_logic/sequential_wp.v
rename to theories/program_logics/program_logic/sequential_wp.v
index f230eda579a34bcbb0cf95d3e49fc102d9f761d2..35f1b6d3959ca2d50d52dbf2eae467b93323e125 100644
--- a/theories/axiomatic/program_logic/sequential_wp.v
+++ b/theories/program_logics/program_logic/sequential_wp.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import base proofmode classes.
 From iris.base_logic.lib Require Export fancy_updates.
 From iris.program_logic Require Export language.
-From semantics.axiomatic.program_logic Require Export notation.
+From semantics.pl.program_logic Require Export notation.
 From iris.prelude Require Import options.
 Import uPred.
 
diff --git a/theories/axiomatic/ra_lib.v b/theories/program_logics/ra_lib.v
similarity index 98%
rename from theories/axiomatic/ra_lib.v
rename to theories/program_logics/ra_lib.v
index ad41272af7f3920fe3a5ff6f0fb89a8eed6db68c..aa26fc7e3f51a6ca3f0d8ae423871af51789fde0 100644
--- a/theories/axiomatic/ra_lib.v
+++ b/theories/program_logics/ra_lib.v
@@ -1,7 +1,7 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.bi Require Import fractional.
-From semantics.axiomatic.heap_lang Require Import primitive_laws proofmode.
+From semantics.pl.heap_lang Require Import primitive_laws proofmode.
 From iris.base_logic Require Import own.
 From iris.prelude Require Import options.
 
diff --git a/theories/axiomatic/reloc/adequacy.v b/theories/program_logics/reloc/adequacy.v
similarity index 86%
rename from theories/axiomatic/reloc/adequacy.v
rename to theories/program_logics/reloc/adequacy.v
index 8d4375ea45b77f13c73f1e3c72c4270e62fceab4..28bae45312a56375c6b9e9071f986b040858f100 100644
--- a/theories/axiomatic/reloc/adequacy.v
+++ b/theories/program_logics/reloc/adequacy.v
@@ -1,8 +1,8 @@
 From iris.heap_lang Require Export lang.
-From semantics.axiomatic.heap_lang Require Export adequacy.
+From semantics.pl.heap_lang Require Export adequacy.
 From iris.base_logic Require Import ghost_var ghost_map.
-From semantics.axiomatic.reloc Require Import ghost_state.
-From semantics.axiomatic.reloc Require Export syntactic logrel.
+From semantics.pl.reloc Require Import ghost_state.
+From semantics.pl.reloc Require Export syntactic logrel.
 From iris.prelude Require Import options.
 
 
@@ -12,32 +12,33 @@ Lemma refines_adequate Σ `{reloc_preGS Σ} (τ : ∀ _ : relocGS Σ, semtypeO)
   (∀ `{relocGS Σ}, ⊢ refines e e' (τ _)) →
   adequate NotStuck e σ (λ v _, ∃ v' h', rtc thread_step (e', σ) (of_val v', h') ∧ ϕ v v').
 Proof.
-  intros Hnoproph Hpost Hlog. 
+  intros Hnoproph Hpost Hlog.
   eapply (heap_adequacy Σ _). iIntros (Hheap).
   iMod (ghost_map_alloc σ.(heap)) as "(%γheap & Hauth & _)".
   iMod (ghost_var_alloc e') as "(%γexpr & He1 & He2)".
   set (Hreloc := (RelocGS Σ _ _ _ γexpr γheap)).
-  
+
   (* initialize the invariant *)
   iApply (inv_alloc srcN (src_inv e' σ.(heap)) with "[Hauth He1]").
-  { iExists e', σ.(heap). rewrite exprS_eq heapS_auth_eq. rewrite /exprS_def /heapS_auth_def. 
+  { iExists e', σ.(heap). rewrite exprS_eq heapS_auth_eq. rewrite /exprS_def /heapS_auth_def.
     iFrame. done.
-  } 
+  }
+
   iIntros "#Hinv".
   iApply wp_fupd.
   iApply (wp_wand with "[He2]").
   { iApply (Hlog Hreloc $! []). iSplit.
     - iExists _, _. iFrame "Hinv".
     - rewrite exprS_eq /exprS_def. iFrame.
-  } 
+  }
   iIntros (v) "(%v' & [_ Hsrc] & #Ht)".
   (* requires that we open invariants around fancy updates *)
   iInv "Hinv" as "(%e'' & %σ'' & >He & >Hheap & >%Hstep)" "Hcl".
   iDestruct (exprS_agree with "He Hsrc") as %->.
-  iMod ("Hcl" with "[-]"). 
+  iMod ("Hcl" with "[-]").
   { iNext. iExists _, _. iFrame. done. }
   iModIntro. iDestruct (Hpost with "Ht") as "%Hp".
-  iPureIntro. eexists _, _. 
+  iPureIntro. eexists _, _.
   rewrite Hnoproph. split; done.
 Qed.
 
@@ -45,7 +46,7 @@ Lemma thread_erased_step e e' σ σ' :
   thread_step (e, σ) (e', σ') →
   erased_step ([e], σ) ([e'], σ').
 Proof.
-  intros Hprim. exists []. 
+  intros Hprim. exists [].
   eapply (step_atomic _ _ _ _ [] [] []); done.
 Qed.
 
@@ -60,7 +61,7 @@ Qed.
 Theorem refines_typesafety Σ `{reloc_preGS Σ} (τ : ∀ _ : relocGS Σ, semtypeO) (e e' : expr) e1 σ σ' :
   σ = mkstate σ.(heap) →
   (∀ `{relocGS Σ}, ⊢ refines e e' (τ _)) →
-  rtc thread_step (e, σ) (e1, σ') → 
+  rtc thread_step (e, σ) (e1, σ') →
   not_stuck e1 σ'.
 Proof.
   intros ? Hlog ?%rtc_thread_erased_step.
diff --git a/theories/axiomatic/reloc/contextual_refinement.v b/theories/program_logics/reloc/contextual_refinement.v
similarity index 99%
rename from theories/axiomatic/reloc/contextual_refinement.v
rename to theories/program_logics/reloc/contextual_refinement.v
index e3795680d91bd07cc464ad0ffe47a117afa1c3b5..920296969f7bb0c80cf3c5281a65029b2ee5ea33 100644
--- a/theories/axiomatic/reloc/contextual_refinement.v
+++ b/theories/program_logics/reloc/contextual_refinement.v
@@ -2,7 +2,7 @@
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import proofmode.
-From semantics.axiomatic.reloc Require Export syntactic logrel fundamental adequacy.
+From semantics.pl.reloc Require Export syntactic logrel fundamental adequacy.
 
 (** * Proving contextual refinement *)
 
diff --git a/theories/axiomatic/reloc/fundamental.v b/theories/program_logics/reloc/fundamental.v
similarity index 98%
rename from theories/axiomatic/reloc/fundamental.v
rename to theories/program_logics/reloc/fundamental.v
index 61fcadd8a6d524e0f7faf3e32c3a7bb64e972371..f8041d1ea463f87b18f1b7ee9b379b899df0ed8c 100644
--- a/theories/axiomatic/reloc/fundamental.v
+++ b/theories/program_logics/reloc/fundamental.v
@@ -1,9 +1,9 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.heap_lang Require Export metatheory.
-From semantics.axiomatic.reloc Require Import syntactic notation ghost_state proofmode logrel.
-From semantics.axiomatic.heap_lang Require Export proofmode.
-From semantics.axiomatic.program_logic Require Export notation.
+From semantics.pl.reloc Require Import syntactic notation ghost_state proofmode logrel.
+From semantics.pl.heap_lang Require Export proofmode.
+From semantics.pl.program_logic Require Export notation.
 From Autosubst Require Import Autosubst.
 From iris.prelude Require Import options.
 
diff --git a/theories/axiomatic/reloc/ghost_state.v b/theories/program_logics/reloc/ghost_state.v
similarity index 94%
rename from theories/axiomatic/reloc/ghost_state.v
rename to theories/program_logics/reloc/ghost_state.v
index aa9d6f74fe9c58f00d84c22e0316c63e5c990508..de0da0c2db333a8f7b8a79b060c74184f70c96d5 100644
--- a/theories/axiomatic/reloc/ghost_state.v
+++ b/theories/program_logics/reloc/ghost_state.v
@@ -1,10 +1,10 @@
 From iris.program_logic Require Import language ectx_language.
 From iris.heap_lang Require Export lang notation tactics.
 From iris.base_logic.lib Require Import ghost_map ghost_var.
-From semantics.axiomatic Require Export invariant_lib fupd.
-From semantics.axiomatic.program_logic Require Export notation.
-From semantics.axiomatic.heap_lang Require Import adequacy.
-From semantics.axiomatic.heap_lang Require Export proofmode.
+From semantics.pl Require Export invariant_lib fupd.
+From semantics.pl.program_logic Require Export notation.
+From semantics.pl.heap_lang Require Import adequacy.
+From semantics.pl.heap_lang Require Export proofmode.
 From iris Require Import prelude.
 
 
diff --git a/theories/axiomatic/reloc/logrel.v b/theories/program_logics/reloc/logrel.v
similarity index 97%
rename from theories/axiomatic/reloc/logrel.v
rename to theories/program_logics/reloc/logrel.v
index cf96dae694e7470131a123b90c092ca1ffd3e77d..c0c37cf5b746f59cdf27f046bd6cbd1f7af1e86b 100644
--- a/theories/axiomatic/reloc/logrel.v
+++ b/theories/program_logics/reloc/logrel.v
@@ -1,8 +1,8 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.heap_lang Require Export metatheory.
-From semantics.axiomatic.reloc Require Export notation src_rules.
-From semantics.axiomatic.reloc Require Export persistent_bipred.
+From semantics.pl.reloc Require Export notation src_rules.
+From semantics.pl.reloc Require Export persistent_bipred.
 From Autosubst Require Import Autosubst.
 From iris.prelude Require Import options.
 
diff --git a/theories/axiomatic/reloc/notation.v b/theories/program_logics/reloc/notation.v
similarity index 100%
rename from theories/axiomatic/reloc/notation.v
rename to theories/program_logics/reloc/notation.v
diff --git a/theories/axiomatic/reloc/persistent_bipred.v b/theories/program_logics/reloc/persistent_bipred.v
similarity index 100%
rename from theories/axiomatic/reloc/persistent_bipred.v
rename to theories/program_logics/reloc/persistent_bipred.v
diff --git a/theories/axiomatic/reloc/proofmode.v b/theories/program_logics/reloc/proofmode.v
similarity index 98%
rename from theories/axiomatic/reloc/proofmode.v
rename to theories/program_logics/reloc/proofmode.v
index cc0fc22d7dc288d2175aee7744df6e7822686ce3..92fe38cbb62e02aa6dec1329a71e848842ff665f 100644
--- a/theories/axiomatic/reloc/proofmode.v
+++ b/theories/program_logics/reloc/proofmode.v
@@ -4,10 +4,10 @@ From iris.base_logic.lib Require Import ghost_map ghost_var.
 From iris.base_logic Require Export invariants.
 From iris.proofmode Require Import proofmode.
 From iris.heap_lang Require Export lang notation tactics.
-From semantics.axiomatic.reloc Require Import ghost_state logrel.
+From semantics.pl.reloc Require Import ghost_state logrel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 From iris.proofmode Require Export tactics.
-From semantics.axiomatic.heap_lang Require Import primitive_laws.
+From semantics.pl.heap_lang Require Import primitive_laws.
 From iris Require Import prelude.
 
 
diff --git a/theories/axiomatic/reloc/src_rules.v b/theories/program_logics/reloc/src_rules.v
similarity index 97%
rename from theories/axiomatic/reloc/src_rules.v
rename to theories/program_logics/reloc/src_rules.v
index 7b1f9b887ce503df62105a8dce268f43aaf81a12..2ba26f1c25347156b0122a14b92fbda31b346957 100644
--- a/theories/axiomatic/reloc/src_rules.v
+++ b/theories/program_logics/reloc/src_rules.v
@@ -1,9 +1,9 @@
 From iris.program_logic Require Import language ectx_language.
 From iris.heap_lang Require Export lang notation tactics.
 From iris.base_logic.lib Require Import ghost_map ghost_var.
-From semantics.axiomatic Require Export invariant_lib.
-From semantics.axiomatic.program_logic Require Export notation.
-From semantics.axiomatic.reloc Require Export ghost_state.
+From semantics.pl Require Export invariant_lib.
+From semantics.pl.program_logic Require Export notation.
+From semantics.pl.reloc Require Export ghost_state.
 From iris Require Import prelude.
 
 (** ** Source update rules *)
diff --git a/theories/axiomatic/logrel/syntactic.v b/theories/program_logics/reloc/syntactic.v
similarity index 99%
rename from theories/axiomatic/logrel/syntactic.v
rename to theories/program_logics/reloc/syntactic.v
index 47e08bf4501bff45d83bfce3091fa19a44c93830..04ef245cb8351f21764ef73e9347fbae06f8545d 100644
--- a/theories/axiomatic/logrel/syntactic.v
+++ b/theories/program_logics/reloc/syntactic.v
@@ -1,6 +1,6 @@
 From iris.heap_lang Require Import lang notation.
 From iris.heap_lang Require Export metatheory.
-From semantics.axiomatic.logrel Require Import notation.
+From semantics.pl.reloc Require Import notation.
 From Autosubst Require Export Autosubst.
 From stdpp Require Import gmap.
 From iris.prelude Require Import options.
diff --git a/theories/axiomatic/resource_algebras.v b/theories/program_logics/resource_algebras.v
similarity index 99%
rename from theories/axiomatic/resource_algebras.v
rename to theories/program_logics/resource_algebras.v
index 439e60c2ac185e272af5863b6ca672810c360391..796f27566682b20162f19539325743685a7059a8 100644
--- a/theories/axiomatic/resource_algebras.v
+++ b/theories/program_logics/resource_algebras.v
@@ -1,10 +1,10 @@
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Import lang notation.
 From iris.bi Require Import fractional.
-From semantics.axiomatic.heap_lang Require Import primitive_laws proofmode.
+From semantics.pl.heap_lang Require Import primitive_laws proofmode.
 From Coq.Logic Require FunctionalExtensionality.
 From iris.base_logic Require Import own.
-From semantics.axiomatic Require Import ra_lib.
+From semantics.pl Require Import ra_lib.
 From iris.prelude Require Import options.
 
 (** ** Resource algebras *)
diff --git a/theories/stlc/cbn_logrel.v b/theories/type_systems/stlc/cbn_logrel.v
similarity index 98%
rename from theories/stlc/cbn_logrel.v
rename to theories/type_systems/stlc/cbn_logrel.v
index 5865897d48136580299b86e7ffd73496e0c5a695..cb157a4169d0198c957a629fcf37594938b4ca35 100644
--- a/theories/stlc/cbn_logrel.v
+++ b/theories/type_systems/stlc/cbn_logrel.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import sets maps.
-From semantics.stlc Require Import lang notation types parallel_subst.
+From semantics.ts.stlc Require Import lang notation types parallel_subst.
 From Equations Require Import Equations.
 
 Implicit Types
diff --git a/theories/stlc/exercises01.v b/theories/type_systems/stlc/exercises01.v
similarity index 98%
rename from theories/stlc/exercises01.v
rename to theories/type_systems/stlc/exercises01.v
index f7249c6298dbea47808586c9505db623c19148ab..6b14623ec3eb248e31a99164a1832a185d813950 100644
--- a/theories/stlc/exercises01.v
+++ b/theories/type_systems/stlc/exercises01.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations tactics.
 From iris Require Import prelude.
-From semantics.stlc Require Import lang notation.
+From semantics.ts.stlc Require Import lang notation.
 
 
 (* In these exercises, we will use the reflexive, transitive closure
diff --git a/theories/stlc/exercises02.v b/theories/type_systems/stlc/exercises02.v
similarity index 98%
rename from theories/stlc/exercises02.v
rename to theories/type_systems/stlc/exercises02.v
index 6b45c38e943460cf366265ec9bf297bce83a3f01..007c09426b03416f8c9411e493b2b29199ca1e77 100644
--- a/theories/stlc/exercises02.v
+++ b/theories/type_systems/stlc/exercises02.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations tactics.
 From iris Require Import prelude.
-From semantics.stlc Require Import lang notation.
-From semantics.stlc Require untyped types.
+From semantics.ts.stlc Require Import lang notation.
+From semantics.ts.stlc Require untyped types.
 
 
 (** ** Exercise 1: Prove that the structural and contextual semantics are equivalent. *)
diff --git a/theories/stlc/lang.v b/theories/type_systems/stlc/lang.v
similarity index 100%
rename from theories/stlc/lang.v
rename to theories/type_systems/stlc/lang.v
diff --git a/theories/stlc/logrel.v b/theories/type_systems/stlc/logrel.v
similarity index 99%
rename from theories/stlc/logrel.v
rename to theories/type_systems/stlc/logrel.v
index 2632e3fc175d01b40d8f9ea873d3899b4d8f7255..7a9a93dcaec19ab9dff3f8bc1685675e2eedc60d 100644
--- a/theories/stlc/logrel.v
+++ b/theories/type_systems/stlc/logrel.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import sets maps.
-From semantics.stlc Require Import lang notation types parallel_subst.
+From semantics.ts.stlc Require Import lang notation types parallel_subst.
 From Equations Require Import Equations.
 
 Implicit Types
diff --git a/theories/stlc/notation.v b/theories/type_systems/stlc/notation.v
similarity index 97%
rename from theories/stlc/notation.v
rename to theories/type_systems/stlc/notation.v
index 124c4d3abc477d0ea907bd3183d4a10624e26a95..4da6e39d40df3f45b500ff150a4f2986bc099fd6 100644
--- a/theories/stlc/notation.v
+++ b/theories/type_systems/stlc/notation.v
@@ -1,4 +1,4 @@
-From semantics.stlc Require Export lang.
+From semantics.ts.stlc Require Export lang.
 Set Default Proof Using "Type".
 
 
diff --git a/theories/stlc/parallel_subst.v b/theories/type_systems/stlc/parallel_subst.v
similarity index 99%
rename from theories/stlc/parallel_subst.v
rename to theories/type_systems/stlc/parallel_subst.v
index 6c7aeb8c65c170821ddc6dc69ec99375412c5d84..ec96c0d1a72cce16b2a86f09b94a879e7e0c054d 100644
--- a/theories/stlc/parallel_subst.v
+++ b/theories/type_systems/stlc/parallel_subst.v
@@ -1,4 +1,4 @@
-From semantics.stlc Require Import lang.
+From semantics.ts.stlc Require Import lang.
 From stdpp Require Import prelude.
 From iris Require Import prelude.
 From semantics.lib Require Export maps .
diff --git a/theories/stlc/types.v b/theories/type_systems/stlc/types.v
similarity index 99%
rename from theories/stlc/types.v
rename to theories/type_systems/stlc/types.v
index d63499b5fae92f0efc57dedded307616dddd4ba6..67ec84d982b13c1c9639572648d3e272fd1d1df4 100644
--- a/theories/stlc/types.v
+++ b/theories/type_systems/stlc/types.v
@@ -1,6 +1,6 @@
 From stdpp Require Import base relations tactics.
 From iris Require Import prelude.
-From semantics.stlc Require Import lang notation.
+From semantics.ts.stlc Require Import lang notation.
 From semantics.lib Require Import sets maps.
 
 (** ** Syntactic typing *)
diff --git a/theories/stlc/untyped.v b/theories/type_systems/stlc/untyped.v
similarity index 99%
rename from theories/stlc/untyped.v
rename to theories/type_systems/stlc/untyped.v
index 6cc327fea7e2a3237f1f95af45594fd71311c55b..c38d85e460a5bc8c69c55e86d72bd94b50c352d2 100644
--- a/theories/stlc/untyped.v
+++ b/theories/type_systems/stlc/untyped.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations tactics.
 From iris Require Import prelude.
 From semantics.lib Require Import sets maps.
-From semantics.stlc Require Import lang notation.
+From semantics.ts.stlc Require Import lang notation.
 
 (** The following two lemmas will be helpful in the sequel.
   They just lift multiple reduction steps (via [rtc]) to application.
diff --git a/theories/stlc_extended/bigstep.v b/theories/type_systems/stlc_extended/bigstep.v
similarity index 94%
rename from theories/stlc_extended/bigstep.v
rename to theories/type_systems/stlc_extended/bigstep.v
index 94e74012363bf6058c9e145ac923a0b88d274ea9..76557a32bca587d3f7b22e38229731026fde1ede 100644
--- a/theories/stlc_extended/bigstep.v
+++ b/theories/type_systems/stlc_extended/bigstep.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
-From semantics.stlc_extended Require Import lang notation types.
+From semantics.ts.stlc_extended Require Import lang notation types.
 
 (** * Big-step semantics *)
 
diff --git a/theories/stlc_extended/lang.v b/theories/type_systems/stlc_extended/lang.v
similarity index 100%
rename from theories/stlc_extended/lang.v
rename to theories/type_systems/stlc_extended/lang.v
diff --git a/theories/stlc_extended/logrel.v b/theories/type_systems/stlc_extended/logrel.v
similarity index 99%
rename from theories/stlc_extended/logrel.v
rename to theories/type_systems/stlc_extended/logrel.v
index bd55262ccf5bcf70d5328bac6db9f102242fa179..6e9d9a44d1f28951881621ac8ad8819e46d62b3d 100644
--- a/theories/stlc_extended/logrel.v
+++ b/theories/type_systems/stlc_extended/logrel.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
-From semantics.stlc_extended Require Import lang notation parallel_subst types bigstep.
+From semantics.ts.stlc_extended Require Import lang notation parallel_subst types bigstep.
 From Equations Require Export Equations.
 
 (** * Logical relation for the extended STLC *)
diff --git a/theories/stlc_extended/notation.v b/theories/type_systems/stlc_extended/notation.v
similarity index 98%
rename from theories/stlc_extended/notation.v
rename to theories/type_systems/stlc_extended/notation.v
index 178422373698bcef9afef2b69414395b77805d8c..2d8e7dece6c74277c7fa669e29b4c93798da7fc4 100644
--- a/theories/stlc_extended/notation.v
+++ b/theories/type_systems/stlc_extended/notation.v
@@ -1,4 +1,4 @@
-From semantics.stlc_extended Require Export lang.
+From semantics.ts.stlc_extended Require Export lang.
 Set Default Proof Using "Type".
 
 
diff --git a/theories/stlc_extended/parallel_subst.v b/theories/type_systems/stlc_extended/parallel_subst.v
similarity index 98%
rename from theories/stlc_extended/parallel_subst.v
rename to theories/type_systems/stlc_extended/parallel_subst.v
index 9cb6f1075562419d32dfd53a27f0996ceb5f6c48..536ade1d482accbc1d9eeb2c552a65458f512c67 100644
--- a/theories/stlc_extended/parallel_subst.v
+++ b/theories/type_systems/stlc_extended/parallel_subst.v
@@ -1,6 +1,6 @@
 From stdpp Require Import prelude.
 From iris Require Import prelude.
-From semantics.stlc_extended Require Import lang.
+From semantics.ts.stlc_extended Require Import lang.
 From semantics.lib Require Import maps.
 
 Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
diff --git a/theories/stlc_extended/types.v b/theories/type_systems/stlc_extended/types.v
similarity index 99%
rename from theories/stlc_extended/types.v
rename to theories/type_systems/stlc_extended/types.v
index 61a086c94b745636507f92b427f7a0cb8fe80c25..54cb29e3d98bb6e889be5be544449050f407edce 100644
--- a/theories/stlc_extended/types.v
+++ b/theories/type_systems/stlc_extended/types.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import maps.
-From semantics.stlc_extended Require Import lang notation.
+From semantics.ts.stlc_extended Require Import lang notation.
 
 (** ** Syntactic typing *)
 Inductive type : Type :=
diff --git a/theories/systemf/bigstep.v b/theories/type_systems/systemf/bigstep.v
similarity index 99%
rename from theories/systemf/bigstep.v
rename to theories/type_systems/systemf/bigstep.v
index 0ab12f2e03cba7fdc5fc2ac72eae926bb0ced023..0170fe4ce3e36b677029335bd961653b3190d9a3 100644
--- a/theories/systemf/bigstep.v
+++ b/theories/type_systems/systemf/bigstep.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export debruijn.
-From semantics.systemf Require Import lang notation types.
+From semantics.ts.systemf Require Import lang notation types.
 From Equations Require Import Equations.
 
 (** * Big-step semantics *)
diff --git a/theories/systemf/binary_logrel.v b/theories/type_systems/systemf/binary_logrel.v
similarity index 99%
rename from theories/systemf/binary_logrel.v
rename to theories/type_systems/systemf/binary_logrel.v
index f2b1a327e132f1a2cd2050d9d949020dc0e1859f..4717a13cee9b3f52823c40bfcd40924b2148dcaf 100644
--- a/theories/systemf/binary_logrel.v
+++ b/theories/type_systems/systemf/binary_logrel.v
@@ -4,7 +4,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export facts.
-From semantics.systemf Require Import lang notation parallel_subst types bigstep tactics.
+From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics.
 From Equations Require Export Equations.
 
 (** * Logical relation for SystemF *)
diff --git a/theories/systemf/church_encodings.v b/theories/type_systems/systemf/church_encodings.v
similarity index 98%
rename from theories/systemf/church_encodings.v
rename to theories/type_systems/systemf/church_encodings.v
index fa31a9c8f74c6794e63b89c19537720043b575ba..9578db518c2706ee666e11c309049e6bed5b7d37 100644
--- a/theories/systemf/church_encodings.v
+++ b/theories/type_systems/systemf/church_encodings.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export debruijn.
-From semantics.systemf Require Import lang notation types bigstep tactics.
+From semantics.ts.systemf Require Import lang notation types bigstep tactics.
 
 (** * Church encodings *)
 Implicit Types
diff --git a/theories/systemf/exercises03.v b/theories/type_systems/systemf/exercises03.v
similarity index 97%
rename from theories/systemf/exercises03.v
rename to theories/type_systems/systemf/exercises03.v
index 7aa0de4afafb0a3a7fb8ade676729fe9e572ad02..ef04b8e87c3e2f5b67247494c1f56f21adcb682e 100644
--- a/theories/systemf/exercises03.v
+++ b/theories/type_systems/systemf/exercises03.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
-From semantics.systemf Require Import lang notation types tactics.
+From semantics.ts.systemf Require Import lang notation types tactics.
 
 (** Exercise 3 (LN Exercise 22): Universal Fun *)
 
diff --git a/theories/systemf/exercises04.v b/theories/type_systems/systemf/exercises04.v
similarity index 98%
rename from theories/systemf/exercises04.v
rename to theories/type_systems/systemf/exercises04.v
index e14ab1c0e1a592cd54c3add985a45e2135651806..7b450fd08321d93d2be1381247c16710d4fe7f3f 100644
--- a/theories/systemf/exercises04.v
+++ b/theories/type_systems/systemf/exercises04.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
-From semantics.systemf Require Import lang notation parallel_subst types logrel tactics.
+From semantics.ts.systemf Require Import lang notation parallel_subst types logrel tactics.
 
 Section church_encodings.
   (** Exercise 1 (LN Exercise 24): Church encoding, sum types *)
diff --git a/theories/systemf/exercises05.v b/theories/type_systems/systemf/exercises05.v
similarity index 96%
rename from theories/systemf/exercises05.v
rename to theories/type_systems/systemf/exercises05.v
index 221dc2ca5fcb9d904cc25d23c0336bb460788dbf..3b157274ea19d0ca4be5206f3ea63ec01fade8b8 100644
--- a/theories/systemf/exercises05.v
+++ b/theories/type_systems/systemf/exercises05.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
-From semantics.systemf Require Import lang notation parallel_subst types tactics.
-From semantics.systemf Require logrel binary_logrel existential_invariants.
+From semantics.ts.systemf Require Import lang notation parallel_subst types tactics.
+From semantics.ts.systemf Require logrel binary_logrel existential_invariants.
 
 (** * Exercise Sheet 5 *)
 
diff --git a/theories/systemf/existential_invariants.v b/theories/type_systems/systemf/existential_invariants.v
similarity index 96%
rename from theories/systemf/existential_invariants.v
rename to theories/type_systems/systemf/existential_invariants.v
index 18812b30f08627ea1b60d89de423b7ab66b6e96f..235bb512a23c9c7679d07fc3730617505c0db989 100644
--- a/theories/systemf/existential_invariants.v
+++ b/theories/type_systems/systemf/existential_invariants.v
@@ -1,8 +1,8 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export debruijn.
-From semantics.systemf Require Import lang notation parallel_subst types bigstep tactics.
-From semantics.systemf Require logrel binary_logrel.
+From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics.
+From semantics.ts.systemf Require logrel binary_logrel.
 From Equations Require Import Equations.
 
 (** * Existential types and invariants *)
@@ -137,4 +137,4 @@ Section binary_mybit.
       all: simp type_interp; eauto.
   Qed.
 
-End binary_mybit.
\ No newline at end of file
+End binary_mybit.
diff --git a/theories/systemf/free_theorems.v b/theories/type_systems/systemf/free_theorems.v
similarity index 94%
rename from theories/systemf/free_theorems.v
rename to theories/type_systems/systemf/free_theorems.v
index 8147b44a89744ebcfa079a85d69728e8470bb390..1164aa4489199cc936324723e89aced261e5bdf7 100644
--- a/theories/systemf/free_theorems.v
+++ b/theories/type_systems/systemf/free_theorems.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export debruijn.
-From semantics.systemf Require Import lang notation parallel_subst types bigstep tactics logrel.
+From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep tactics logrel.
 From Equations Require Import Equations.
 
 (** * Free Theorems *)
diff --git a/theories/systemf/lang.v b/theories/type_systems/systemf/lang.v
similarity index 100%
rename from theories/systemf/lang.v
rename to theories/type_systems/systemf/lang.v
diff --git a/theories/systemf/logrel.v b/theories/type_systems/systemf/logrel.v
similarity index 99%
rename from theories/systemf/logrel.v
rename to theories/type_systems/systemf/logrel.v
index 1d7b3b22875c665b5cf4f90c2dfe184f73456e59..0fdffae31ef675fe5a369b519f6f917f255dcd15 100644
--- a/theories/systemf/logrel.v
+++ b/theories/type_systems/systemf/logrel.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export facts.
-From semantics.systemf Require Import lang notation parallel_subst types bigstep.
+From semantics.ts.systemf Require Import lang notation parallel_subst types bigstep.
 From Equations Require Export Equations.
 
 
diff --git a/theories/systemf/notation.v b/theories/type_systems/systemf/notation.v
similarity index 98%
rename from theories/systemf/notation.v
rename to theories/type_systems/systemf/notation.v
index c3b8fd7d55c90480c6e00bc2f52030545cb3bdc8..563b1117605872195167064bf036ddb65669ae9e 100644
--- a/theories/systemf/notation.v
+++ b/theories/type_systems/systemf/notation.v
@@ -1,4 +1,4 @@
-From semantics.systemf Require Export lang.
+From semantics.ts.systemf Require Export lang.
 Set Default Proof Using "Type".
 
 
diff --git a/theories/systemf/parallel_subst.v b/theories/type_systems/systemf/parallel_subst.v
similarity index 99%
rename from theories/systemf/parallel_subst.v
rename to theories/type_systems/systemf/parallel_subst.v
index 9f6e49d9f7bee88b0ce45e1321c28b80a695faa0..8f8987b7bf9578c50f508d5a9c2fbfd0ed962ec6 100644
--- a/theories/systemf/parallel_subst.v
+++ b/theories/type_systems/systemf/parallel_subst.v
@@ -1,6 +1,6 @@
 From stdpp Require Import prelude.
 From iris Require Import prelude.
-From semantics.systemf Require Import lang.
+From semantics.ts.systemf Require Import lang.
 From semantics.lib Require Import maps.
 
 Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
diff --git a/theories/systemf/tactics.v b/theories/type_systems/systemf/tactics.v
similarity index 98%
rename from theories/systemf/tactics.v
rename to theories/type_systems/systemf/tactics.v
index ea3a10a59b75e95c34ad904d08cdd20a6a8e9028..85eb10ec898c3a45b4da5b807bb0f2f5f80312fc 100644
--- a/theories/systemf/tactics.v
+++ b/theories/type_systems/systemf/tactics.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import facts.
-From semantics.systemf Require Export lang notation parallel_subst types bigstep.
+From semantics.ts.systemf Require Export lang notation parallel_subst types bigstep.
 
 Lemma list_subseteq_cons {X} (A B : list X) x : A ⊆ B → x :: A ⊆ x :: B.
 Proof. intros Hincl. intros y. rewrite !elem_of_cons. naive_solver. Qed.
diff --git a/theories/systemf/types.v b/theories/type_systems/systemf/types.v
similarity index 99%
rename from theories/systemf/types.v
rename to theories/type_systems/systemf/types.v
index 9abc84afe287edb96e638d020d4988c66d8ddb80..3377b839726405be67f6986a0535ecf8f8b7ad1d 100644
--- a/theories/systemf/types.v
+++ b/theories/type_systems/systemf/types.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import maps.
-From semantics.systemf Require Import lang notation.
+From semantics.ts.systemf Require Import lang notation.
 From Autosubst Require Export Autosubst.
 
 (** ** Syntactic typing *)
diff --git a/theories/systemf_mu/exercises06.v b/theories/type_systems/systemf_mu/exercises06.v
similarity index 98%
rename from theories/systemf_mu/exercises06.v
rename to theories/type_systems/systemf_mu/exercises06.v
index 87615741d838e538239df1dae7fbacb86ef0d4da..b74b43bbab276f6d75431b90e18104dcac5df813 100644
--- a/theories/systemf_mu/exercises06.v
+++ b/theories/type_systems/systemf_mu/exercises06.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations tactics.
 From iris Require Import prelude.
-From semantics.systemf_mu Require Import lang notation types pure tactics logrel.
+From semantics.ts.systemf_mu Require Import lang notation types pure tactics logrel.
 From Autosubst Require Import Autosubst.
 
 (** * Exercise Sheet 6 *)
diff --git a/theories/systemf_mu/lang.v b/theories/type_systems/systemf_mu/lang.v
similarity index 100%
rename from theories/systemf_mu/lang.v
rename to theories/type_systems/systemf_mu/lang.v
diff --git a/theories/systemf_mu/logrel.v b/theories/type_systems/systemf_mu/logrel.v
similarity index 99%
rename from theories/systemf_mu/logrel.v
rename to theories/type_systems/systemf_mu/logrel.v
index 8749c92d2619e6e51c60a3905b4e25b410cc4ccf..6888c34788f10902ad24852c5a4fa4dcdc7951c7 100644
--- a/theories/systemf_mu/logrel.v
+++ b/theories/type_systems/systemf_mu/logrel.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export facts.
-From semantics.systemf_mu Require Import lang notation types tactics pure parallel_subst.
+From semantics.ts.systemf_mu Require Import lang notation types tactics pure parallel_subst.
 From Equations Require Export Equations.
 
 (** * Logical relation for SystemF + recursive types *)
diff --git a/theories/systemf_mu/notation.v b/theories/type_systems/systemf_mu/notation.v
similarity index 98%
rename from theories/systemf_mu/notation.v
rename to theories/type_systems/systemf_mu/notation.v
index f63b18474a25c1b400f7763e879291ede902a058..d0398d85246aacc1377cd98915969e2c216e63a6 100644
--- a/theories/systemf_mu/notation.v
+++ b/theories/type_systems/systemf_mu/notation.v
@@ -1,4 +1,4 @@
-From semantics.systemf_mu Require Export lang.
+From semantics.ts.systemf_mu Require Export lang.
 Set Default Proof Using "Type".
 
 
diff --git a/theories/systemf_mu/parallel_subst.v b/theories/type_systems/systemf_mu/parallel_subst.v
similarity index 98%
rename from theories/systemf_mu/parallel_subst.v
rename to theories/type_systems/systemf_mu/parallel_subst.v
index 9937cb7cd8e896bb0e638122eb00b24a49aeebe8..4961307ced31e3bcbafcd62b6f126778de5d4704 100644
--- a/theories/systemf_mu/parallel_subst.v
+++ b/theories/type_systems/systemf_mu/parallel_subst.v
@@ -1,8 +1,7 @@
 From stdpp Require Import prelude.
 From iris Require Import prelude.
-From semantics.lib Require Import facts.
-From semantics.systemf_mu Require Import lang.
-From semantics.lib Require Import maps.
+From semantics.lib Require Import facts maps.
+From semantics.ts.systemf_mu Require Import lang.
 
 Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
   match e with
diff --git a/theories/systemf_mu/pure.v b/theories/type_systems/systemf_mu/pure.v
similarity index 99%
rename from theories/systemf_mu/pure.v
rename to theories/type_systems/systemf_mu/pure.v
index 5bb483188abdf7c3f87d0ae7305fd844c453b38c..22414374c2a34bf8a83c2aa84ab10190ebfecf3c 100644
--- a/theories/systemf_mu/pure.v
+++ b/theories/type_systems/systemf_mu/pure.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import maps.
-From semantics.systemf_mu Require Import lang notation.
+From semantics.ts.systemf_mu Require Import lang notation.
 
 Lemma contextual_ectx_step_case K e e' :
   contextual_step (fill K e) e' →
diff --git a/theories/systemf_mu/tactics.v b/theories/type_systems/systemf_mu/tactics.v
similarity index 98%
rename from theories/systemf_mu/tactics.v
rename to theories/type_systems/systemf_mu/tactics.v
index 36b6dad39d7ff7b84807b5ce07b3f43794f3bff0..70b9da11ea81843d683e69946f09fdee8ab7392d 100644
--- a/theories/systemf_mu/tactics.v
+++ b/theories/type_systems/systemf_mu/tactics.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export facts maps sets.
-From semantics.systemf_mu Require Export lang notation types.
+From semantics.ts.systemf_mu Require Export lang notation types.
 
 Ltac map_solver :=
   repeat match goal with
diff --git a/theories/systemf_mu/types.v b/theories/type_systems/systemf_mu/types.v
similarity index 99%
rename from theories/systemf_mu/types.v
rename to theories/type_systems/systemf_mu/types.v
index 0c34812d02e4d392bf8d91bad8d1b69d9243feb9..e72425a0e43709f5d8755bb99777fa388984503f 100644
--- a/theories/systemf_mu/types.v
+++ b/theories/type_systems/systemf_mu/types.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import maps.
-From semantics.systemf_mu Require Import lang notation.
+From semantics.ts.systemf_mu Require Import lang notation.
 From Autosubst Require Export Autosubst.
 
 (** ** Syntactic typing *)
diff --git a/theories/systemf_mu/untyped_encoding.v b/theories/type_systems/systemf_mu/untyped_encoding.v
similarity index 95%
rename from theories/systemf_mu/untyped_encoding.v
rename to theories/type_systems/systemf_mu/untyped_encoding.v
index b077bbcd14b3ee7fd960d28aeeca56f209173a5b..f85f267fd18ce848b7ea275d126f91da349fcac3 100644
--- a/theories/systemf_mu/untyped_encoding.v
+++ b/theories/type_systems/systemf_mu/untyped_encoding.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations tactics.
 From iris Require Import prelude.
-From semantics.systemf_mu Require Import lang notation types pure tactics.
+From semantics.ts.systemf_mu Require Import lang notation types pure tactics.
 From Autosubst Require Import Autosubst.
 
 (** * Encoding of the untyped lambda calculus *)
diff --git a/theories/systemf_mu/z_combinator.v b/theories/type_systems/systemf_mu/z_combinator.v
similarity index 98%
rename from theories/systemf_mu/z_combinator.v
rename to theories/type_systems/systemf_mu/z_combinator.v
index e1e0cb26950ef4d86f95a67cd749f2d3cf9e659b..4abde6b061b38e4cd11d1bee91a57f9c21fb02fa 100644
--- a/theories/systemf_mu/z_combinator.v
+++ b/theories/type_systems/systemf_mu/z_combinator.v
@@ -1,5 +1,5 @@
 From iris Require Import prelude.
-From semantics.systemf_mu Require Import lang notation parallel_subst types tactics logrel pure.
+From semantics.ts.systemf_mu Require Import lang notation parallel_subst types tactics logrel pure.
 From semantics.lib Require Import maps.
 
 Lemma sem_expr_rel_lambda_val A B δ k x e :
diff --git a/theories/systemf_mu_state/execution.v b/theories/type_systems/systemf_mu_state/execution.v
similarity index 99%
rename from theories/systemf_mu_state/execution.v
rename to theories/type_systems/systemf_mu_state/execution.v
index bfd96b7a6ac80dfb79079827c8cb5eb67615098c..d63a9da2bec7979c3a2a0f03e9a5b0002dcd8983 100644
--- a/theories/systemf_mu_state/execution.v
+++ b/theories/type_systems/systemf_mu_state/execution.v
@@ -1,6 +1,6 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
-From semantics.systemf_mu_state Require Import lang notation.
+From semantics.ts.systemf_mu_state Require Import lang notation.
 (* TODO: everywhere replace the metavar σ for heaps with h *)
 
 (** ** Deterministic reduction *)
diff --git a/theories/systemf_mu_state/exercises07.v b/theories/type_systems/systemf_mu_state/exercises07.v
similarity index 97%
rename from theories/systemf_mu_state/exercises07.v
rename to theories/type_systems/systemf_mu_state/exercises07.v
index 828b70997d14caa13a590527802dbe0e7886d9fe..1ba385f263b6e3511bbeffa36b5c759a3d4da83d 100644
--- a/theories/systemf_mu_state/exercises07.v
+++ b/theories/type_systems/systemf_mu_state/exercises07.v
@@ -1,5 +1,5 @@
 From iris Require Import prelude.
-From semantics.systemf_mu_state Require Import lang notation parallel_subst tactics execution.
+From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst tactics execution.
 
 (** * Exercise Sheet 7 *)
 
diff --git a/theories/systemf_mu_state/lang.v b/theories/type_systems/systemf_mu_state/lang.v
similarity index 99%
rename from theories/systemf_mu_state/lang.v
rename to theories/type_systems/systemf_mu_state/lang.v
index 1bb8fa627db23b46564a3cc8e7bef33c29f2afc7..d9ab6652171b3bc8b52c682a479a1a2657140483 100644
--- a/theories/systemf_mu_state/lang.v
+++ b/theories/type_systems/systemf_mu_state/lang.v
@@ -1,6 +1,6 @@
 From iris.prelude Require Import prelude.
 From stdpp Require Export binders strings.
-From semantics.systemf_mu_state Require Export locations.
+From semantics.ts.systemf_mu_state Require Export locations.
 From semantics.lib Require Export maps.
 
 Declare Scope expr_scope.
diff --git a/theories/systemf_mu_state/locations.v b/theories/type_systems/systemf_mu_state/locations.v
similarity index 100%
rename from theories/systemf_mu_state/locations.v
rename to theories/type_systems/systemf_mu_state/locations.v
diff --git a/theories/systemf_mu_state/logrel.v b/theories/type_systems/systemf_mu_state/logrel.v
similarity index 99%
rename from theories/systemf_mu_state/logrel.v
rename to theories/type_systems/systemf_mu_state/logrel.v
index a10c51642c3d681a98ae1979a063fbe7bf634da2..8786a2b02e87cee83b1c2484e77332c5ef3575fd 100644
--- a/theories/systemf_mu_state/logrel.v
+++ b/theories/type_systems/systemf_mu_state/logrel.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export facts maps.
-From semantics.systemf_mu_state Require Import lang notation parallel_subst execution.
+From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst execution.
 From Equations Require Export Equations.
 From Autosubst Require Export Autosubst.
 
diff --git a/theories/systemf_mu_state/mutbit.v b/theories/type_systems/systemf_mu_state/mutbit.v
similarity index 98%
rename from theories/systemf_mu_state/mutbit.v
rename to theories/type_systems/systemf_mu_state/mutbit.v
index c66b578fa9cf81a8f4987df29aa23b9f95b4e938..1899ecf40916a242434f803420136b614404562b 100644
--- a/theories/systemf_mu_state/mutbit.v
+++ b/theories/type_systems/systemf_mu_state/mutbit.v
@@ -1,6 +1,6 @@
 From iris Require Import prelude.
 From stdpp Require Import gmap.
-From semantics.systemf_mu_state Require Import lang notation parallel_subst execution tactics logrel .
+From semantics.ts.systemf_mu_state Require Import lang notation parallel_subst execution tactics logrel .
 
 (** Proving safety of MutBit *)
 
diff --git a/theories/systemf_mu_state/notation.v b/theories/type_systems/systemf_mu_state/notation.v
similarity index 98%
rename from theories/systemf_mu_state/notation.v
rename to theories/type_systems/systemf_mu_state/notation.v
index 45d48e9cfd8581b4f6bd489c4eac69dc4323177b..e4d1cd0ffba955dd5f84b9b9428a35bf4e335884 100644
--- a/theories/systemf_mu_state/notation.v
+++ b/theories/type_systems/systemf_mu_state/notation.v
@@ -1,4 +1,4 @@
-From semantics.systemf_mu_state Require Export lang.
+From semantics.ts.systemf_mu_state Require Export lang.
 Set Default Proof Using "Type".
 
 
diff --git a/theories/systemf_mu_state/parallel_subst.v b/theories/type_systems/systemf_mu_state/parallel_subst.v
similarity index 99%
rename from theories/systemf_mu_state/parallel_subst.v
rename to theories/type_systems/systemf_mu_state/parallel_subst.v
index 61fa74833e7d1d65da9dd78491fe362119ef8612..2d177d843ac3f3fdffa1fa3ef4370fd0cf6fa9b4 100644
--- a/theories/systemf_mu_state/parallel_subst.v
+++ b/theories/type_systems/systemf_mu_state/parallel_subst.v
@@ -1,7 +1,7 @@
 From stdpp Require Import prelude.
 From iris Require Import prelude.
 From semantics.lib Require Import facts.
-From semantics.systemf_mu_state Require Import lang.
+From semantics.ts.systemf_mu_state Require Import lang.
 From semantics.lib Require Import maps.
 
 Fixpoint subst_map (xs : gmap string expr) (e : expr) : expr :=
diff --git a/theories/systemf_mu_state/tactics.v b/theories/type_systems/systemf_mu_state/tactics.v
similarity index 97%
rename from theories/systemf_mu_state/tactics.v
rename to theories/type_systems/systemf_mu_state/tactics.v
index 854c4e5397c11f63d2f1f0615a9a1d955ce2c681..a38ae75e31075d7a2b513758b529acc9b3de22a2 100644
--- a/theories/systemf_mu_state/tactics.v
+++ b/theories/type_systems/systemf_mu_state/tactics.v
@@ -1,7 +1,7 @@
 From stdpp Require Import gmap base relations.
 From iris Require Import prelude.
 From semantics.lib Require Export facts maps sets.
-From semantics.systemf_mu_state Require Export lang notation parallel_subst types.
+From semantics.ts.systemf_mu_state Require Export lang notation parallel_subst types.
 
 Ltac map_solver :=
   repeat match goal with
diff --git a/theories/systemf_mu_state/types.v b/theories/type_systems/systemf_mu_state/types.v
similarity index 99%
rename from theories/systemf_mu_state/types.v
rename to theories/type_systems/systemf_mu_state/types.v
index 1e1efd9d96b2602417ccf53d76092201bea047e9..b5bf5aeb529cce1cbd50e4428d59ad6ebf74d220 100644
--- a/theories/systemf_mu_state/types.v
+++ b/theories/type_systems/systemf_mu_state/types.v
@@ -1,7 +1,7 @@
 From stdpp Require Import base relations.
 From iris Require Import prelude.
 From semantics.lib Require Import maps.
-From semantics.systemf_mu_state Require Import lang notation.
+From semantics.ts.systemf_mu_state Require Import lang notation.
 From Autosubst Require Export Autosubst.
 
 (** ** Syntactic typing *)
diff --git a/theories/warmup/sheet0.v b/theories/type_systems/warmup/sheet0.v
similarity index 100%
rename from theories/warmup/sheet0.v
rename to theories/type_systems/warmup/sheet0.v