Guarded Realization Semantics: Occurrence-Sensitive Certificates and Behavior-Dependent Lower Bounds

SeungJu Lee

Distinct proofs, programs, formulas, or rewrite paths may have the same observable behavior while differing in occurrence structure, sharing, interfaces, or transformation history.…