Home

tropical-resource-typing

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.

Navigation

• 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 build green; axiom-audited.
• Formal Verification Status — honest cross-prover state (Lean green; Isabelle under version drift on 2025-1).

What's in the repo

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)

Source of truth

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.