diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 6f094f0..7fcfe94 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -19,6 +19,7 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:8.17'
+          - 'coqorg/coq:8.18'
       max-parallel: 4
       fail-fast: false
 
diff --git a/README.md b/README.md
index 20a96ee..c74eddd 100644
--- a/README.md
+++ b/README.md
@@ -26,13 +26,17 @@ to the code structure.
 
 - `gitree/` -- contains the core definitions related to guarded interaction trees
 - `lib/` -- derived combinators for gitrees
+- `effects/` -- concrete effects, their semantics, and program logic rules
 - `examples/input_lang/` -- formalization of the language with io, the soundness and adequacy
-- `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy
 - `examples/affine_lang/` -- formalization of the affine language, type safety of the language interoperability
-- `effects/` -- concrete effects, their interpretaions, and logics
+- `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy
+- `examples/delim_lang/` -- formalization shift/reset effects, of a language with delimited continuations and its soundness
 - `prelude.v` -- some stuff that is missing from Iris
 - `lang_generic.v` -- generic facts about languages with binders and their interpretations, shared by `input_lang` and `affine_lang`
-- `vendor/Binding/` -- the functorial syntax library used for
+
+For the representation of binders we use a library implemented by
+Filip Sieczkowski and Piotr Polesiuk, located in the `vendor/Binding/`
+folder.
 
 ### References from the paper to the code
 
@@ -76,15 +80,6 @@ Below we describe the correspondence per-section.
 
 ## Notes
 
-### Representations of binders 1
-For the representation of languages with binders, we follow the
-approach of (Benton, Hur, Kennedy, McBride, JAR 2012) with well-scoped
-terms and substitutions/renamings. (`input_lang`, `affine_lang`)
-
-### Representations of binders 2
-For `input_lang_callcc` we use a binder library, implemented by Filip
-Sieczkowski and Piotr Polesiuk.
-
 ### Disjunction property
 Some results in the formalization make use of the disjunction property
 of Iris: if (P ∨ Q) is provable, then either P or Q are provable on
diff --git a/TODO.md b/TODO.md
deleted file mode 100644
index 1038abe..0000000
--- a/TODO.md
+++ /dev/null
@@ -1,18 +0,0 @@
-# Now
-- cleanup code
-  + especially implicit arguments, inserted by typeclasses
-  + lemmas for logrel
-- backward compatibility
-  + instances of CtxIndep from individual effects, from sreifiers to greifiers
-- write summary
-  + reifiers changes
-  + non-cps vs cps
-  + extra ticks for throw
-# Later
-- (ctrees)[https://perso.ens-lyon.fr/yannick.zakowski/papers/ctrees.pdf]
-- Nondet : (n : nat) (f : fin n -n> \later IT) -n> IT
-- (Nondet : (f : nat -n> \later IT) -n> IT) (might require transfinite iris)
-- Cooperative concurrency
-# Later later
-- bisimularity for gitrees (might require transfinite iris)
-- concurrency