diff --git a/teaching/2023/cs422/index.md b/teaching/2023/cs422/index.md
index 9ecef6f..bc6e078 100644
--- a/teaching/2023/cs422/index.md
+++ b/teaching/2023/cs422/index.md
@@ -168,6 +168,30 @@ Note: See the [spawn-join](https://github.com/kframework/k/tree/master/k-distrib
 Note: See the [letrec](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/3_fun/1_untyped/2_substitution/exercises/letrec) exercise for details and test programs.
 
 ---
+
+- [K Tutorial, Part 5: Defining type systems](https://kframework.org/k-distribution/pl-tutorial/) (useful to define the type inferencer of FUN next). Click [here](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/1_k/5_types) to see the code on GitHub.
+
+
+---
+<b><em><span style="color:red">HW6-1 (can think of it as an extra-credit take-home final, whose weigh is same as a normal HW; choose one of HW6-1 or HW6-2)</span></em></b>
+
+This HW has only one exercise, but remember that all HWs have equal weight. The exercise is to develop a let-polymorphic type inferencer for FUN. Use the existing syntax of FUN. If correct, your type inferencer should type all the existing FUN programs.
+
+You are only required to do it using the implicit-constraint style, like in `1_k/5_types/lesson_9.5`.
+
+Explain why the type inferencer in HW6 is unsound w.r.t. references (yes, it is most likely unsound!), and fix it.
+
+Note: See the [fun-type-inferencer](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/3_fun/2_type-inference/exercises/fun-type-inferencer) exercise for details and test programs.
+
 ---
-... more to come ...
+
+- ***LOGIK: Designing Logic Programming Languages***
+  - [Logik](https://kframework.org/k-distribution/pl-tutorial/) (Part 10 of the K Tutorial). Click [here](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/4_logik) to see the code on GitHub. 
+
+
 ---
+<b><em><span style="color:red">HW6-2 (can think of it as a take-home final, whose weigh is same as a normal HW; choose one of HW6-1 or HW6-2)</span></em></b>
+
+This HW has only one exercise, but remember that all HWs have equal weight. The exercise is to extend LOGIK with several features.
+
+Note: See the [LOGIK extended](https://github.com/kframework/k/tree/master/k-distribution/pl-tutorial/2_languages/4_logik/extended/exercises/logik-extended) exercise for details and test programs.