diff --git a/TODO.md b/TODO.md
index 825dbfb..f54c370 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,16 +1,19 @@
 # Possible future topics
 - Have a file showcasing advanced Coq tactics.
-- Add example with "Landin's knot" (recursion through the store).
+- Add example with "Landin's knot" (recursion through the store) to showcase use of invariants for sequential programs.
 - Add some exercises from Persistently chapter in ILN to Persistently chapter.
 - Introduce Generic CMRAs
 - Introduce Higher Order CMRAs
 - Internal equivalence and validity (Plainly, SIProp)
 - Inner workings of BI and using Iris proofmode on other logics.
   - Incompatibility of excluded middle.
-- How to define a new language in Iris.
 - Defining new modalities
   - Run through the relevant typeclasses
+- On inductive, co-inductive, and guarded-recursive predicates (based on chapter in ILN).
+- How to define a new language in Iris.
+- How to define a new program in Iris.
+- How to define logical relations models of type systems in Iris.
 
 # Features
 - Make tutorial accessible as an interactive webpage (jscoq)
-  - See e.g. https://jscoq.github.io/ext/sf/
\ No newline at end of file
+  - See e.g. https://jscoq.github.io/ext/sf/