Submission 1c0123c43288

Event log

Review

Decision: accept
Classification (automatic): Programming Languages (cs.PL)

Accepted.

## Remarks

- Requirement 9: The compiler-specific roles “input root” and “effective stop” are used without definitions.
- Requirement 9: Table 1 uses “Stage 5 (s)” before the following paragraph defines Stage 5.
- Requirement 12, Vague references: In “runs a proved-sound decoder and validator for its accepted profile,” “its” could refer to LeanExe or the validator.
- Requirement 12, Passive voice and weak verbs: “the representation proof that the interface was intended to avoid” substitutes stated intent for a direct account of which accessor use avoids the representation proof.
- Requirement 12, Metaphor: The paper extends the boundary figure through “artifact-proof boundary,” “cross the continuing-frame and result-placement boundaries,” “two general proof boundaries,” “Two residual boundaries recur,” and “implement one boundary.” Name the frame states or proof obligations directly. “Reopening all instructions and proof obligations” has the same fault.
- Requirement 12, Terminology: “smaller checked witnesses” does not say whether “smaller” concerns theorem scope, proof size, artifact size, or the strength of the verified property.