ch:simple-types: ch:simple-types

Problem and result. Build one check-and-run path for the Boolean/function fragment. It returns a validated derivation for the source, evaluates by capture-avoiding call-by-value steps, and validates the final value at the same type. The finished program evaluates $\mathit{not}\mathsf{tt}$ to $\mathsf{ff}$ and $\mathit{not}\mathsf{ff}$ to $\mathsf{tt}$; it rejects the two ill-typed terms and a raw nested-shadowing input; and it retains $\mathbf{2}$ after reduction.

Representation. Use natural numbers as names. Equality and least-fresh-name selection are decidable and the printed witness remains readable; de Bruijn indices would remove alpha-renaming but require shifting at every binder. Use an ordered list context because it mirrors the printed context rules and makes duplicate declarations observable; a finite map would speed lookup but erase insertion order unless it carried extra evidence. A successful checker result is Checked Ty Derivation, not a Boolean. The tree costs more space than a Boolean answer but an independent traversal can replay every Var, Lam, App, Boolean, and If node. Use an option-valued one-step function plus a fueled driver. A big-step evaluator is shorter for successful runs, but the one-step interface mirrors the preservation cases and reveals the selected call-by-value order.

First complete version. Define Ty, Term, the ordered binding list, and the six derivation constructors. Implement lookup and a context-formation test before inference. At a lambda, reject the raw input when its binder is already in the context; the independent validator performs the same check before replaying the body evidence. Application synthesis requires an arrow result for the function and exact domain equality for the argument. Conditional synthesis requires a Boolean guard and equal branch types.

Next implement free-name calculation and capture-avoiding substitution. The fresh name is larger than the target and every name in the body and replacement. Implement the six call-by-value rules, then a fueled driver. The first end-to-end run checks $\mathit{not}\mathsf{ff}:\mathbf{2}$, evaluates it to $\mathsf{tt}$, and rechecks the result at $\mathbf{2}$. This is already the promised check-and-run result; later tests enlarge its coverage rather than supplying its missing evaluator.

Remaining cases. Add the symmetric $\mathit{not}\mathsf{tt}$ run, the stuck application, the self-application rejection, and validation of the evaluated result, in the same order as the canonical-forms, preservation, and progress cases. Add the raw term $\lambda 0:\mathbf{2}.\lambda 0:\mathbf{2}.0$: inference and evidence replay must both reject its duplicate binder. Its alpha-class can be typed after freshening, but this artifact’s raw-input contract requires distinct binders. Keep the universal size argument for $A=A\to B$ as a printed proof rather than treating finite rejection as that proof.

A failing version. The function substituteNaive descends below a binder that occurs free in the replacement. On the source body $\lambda 1:\mathbf{2}.0$ and replacement variable (1), it returns $\lambda 1:\mathbf{2}.1$, capturing the inserted name. The correct substitution freshens that binder, and the named witness checks both outputs. A second faulty version prepends a lambda binder without checking the existing context. Both inference and evidence replay then accept the nested-shadowing input through an ill-formed context; the new regression kills that version.

Acceptance test. Run the four exact commands printed in the artifact README. Require eight PASS lines, the final summary, a silent check, one passing corpus test, and an empty audit.

Mathematical boundary. These cases illustrate progress and preservation. They prove neither theorem and do not establish normalization.