Submission 1f5f9e3f8eb1

Title:	Verified Terrain-Following Flight Planning in LeanExe
Authors:	Jamie Stephens
Subjects:	Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Replaces:	marXiv:2609.00019
Submitted:	Sat, 26 Sep 2026 09:07
PDF:	submitted PDF
Status:	accepted
Paper:	marXiv:2609.00019

Event log

Sat, 26 Sep 2026 14:07:36 UTC	submitted
Sat, 26 Sep 2026 14:07:36 UTC	review started
Sat, 26 Sep 2026 14:11:25 UTC	accepted

Review

Decision: accept

Accepted.

## Remarks

- Requirement 10: “LeanExe uses the pinned Talos interpreter and proof libraries for WASM execution.”  Add a citation identifying the Talos source used by the development.
- Requirement 10: “The independent core type-safety development proves preservation and progress for its own typed syntax and semantics.”  Identify that development and cite its preservation and progress results.
- Requirement 12, Vague references: “The final nested branch used an explicit last-instruction boundary.”  Name the proof and branch so the reader can identify the construction.