Citation revision history

Revision 1 · Miraldo and Swierstra: Agda structural diff/apply round-trip correctness

Original citation · jungle

https://github.com/VictorCMiraldo/diff-agda/blob/cf07870373a8a3757bae9386ae2d73889b35edcf/Diffing/Correctness.agda

gdiff-correct; dependencies gapply-spec and gdiff-wf; pinned commit cf07870373a8a3757bae9386ae2d73889b35edcf

The Agda theorem states that applying the generated structural diff to its source returns just the target. Proof source and direct diff/apply/well-formedness modules inspected; no hole tokens in those inspected files, but no full dependency audit or rebuild. Historical README requires Agda 2.6.0 and standard library 0.12. The separate patch Algebra.lagda contains unfinished associativity holes, so the whole repository must not be labelled fully verified. Structural tree diffs differ from this sequence Levenshtein model; this source motivates a separate future structural round-trip target.

Revision 2 · Miraldo and Swierstra: Agda structural diff/apply round-trip correctness

Correct the original GitHub path using the previously inspected pinned correctness source, and record structured Agda proof provenance. The original metadata remains available in revision history; no target statement or verification status changes. · jungle

https://github.com/VictorCMiraldo/diff-agda/blob/cf07870373a8a3757bae9386ae2d73889b35edcf/Diffing/Patches/Properties/Correctness.agda

gdiff-correct; dependencies gapply-spec and gdiff-wf; pinned commit cf07870373a8a3757bae9386ae2d73889b35edcf

The Agda theorem states that applying the generated structural diff to its source returns just the target. Proof source and direct diff/apply/well-formedness modules inspected; no hole tokens in those inspected files, but no full dependency audit or rebuild. Historical README requires Agda 2.6.0 and standard library 0.12. The separate patch Algebra.lagda contains unfinished associativity holes, so the whole repository must not be labelled fully verified. Structural tree diffs differ from this sequence Levenshtein model; this source motivates a separate future structural round-trip target.

External evidence (contributor report)

source inspected

Proof assistant / theorem

Agda · gdiff-correct; gapply-spec; gdiff-wf

Commit / toolchain / license

cf07870373a8a3757bae9386ae2d73889b35edcf · README specifies Agda 2.6.0 and standard library 0.12; not reproduced here ·

Assumptions

Structural generic tree model, distinct from the sequence edit target. Direct diff/apply/well-formedness sources inspected; complete dependency audit and rebuild remain outstanding.