feat: Add 7 typed holes skills for PLT (162 total skills)

Add comprehensive typed holes skills covering theory and practice:

Core Theory (3 skills):
- typed-holes-foundations.md: Gradual typing, bidirectional typing, hole semantics
- hazelnut-calculus.md: Structure editor calculus (POPL 2017), edit actions, Grove
- typed-holes-semantics.md: Advanced semantics, pattern matching, error localization

Practice (3 skills):
- typed-holes-interaction.md: IDE integration, goal-directed programming, tactics
- live-programming-holes.md: Hazel environment, incremental typing (OOPSLA 2025)
- structure-editors.md: Projectional editing, rendering, text integration

AI-Assisted Programming (1 skill):
- typed-holes-llm.md: LLM + typed holes (OOPSLA 2024), static context, validation

Skills based on latest research:
- OOPSLA 2024: Statically Contextualizing LLMs with Typed Holes
- OOPSLA 2025: Incremental Bidirectional Typing (Distinguished Paper)
- POPL 2025: Grove collaborative editing
- POPL 2024: Type Error Localization with Holes

Updates:
- PLT category: 6 → 13 skills
- Total skills: 155 → 162
- Added AI-assisted coding scenario to README
- Updated _INDEX.md with typed holes workflows
- All skills ~400 lines, YAML frontmatter, CI-validated

Author: rand

README.md

@@ -1,6 +1,6 @@
 # Claude Code Development Reference
 
-A comprehensive skills library and development guidelines for working with Claude Code across 155 atomic, composable skills spanning 31 technology domains.
+A comprehensive skills library and development guidelines for working with Claude Code across 162 atomic, composable skills spanning 31 technology domains.
 
 ## Overview
 
@@ -100,10 +100,11 @@ This repository serves as a complete reference for software development best pra
 - **Numerical**: Linear algebra, optimization algorithms, numerical methods, probability/statistics (4 skills)
 - **Pure Math**: Topology (point-set, algebraic), category theory, differential equations, abstract algebra, set theory, number theory (7 skills)
 
-**Programming Language Theory** (6 skills):
-- Lambda calculus, type systems, dependent types
-- Curry-Howard correspondence, operational semantics
-- Program verification (Hoare logic, SMT-based verification)
+**Programming Language Theory** (13 skills):
+- **Core PLT**: Lambda calculus, type systems, dependent types
+- **Curry-Howard & Semantics**: Propositions as types, operational semantics, program verification
+- **Typed Holes & Live Programming**: Hazel/Hazelnut calculus, structure editors, incremental typing (OOPSLA 2025)
+- **AI-Assisted Programming**: LLM + typed holes integration (OOPSLA 2024), static context for code synthesis
 
 **Real-time & Networking:**
 - WebSocket implementation, Server-Sent Events
@@ -202,7 +203,7 @@ skills/plt/type-systems.md
 │
 ├── README.md              # This file
 │
-└── skills/                # 155 atomic skills across 31 categories
+└── skills/                # 162 atomic skills across 31 categories
     │
     ├── _INDEX.md          # Full catalog with use cases and workflows
     │
@@ -306,6 +307,14 @@ skills/skill-creation.md           # Template and guidelines
 4. Use `ios-networking.md` → API integration
 5. Deploy backend with `redpanda-streaming.md` + `modal-web-endpoints.md`
 
+### Scenario: AI-Assisted Programming with Typed Holes
+1. Start with `plt/typed-holes-foundations.md` → Understand gradual typing and bidirectional checking
+2. Study `plt/typed-holes-llm.md` → Learn OOPSLA 2024 approach to LLM + static types
+3. Implement language server integration → Extract type context from holes
+4. Build LLM integration → Type-driven prompts, validation pipeline, ranking
+5. Add interactive refinement → User + LLM collaboration via holes
+6. Optional: `plt/live-programming-holes.md` → Real-time feedback with incremental typing
+
 ## Technology Coverage Matrix
 
 | Domain | Technologies | Skills | Key Capabilities |
@@ -318,7 +327,7 @@ skills/skill-creation.md           # Template and guidelines
 | **ML/AI** | DSPy, Unsloth, HuggingFace, Diffusion | 14 | LLM orchestration, fine-tuning, image generation |
 | **Formal** | Z3, Lean 4, CSP | 10 | Proof systems, constraint solving |
 | **Math** | Linear algebra, topology, category theory, etc. | 11 | Numerical + pure mathematics |
-| **PLT** | Lambda calculus, type systems, verification | 6 | Language design, formal verification |
+| **PLT** | Lambda calculus, type systems, typed holes, Hazel, LLM integration | 13 | Language design, live programming, AI-assisted coding |
 | **DevOps** | GitHub Actions, Terraform, K8s, Docker | 16 | CI/CD, IaC, containers |
 | **Data** | ETL, Streaming, Batch | 10 | Pipelines, real-time, analytics |
 
@@ -345,4 +354,4 @@ Feel free to fork and adapt for your own use.
 
 ---
 
-**Total: 155 atomic skills** | **Average: 320 lines/skill** | **31 categories** | **100% CI-validated**
+**Total: 162 atomic skills** | **Average: 320 lines/skill** | **31 categories** | **100% CI-validated**

skills/_INDEX.md

@@ -512,7 +512,9 @@ This index catalogs all atomic skills available in the skills system, organized
 
 ---
 
-### Programming Language Theory (6 skills)
+### Programming Language Theory (13 skills)
+
+**Core PLT:**
 
 | Skill | Use When | Lines |
 |-------|----------|-------|
@@ -523,11 +525,26 @@ This index catalogs all atomic skills available in the skills system, organized
 | `operational-semantics.md` | Small-step/big-step semantics, evaluation strategies, reduction systems | ~420 |
 | `program-verification.md` | Hoare logic, SMT-based verification, refinement types, separation logic | ~400 |
 
+**Typed Holes & Live Programming:**
+
+| Skill | Use When | Lines |
+|-------|----------|-------|
+| `typed-holes-foundations.md` | Typed holes basics, gradual typing, bidirectional typing, hole semantics | ~400 |
+| `hazelnut-calculus.md` | Structure editor calculus, edit actions, zipper navigation, Grove | ~420 |
+| `typed-holes-semantics.md` | Advanced hole semantics: closures, pattern matching, error localization, polymorphism | ~400 |
+| `typed-holes-interaction.md` | IDE integration, goal-directed programming, tactics, proof search, elaborator reflection | ~380 |
+| `live-programming-holes.md` | Hazel environment, live evaluation, incremental typing (OOPSLA 2025), collaboration | ~420 |
+| `structure-editors.md` | Structure editor design, projectional editing, rendering, text integration | ~400 |
+| `typed-holes-llm.md` | LLM + typed holes (OOPSLA 2024), static context, validation, ranking, AI pair programming | ~450 |
+
 **Common workflows:**
 - PL foundations: `lambda-calculus.md` → `type-systems.md` → `operational-semantics.md`
 - Dependent types: `type-systems.md` → `dependent-types.md` → `curry-howard.md`
 - Formal verification: `operational-semantics.md` → `program-verification.md` → `formal/lean-proof-basics.md`
 - Type theory: `lambda-calculus.md` → `type-systems.md` → `dependent-types.md` → `curry-howard.md`
+- Typed holes theory: `typed-holes-foundations.md` → `hazelnut-calculus.md` → `typed-holes-semantics.md`
+- Typed holes practice: `typed-holes-interaction.md` → `live-programming-holes.md` → `structure-editors.md`
+- AI-assisted coding: `typed-holes-foundations.md` → `typed-holes-llm.md` → Implement LSP+LLM integration
 
 ---
 
@@ -580,7 +597,7 @@ This index catalogs all atomic skills available in the skills system, organized
 **DSPy Framework:** Search `ml/dspy-*.md`
 **Diffusion Models:** Search `ml/diffusion-*.md`, `ml/stable-diffusion-*.md`
 **Advanced Mathematics:** Search `math/*.md` | Numerical: `math/linear-algebra-*.md`, `math/optimization-*.md`, `math/numerical-*.md`, `math/probability-*.md` | Pure math: `math/topology-*.md`, `math/category-theory-*.md`, `math/differential-equations.md`, `math/abstract-algebra.md`, `math/set-theory.md`, `math/number-theory.md`
-**Programming Language Theory:** Search `plt/*.md`, `plt/lambda-calculus.md`, `plt/type-systems.md`, `plt/dependent-types.md`, `plt/curry-howard.md`, `plt/operational-semantics.md`, `plt/program-verification.md`
+**Programming Language Theory:** Search `plt/*.md`, `plt/lambda-calculus.md`, `plt/type-systems.md`, `plt/dependent-types.md`, `plt/curry-howard.md`, `plt/operational-semantics.md`, `plt/program-verification.md`, `plt/typed-holes-*.md`, `plt/hazelnut-calculus.md`, `plt/live-programming-holes.md`, `plt/structure-editors.md`
 **React Native:** Search `mobile/react-native-*.md`
 
 ### By Task Type
@@ -943,7 +960,7 @@ This index catalogs all atomic skills available in the skills system, organized
 - Real-time: 4 skills
 - Data Pipelines: 5 skills
 
-**Specialized Domains** (53 skills):
+**Specialized Domains** (60 skills):
 - SAT/SMT Solvers: 3 skills
 - Lean 4: 4 skills
 - Constraint Satisfaction: 3 skills
@@ -953,7 +970,7 @@ This index catalogs all atomic skills available in the skills system, organized
 - DSPy Framework: 7 skills
 - Diffusion Models: 3 skills
 - Advanced Mathematics: 11 skills (4 numerical + 7 pure math)
-- Programming Language Theory: 6 skills
+- Programming Language Theory: 13 skills (6 core + 7 typed holes & live programming)
 - React Native: 4 skills
 - Formal Methods: 2 skills (verification-focused)
 
@@ -977,5 +994,5 @@ See `MIGRATION_GUIDE.md` for detailed mapping.
 ---
 
 **Last Updated:** 2025-10-25
-**Total Skills:** 155
+**Total Skills:** 162
 **Format Version:** 1.0 (Atomic)