From e529e4b0f4513e2bc593bdf85292f66e84d2f75b Mon Sep 17 00:00:00 2001 From: sanjay Date: Mon, 18 May 2026 13:58:06 +0530 Subject: [PATCH] Add internal project ideas page (/ideas-internal/) Co-Authored-By: Claude Sonnet 4.6 --- ideas-internal.md | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 ideas-internal.md diff --git a/ideas-internal.md b/ideas-internal.md new file mode 100644 index 0000000..b96173a --- /dev/null +++ b/ideas-internal.md @@ -0,0 +1,35 @@ +--- +layout: page +title: Project Ideas +permalink: /ideas-internal/ +--- + +## Education + +**CS pedagogy** +- Nand2Tetris in OCaml/LEAN: Piyush (IITPKD), Patanjali (IITM), Manu (IITGN) +- Dynamic textbook +- Intro to CS for non-CS audience: Aalok Thakkar (Ashoka) +- OCaml notebooks (like Jupyter) that run in the browser + +**Lean for elementary mathematics** — Formalise pen-and-paper arithmetic operations (addition, subtraction, multiplication, long division) and basic discrete math proofs in Lean. Goals: (1) teaching material for 1-day beginner workshops on formal verification; (2) potential basis for teaching discrete math at IITM. Collaborators: Pranav Ramesh, [Neeldhara Mishra](https://www.neeldhara.com/) (IIT Gandhinagar). + +--- + +## Systems, Security & Formal Methods + +**Cryptographic primitives in OxCaml** — Implement basic cryptographic primitives natively in OxCaml, rather than as C wrappers (cf. [cryptokit](https://github.com/xavierleroy/cryptokit)). Demonstrate the performance and safety benefits of direct OxCaml implementations. + +**Lean verification of Bluespec System Verilog hardware** — Use Lean to verify simple hardware designs written in Bluespec System Verilog. + +--- + +## Concurrency & Programming Languages + +**Linearizable data structures in presence of data races** + +**Memory model 2.0** + +**Composable concurrency** + +**Linearizability checker for blocking operations**