updates

src/SUMMARY.md

@@ -1,9 +1,16 @@
 # Summary
 
-- [Computability](./Computability.md)
-  - [Paradoxes]()
-  - [Gödel, Church, and Turing]()
-- [Type Theory]()
-  - [Untyped lambda]()
+- [Paradoxes, Foundations, and Computability](./PARADOXES_FOUNDATIONS_COMPUTABILITY.md)
+  - [Russell's Paradox, Set Theory, Type Theory]()
+  - [Encoding First Order Logic in Foundations]()
+  - [Other Paradoxes, Incompleteness, Decidability]()
+- [Developments of Type Theory]()
   - [Lambda Cube]()
-  - [CoC, CiC]()
+  - [HoTT and Univalence]()
+- [Curry Howard Correspondence]()
+  - [PAT]()
+  - [Logic <-> Type Theories]()
+
+- [Verified Rust with Verus]()
+  - [Borrow Checker, Linear Types]()
+  - [Case Study: Verified Parsers](./verified_parsers.md)