Skip to content

Commit a09ac77

Browse files
hyperpolymathclaude
andcommitted
chore(roadmap): tick WasmGC recursive types — layout/ subtree complete
All layout/ milestones now at 100%: - WHT_Var/WHT_Rec added to WasmHeapType - DecEq extended (16 new cases, all provable) - listTailField now uses WHT_Var 0 (proper isorecursive type) - listHeapTypeIsRec + listTailIsVar0 proofs added (both Refl) No open items remain in the layout/ subtree. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 3d7697e commit a09ac77

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

ROADMAP.adoc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
2323
* [x] katagoria L11-modal-box: comonad laws proved (Refl after case split — believe_me-free)
2424
* [x] typed-wasm DecEq: `DecEq (a, b)` instance added — WHT_Struct resolution chain complete
2525
* [x] protocol-squisher tropical: foldl-min optimality proved (`foldl_tcAdd_le_init/mem` + `minimax_path_optimal`)
26-
* [ ] typed-wasm layout: model WasmGC recursive types (List self-reference in Stdlib.idr)
26+
* [x] typed-wasm layout: WasmGC recursive types — WHT_Var/WHT_Rec added; List self-reference correct
2727
* [ ] Extend `Tropical.thy`: linorder instance, tropical matrices, Kleene algebra
2828
* [ ] Write arXiv paper on speculative tropical session types
2929
* [ ] typed-wasm ABI conventions for AffineScript + Ephapax cross-language calls (pending recursive types)

0 commit comments

Comments
 (0)