Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 29 additions & 0 deletions CITATION.cff
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
cff-version: 1.2.0
message: "If you use this software, please cite it as below."
type: software
title: "Tropical Resource Typing"
abstract: "Lean 4 applied to max-plus (tropical) algebra to resource-aware type systems for compositional worst-case bounds. Provides a reusable resource-grade axis with parametric transport, a no-go theorem (hub_ceiling) refuting Protocol Squisher's universal-interoperability claim; separation proofs distinguishing tropical instances from finite {0,1,ω} reifications; and a separation proof that resource algebras measure Echo residues but are not Echo instances."
authors:
- family-names: "Jewell"
given-names: "Jonathan D.A."
orcid: "https://orcid.org/0000-0002-3078-6652"
repository-code: "https://github.com/hyperpolymath/tropical-types"
keywords:
- "tropical-algebra"
- "lean4"
- "epistemic-computing"
- "epistemic-infrastructure"
- "equivalence-aware-computing"
- "formal-verification"
- "hyperpolymath"
- "isabelle"
- "max-plus-algebra"
- "open-source"
- "research-software"
- "theorem-proving"
- "typed-provenance"
- "veridical-computing"
- "resource-aware-computing"
- "protocol-interop"
- "type-theory-in-number-theory"
- "worst-case-analysis"
Loading