diff --git a/.gitignore b/.gitignore
index e38a0bd599723aa5eafdad96980bc566d075591e..334369ae1b4cba4cc6a1ad1d30621516353de064 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,4 +9,5 @@
 *~
 *.bak
 .coq-native/
+iris-project
 Makefile.coq
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000000000000000000000000000000000000..941d913e2ae27c2842dff9d29ab0cb6547e03ba1
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "iris"]
+	path = iris
+	url = https://gitlab.mpi-sws.org/FP/iris-coq.git
diff --git a/Makefile b/Makefile
index 6c3ca5b55b668d803065baccb0727a23ea64344d..4ab350fe1e22af810ac424b9f65dfbafde0c2b12 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,4 @@
+
 # Makefile originally taken from coq-club
 
 %: Makefile.coq phony
@@ -13,10 +14,18 @@ clean: Makefile.coq
 Makefile.coq: _CoqProject Makefile
 	coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq
 
+iris-local: clean
+	git submodule update --init iris
+	ln -s iris iris-enabled
+	+make -C iris -f Makefile
+
+iris-system: clean
+	rm -f iris-enabled
+
 _CoqProject: ;
 
 Makefile: ;
 
 phony: ;
 
-.PHONY: all clean phony
+.PHONY: all clean phony iris-local iris-system
diff --git a/README.md b/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..b55b334704cfd5eefbdb988b92a56dbd8353a611
--- /dev/null
+++ b/README.md
@@ -0,0 +1,26 @@
+# LAMBDA-RUST COQ DEVELOPMENT
+
+This is the Coq formalization of lambda-Rust.
+
+## Prerequisites
+
+This version is known to compile with:
+
+ - Coq 8.5pl2
+ - Ssreflect 1.6
+
+You will furthermore need an up-to-date version of
+[Iris](https://gitlab.mpi-sws.org/FP/iris-coq/).  Run `git submodule status` to
+see which git commit of Iris is known to work.  You can pick between using a
+system-installed Iris (from Coq's `user-contrib`) or a version of Iris locally
+compiled for lambda-Rust.
+
+## Building Instructions
+
+To use the system-installed Iris (which is the default), run `make iris-system`.
+This only works if you previously built and installed a compatible version of the
+Iris Coq formalization.  To use a local Iris (which will always be the right
+version), run `make iris-local`.  Run this command again later to update the
+local Iris, in case the preferred Iris version changed.
+
+Now run `make` to build the full development.
diff --git a/_CoqProject b/_CoqProject
index 9769f2a71cc1a9a4dffe3081347bbb917d116cb4..c4ae5b38be5032c7027833b1b1003f4740daa6b4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,18 +1,19 @@
--Q . lrust
-adequacy.v
-derived.v
-heap.v
-lang.v
-lifting.v
-memcpy.v
-notation.v
-proofmode.v
-races.v
-tactics.v
-wp_tactics.v
-lifetime.v
-type.v
-type_incl.v
-perm.v
-perm_incl.v
-typing.v
+-Q theories lrust
+-Q iris-enabled iris
+theories/adequacy.v
+theories/derived.v
+theories/heap.v
+theories/lang.v
+theories/lifting.v
+theories/memcpy.v
+theories/notation.v
+theories/proofmode.v
+theories/races.v
+theories/tactics.v
+theories/wp_tactics.v
+theories/lifetime.v
+theories/type.v
+theories/type_incl.v
+theories/perm.v
+theories/perm_incl.v
+theories/typing.v
diff --git a/iris b/iris
new file mode 160000
index 0000000000000000000000000000000000000000..bb5e21f21fd1b5be820005eb53750f84270ab4ec
--- /dev/null
+++ b/iris
@@ -0,0 +1 @@
+Subproject commit bb5e21f21fd1b5be820005eb53750f84270ab4ec
diff --git a/adequacy.v b/theories/adequacy.v
similarity index 100%
rename from adequacy.v
rename to theories/adequacy.v
diff --git a/derived.v b/theories/derived.v
similarity index 100%
rename from derived.v
rename to theories/derived.v
diff --git a/heap.v b/theories/heap.v
similarity index 100%
rename from heap.v
rename to theories/heap.v
diff --git a/lang.v b/theories/lang.v
similarity index 100%
rename from lang.v
rename to theories/lang.v
diff --git a/lifetime.v b/theories/lifetime.v
similarity index 100%
rename from lifetime.v
rename to theories/lifetime.v
diff --git a/lifting.v b/theories/lifting.v
similarity index 100%
rename from lifting.v
rename to theories/lifting.v
diff --git a/memcpy.v b/theories/memcpy.v
similarity index 100%
rename from memcpy.v
rename to theories/memcpy.v
diff --git a/notation.v b/theories/notation.v
similarity index 100%
rename from notation.v
rename to theories/notation.v
diff --git a/perm.v b/theories/perm.v
similarity index 100%
rename from perm.v
rename to theories/perm.v
diff --git a/perm_incl.v b/theories/perm_incl.v
similarity index 100%
rename from perm_incl.v
rename to theories/perm_incl.v
diff --git a/proofmode.v b/theories/proofmode.v
similarity index 100%
rename from proofmode.v
rename to theories/proofmode.v
diff --git a/races.v b/theories/races.v
similarity index 100%
rename from races.v
rename to theories/races.v
diff --git a/tactics.v b/theories/tactics.v
similarity index 100%
rename from tactics.v
rename to theories/tactics.v
diff --git a/type.v b/theories/type.v
similarity index 100%
rename from type.v
rename to theories/type.v
diff --git a/type_incl.v b/theories/type_incl.v
similarity index 100%
rename from type_incl.v
rename to theories/type_incl.v
diff --git a/typing.v b/theories/typing.v
similarity index 100%
rename from typing.v
rename to theories/typing.v
diff --git a/wp_tactics.v b/theories/wp_tactics.v
similarity index 100%
rename from wp_tactics.v
rename to theories/wp_tactics.v