Uh oh!
There was an error while loading. Please reload this page.
- Notifications
You must be signed in to change notification settings - Fork 0
A research repository on tropical (max-plus / min-max) algebra for resource-aware type systems, with machine-checked formalisations in Lean 4 and Isabelle/HOL, a Julia reference implementation, and a draft paper.
The core idea: conventional resource typing tracks resources additively; the tropical /
max-plus semiring replaces +/× with max/+ (or, dually, min/max), so type-system
operations compose to a worst-case bound — directly applicable to latency budgets,
worst-case stack/heap usage, and adversarial protocol round-counts.
- Lean 4 Formalization — two dependency-free proofs (the max-plus session-type
semiring and the min-max bottleneck transport semiring) plus the duality that connects
them.
lake buildgreen; axiom-audited. - Formal Verification Status — honest cross-prover state (Lean green; Isabelle under version drift on 2025-1).
| Area | Where | Notes |
|---|---|---|
| Lean 4 | TropicalSessionTypes.lean, TropicalAdapterPath.lean, lakefile.lean | pinned Lean 4.13.0, no Mathlib; lake build green |
| Isabelle/HOL | Tropical*.thy, ROOT | matrix algebra, Kleene, determinants, CNO |
| Julia | impl/ | small reference checker |
| Paper | Tropical Resource Typing For Protocols.pdf, docs/PAPER-OUTLINE.adoc | draft |
| Machine-readable | 0-AI-MANIFEST.a2ml, .machine_readable/6a2/ | bot entry points (6a2 sextet) |
GitHub is the source of truth and the in-repo docs are authoritative; this wiki navigates and summarises them. Key authoritative documents:
- Lean:
docs/LEAN-FORMALIZATION.adoc - Isabelle build state:
docs/BUILD-STATUS-2026-04-26.adoc,docs/HANDOVER_v2.adoc - Estate map:
docs/TROPICAL-ESTATE-MAP.adoc
Licence: MPL-2.0. © 2026 Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk.