diff --git a/README.md b/README.md
new file mode 100644
index 0000000..5693fb4
--- /dev/null
+++ b/README.md
@@ -0,0 +1,67 @@
+# Coq development for the Semantics course 2023 at Saarland University
+
+This repository contains the Coq code for the [Semantics course](https://cms.sic.saarland/semantics_ws2324/) taught by Derek Dreyer at Saarland University in winter semester 23/24. It will be updated throughout the semester as the course progresses.
+
+## Installation instructions
+
+### Windows
+
+Unfortunately, Windows does not support Coq and the libraries we are using well. If you can use either Linux or MacOS instead, please follow the instructions below. Otherwise we recommend you set up WSL as explained [here](https://learn.microsoft.com/en-us/windows/wsl/install), proceed with the installation instructions below, and set up [VSCode for use with WSL](https://code.visualstudio.com/docs/remote/wsl).
+
+
+### Linux/MacOS
+
+We recommend installing Coq through opam, the OCaml package manager. To do so, visit the [opam installation guide](https://opam.ocaml.org/doc/Install.html) and follow the instructions.
+
+Next, clone this repository:
+```
+git clone https://gitlab.mpi-sws.org/FP/semantics-2023.git
+```
+Now proceed to install the dependencies:
+```
+cd semantics-2023
+
+# We create a new "switch" to install the dependencies in. Switches are independent 
+# installation prefixes with their own set of installed packages.
+opam switch create semantics ocaml-base-compiler.4.14.0
+# We tell opam to automatically enable the switch `semantics` in this directory
+opam switch link semantics .
+eval $(opam env)
+
+
+# We tell opam where to find the dependencies
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
+
+# We install the dependencies
+make builddep
+```
+
+## Compiling the Coq code
+
+In this repository you can find the templates for the exercises, files from the lectures, and some auxiliary files. We will make more and more files available as the course progresses.
+
+The Coq code is spread out among multiple files and directories. To compile, run the following command
+```
+make -j
+# or, alternatively, if you want to restrict the number of threads used:
+make -j4
+```
+**IMPORTANT:** You will have to compile to interactively do proofs. You will have to recompile if the dependencies of the file your editing change.
+
+
+## Editing the Coq code
+To edit the Coq code and complete the exercises, you will need an editor. We recommend you use [CoqIDE](https://coq.inria.fr/refman/practical-tools/coqide.html) or [VSCoq](https://github.com/coq-community/vscoq) ([VSCode](https://code.visualstudio.com/)).
+
+### CoqIDE
+
+To install CoqIDE, run the following command:
+```
+opam install coqide
+```
+
+### VSCode
+
+TODO links to installation instructions for VSCode/VSCoq
+
+If you're using WSL for Coq then you will want to use VSCoq (VSCode) because it integrates well with WSL. For instructions on how to set this up, see [here](https://code.visualstudio.com/docs/remote/wsl).