Available supplements

Chapter 3: bounded first-order proof search

The directory artifacts/ch03-first-order/ contains a Kappa proof-producing implementation of the finite-height Ax, implication, and universal fragment used in definition 3.35, exercise 3.6. It returns a named derivation, checks every node independently, prints the tree, and memoizes both success and failure under alpha-normal keys. Its executable formula language has unary $P/Q$ atoms, implication, and universal formulas whose single bound token does not occur beneath a nested universal; it does not represent the chapter’s general first-order binding syntax. It targets portable kappa-v1 and pins the clean compiler source commit 216f913e e9d94519 ccb3d9e1 6f6f9d36 52188fe. The single accepted corpus SHA-256 is . Run

kappa test \
  artifacts/ch03-first-order/corpus.kp

and use run to obtain ten case lines, the printed tree, and

All 10 Chapter 3 corpus cases passed.

The mathematical height is checked from the returned tree; a separate administrative budget justifies the mutually recursive Kappa implementation. The checker also rejects an out-of-pool universal-left witness and a nonleast universal-right name. The in-file validAxMutant deletes only the Ax membership test, and the harness kills it with one forged certificate. Kappa’s audit is empty and no compiler defect was encountered. This is finite executable behavior, not evidence for unrestricted proof search, cut elimination, or normalization.

Chapter 3: Hindley–Milner inference

The directory artifacts/ch04-hm/ in the same repository commit as this book contains a Kappa implementation of the pure let-language, first-order unification, and Algorithm W of chapter 3. It targets the portable kappa-v1 profile and pins the clean Kappa source commit 53ce3a88e6e cf3f6729a3e02e75d836d00f301c0; the companion README records the specification digest, compiler digest, platform, relevant conformance limits, and accepted-output summary. The accepted corpus SHA-256 is fdc429ef7be6f7776646092eaec468647b849542ffdb851afb9431daf05a0d09. From the repository root, run

kappa test artifacts/ch04-hm/hm.kp

The Appendix T harness typechecks and interprets the program, checks five successful principal schemes, including the complete $\mathsf{twice}\mathsf{twice}$ calculation of section 3.7, and one occurs-check failure. Two further cases exercise generic constructor decomposition together with the opposite cyclic orientation, and a distinct-constructor clash. Three final cases replay a named unifier on its original equations, infer under an open context whose existing variable is index zero, and test capture-avoiding scheme substitution. To print the case-by-case trace, run

kappa run artifacts/ch04-hm/hm.kp

The expected final line of that trace is

All 11 Chapter 4 corpus cases passed.

The principal-scheme comparison implements the syntactic criterion of lemma 3.9 in both directions. The supplement checks implementation behavior; it does not mechanize the termination, MGU, or principal-pair proofs. Its unifier carries computed recursion measures that mirror the printed termination proof. Kappa accepts every recursive definition, and the unsafe/debug audit is empty; there is no admitted lemma, unsafe flag, or unchecked termination escape. The run uses Kappa’s tree-walking interpreter and does not claim interpreter–native-backend parity.

Chapter 6: dimension normalization and coherent units

The directory artifacts/ch6-dimensions/ contains a Kappa data-level implementation of the normalized three-base dimension calculations used in chapter 6. It checks a principal one-parameter equation family, a parity rejection, two polymorphic-square instantiations, and the kilogram–meter to gram–centimeter mechanics conversion. It uses the same pinned portable kappa-v1 compiler identity as the preceding supplement. The accepted corpus SHA-256 is f9679c5352155f4acf298d9478459c8063fdd87554c9a8419714b79d6c0c9c4f. Run

kappa test \
  artifacts/ch6-dimensions/corpus.kp

and use run to obtain six case lines followed by

All 6 Chapter 6 corpus cases passed.

The companion checks calculations, not the Smith-normal-form, principal-W, safety, or invariance proofs. Its audit is empty and no compiler defect was encountered.

Chapter 4: strict rows and qualified inference

The directory artifacts/ch7-rows/ contains a Kappa implementation of the strict unique-label row calculus of chapter 4: normalized lacks predicates, the mutually recursive constrained row inserter and solver, and qualified Algorithm W for the chapter’s pure let-language with its saturated record and variant forms. The rows are object-language nominal data; the supplement does not ask Kappa’s own row inference to stand in for the calculus being tested.

The companion targets the portable kappa-v1 profile and pins the clean Kappa source commit 53ce3a88 e6ecf3f6 729a3e02 e75d836d 00f301c0. Its README records the specification, conformance-ledger, accepted-source, and compiler digests, GHC 9.14.1, arm64 macOS 26.3.1, the relevant conformance limits, and the accepted-output summary. The accepted corpus SHA-256 is 704e9f22f760eda355625009eb2d72fb595c3be2b278d405df5abc5c0bc1e8e8. From the repository root, run

kappa test \
  artifacts/ch7-rows/corpus.kp

The harness typechecks and interprets eleven cases: record extension and restriction; payload- and residual-receiving variant branches; fresh-name selection above a nonempty context; qualified generalization of $\mathsf{withSecure}$ with two admissible instances; a crossing-open-tail row solve with an explicit returned-substitution replay and principal-factor check; a computed trace naming every solver clause on that path; termination under an input-derived bound; rejection of empty-row insertion, a row occurs-check input, a contradictory lacks constraint, and a literal duplicate row; and execution of a nonprincipal naive closed-tail solver. The public solver validates strict formation before solving and reports resource exhaustion separately from calculus failure. To print the trace, run

kappa run \
  artifacts/ch7-rows/corpus.kp

Its final line is

All 11 Chapter 7 corpus cases passed.

The run also prints the computed crossing trace U-Row -> I-Skip -> I-Var -> U-Var -> U-Done. The separate audit command prints an empty list: the program contains no unsafe/debug facility, admitted lemma, or unchecked termination escape. This tree-walking interpreter run checks implementation behavior. It neither mechanizes the chapter’s termination, principal-unifier, Algorithm W, or safety theorems nor claims interpreter–native-backend parity.

Seminar acceptance capsules for Chapters 1–12

All twelve project capsules target portable kappa-v1 and pin Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0. That source is the named commit of https://github.com/wabbit-corp/kappa-haskell.git. A clean checkout with GHC 9.14.1 and Cabal 3.10 or later can reproduce the local compiler as follows:

KAPPA_SOURCE_DIR="$(mktemp -d)"
git clone https://github.com/wabbit-corp/kappa-haskell.git \
  "$KAPPA_SOURCE_DIR"
git -C "$KAPPA_SOURCE_DIR" checkout --detach \
  53ce3a88e6ecf3f6729a3e02e75d836d00f301c0
(
  cd "$KAPPA_SOURCE_DIR"
  cabal build kappa-haskell:exe:kappa
  cabal list-bin kappa-haskell:exe:kappa
)

The accepted arm64 macOS 26.3.1 build used GHC 9.14.1 and Cabal 3.16.1.0. Its repository-local compiler SHA-256 is 476688a4b6078aaef4e7a23f46383a3879df40d391bca7d6878545197a002d01. An independent clean build from the same source commit had native-binary SHA-256 82fa23863a04e65ee22b998f1cad6946752db222160d2cc287f685e65bdfe3d0 and replayed the Chapter 1 capsule successfully. The native digests are host/build evidence; the source commit and four-command replay are the portable pins. After installing that executable as kappa on PATH, run:

kappa check PATH/corpus.kp
kappa test  PATH
kappa run   PATH/corpus.kp
kappa audit PATH/corpus.kp

The check command checks the source, test compares its output with the declared oracle, run prints that output, and audit reports unsafe or unchecked facilities. Every successful check is silent and every successful audit is []. Each README and raw transcript records its exact mutation evidence: either a rejected typechecking mutation or an executable mutant killed by an accepted test. One killed mutation is not evidence that every printed case is independently sensitive; the entry below states whether the companion is an implementation or only a finite boundary card.

Chapter 1: complete named evaluator

Reproducibility record for exercise 1.20. artifacts/ch01-ulc-evaluator/corpus.kp has SHA-256 ac8ef97fb42871b0a6028d7e79c7c243a8d8ecc4757a0b72242e45c7c88e41ec and ends All 7 Chapter 1 corpus cases passed. It implements the complete named grammar, free-name calculation, deterministic fresh-name choice, capture-avoiding substitution, all eleven one-step rule families, the fueled driver, and final classification. Its executable substituteNaive mutant is rejected by a named capture witness. The companion file artifacts/ch01-ulc-evaluator/starter.kp.template contains the same datatypes, helpers, printer, and seven tests, with four numbered implementation holes for the practical project. The completed-corpus run proves no alpha-compatibility, determinism, divergence, or normalization result. The test and run commands use Kappa’s tree-walking interpreter; this acceptance does not invoke the native backend and makes no interpreter–native-backend parity claim. The pinned conformance ledger has known gaps, but this portable kappa-v1 corpus uses only nominal data, lists, pure functions, and top-level structural or explicitly measured recursion. It does not rely on block-local recursion, open effect rows, unsafe/debug facilities, or a native backend.

Chapter 2: syntax-directed checking

Reproducibility record for exercise 2.22. artifacts/ch02-stlc-safety-checker/ has accepted SHA-256 and ends All 8 Chapter 2 corpus cases passed. It implements the named Boolean/function syntax, returns independently checked derivation evidence, executes the six call-by-value rules, and uses capture-avoiding beta substitution. Inference and evidence replay both reject a raw nested-shadowing input whose duplicate binder would form an invalid context. A named witness kills the executable naive-substitution mutant. The README and transcript pin compiler repository, source commit, packaged binary hash, and the exact check/test/run/audit commands. The finite run does not prove progress, preservation, or normalization.

Chapter 3: bounded LJ search

Reproducibility record for exercise 3.10. artifacts/ch03-first-order/ has accepted SHA-256 and ends All 10 Chapter 3 corpus cases passed. It returns, prints, and independently validates the least-height proof, checks the negative bound range and right-to-left fallback, rejects two malformed quantified-rule certificates, reinstantiates an alpha-normal cached success, and kills the in-file membership-only Ax mutant. The accepted language has unary $P/Q$ atoms, implication, and a single bound token that may not occur beneath a nested universal. The historical shape-only capsule is not an acceptance record. It remains at artifacts/ch03-bounded-lj-search/ solely to preserve the earlier finite boundary example; its frozen corpus SHA-256 is . The run proves neither search completeness nor cut elimination.

Chapter 3: substitution-based Algorithm W

Reproducibility record for exercise 4.16. artifacts/ch04-hm/ has accepted SHA-256 and ends All 11 Chapter 4 corpus cases passed. This is the sole package named by hm-inferencer; it implements the pure W signature, replays a named unifier, and checks the open-supply and scheme-capture regressions. These finite runs do not prove principality.

Chapter 5: finite replay

Reproducibility record for exercise 5.7. artifacts/ch5-semi-unification-reduction/ has accepted source SHA-256 e05ea0b858970b14bc11aa37ac05ac88341a327186ab7179a81e4fbdc150079a. It targets portable kappa-v1, pins Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0, and was checked with repository-local compiler SHA-256 476688a4b6078aaef4e7a23f46383a3879df40d391bca7d6878545197a002d01. Run

cd artifacts/ch5-semi-unification-reduction
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The run prints and replays one equation, two inequalities with different matchers, a symbolic node-count certificate derived from the exact $\alpha \to \alpha {⪯}_{\mathsf{su}}\alpha$ input, and the protected inequality generated by polymorphic recursion. Each trace, status, and the aggregate summary is constructed from computed results; inequality traces include the outer substitution, local matcher, and replay. The run uses the ASCII names D, C, B, and A for $\delta$, $\gamma$, $\beta$, and $\alpha$, respectively. It ends All 4 Chapter 5 corpus cases passed. Audit is []. A check-clean mutation that omits the local matcher makes all three matcher-dependent inequality traces fail, makes the two aggregate status lines fail, and changes the aggregate summary to failure. The corpus does not implement witness search and proves no reduction or undecidability theorem.

Chapter 6: dimensions and Smith divisibility

Reproducibility record for exercise 6.9. artifacts/ch6-dimension-inferencer/ has accepted SHA-256 . It targets Kappa source commit 216f913ee9d94519cccb3d9e16f6f9d3652188fe and compiler SHA-256 . Run

cd artifacts/ch6-dimension-inferencer
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The source traverses variables, literals, lambdas, applications, lets, three binary arithmetic constructors, and integer power while threading disjoint supplies and an ordered mixed equation store. In the empty environment it generalizes the inferred square type, replays every generated square equation, computes the canonical sum, and rejects mismatch and odd-pivot inputs. Its single-row solver eliminates a coefficient only when it divides all the others. On the row $(2,3)$ for ${\delta }^2{ϵ}^3=L$, neither coefficient divides the other, so the solver returns Unsupported. The run ends All 7 Chapter 6 corpus cases passed.; audit is []. Applying the check-clean mutation with SHA-256 makes the pivot selector accept ${\delta }^2=L$: check remains successful and the test oracle fails. The seminar project adds the Euclidean column operations that replace $(2,3)$ by $(1,0)$, subtracts environment variables before two-sorted generalization, and threads substitutions in Algorithm W’s left-to-right order. The finite run proves neither the general Smith theorem nor principal inference.

Chapter 4: strict-row boundary

Reproducibility record for exercise 7.12. artifacts/ch7-rows/ has accepted source SHA-256 . It uses the portable kappa-v1 profile and the repository-local compiler SHA-256 . Run

cd artifacts/ch7-rows
../../.local-tools/kappa/bin/kappa check corpus.kp
../../.local-tools/kappa/bin/kappa test  corpus.kp
../../.local-tools/kappa/bin/kappa run   corpus.kp
../../.local-tools/kappa/bin/kappa audit corpus.kp

The run prints the computed clause trace U-Row -> I-Skip -> I-Var -> U-Var -> U-Done, replays the returned substitution in the crossing equation, rejects insertion into the empty row and a row occurs-check input, rejects duplicate formation, and ends All 11 Chapter 7 corpus cases passed. Audit is []. The check-clean mutation with SHA-256 fabricates success in I-Empty; its test oracle fails. The corpus does not prove termination, principality, coherence, inference soundness, or type safety.

Chapter 8: record compilation

Reproducibility record for exercise 8.9. artifacts/ch8-polymorphic-record-compiler/ has accepted source SHA-256 0c5993be5f25d254a6dabdcf53437f5cb6a45bcc78cf6ccfa1d783ccbd56b82d. It uses the same portable profile, source pin, and repository-local compiler digest recorded above. The four commands are

cd artifacts/ch8-polymorphic-record-compiler
../../.local-tools/kappa/bin/kappa check corpus.kp
../../.local-tools/kappa/bin/kappa test  corpus.kp
../../.local-tools/kappa/bin/kappa run   corpus.kp
../../.local-tools/kappa/bin/kappa audit corpus.kp

The source uses separate recursive source and target ASTs, typed lambda nodes, kinded type nodes, and pair-keyed index assignments. The run prints both computed layouts and selections, the full selector, the target applications ending in $@1$ and $@2$, the nested- outer and nested- same- label terms, and a variable-operator type application. Only after printing the selection terms does the evaluator return Joe and Hanako. Missing and duplicate fields are rejected before target execution. The run ends All 13 Chapter 8 corpus cases passed.; audit is []. The check-clean mutation with SHA-256 replaces the distinct-label guard by True; check still succeeds and the duplicate-label test oracle fails, forcing the aggregate failure summary. The finite run proves neither compiler totality, preservation, nor the logical relation.

Chapter 5: finite explicit checker

Reproducibility record for exercise 9.15. artifacts/ch9-system-f-checker/ has accepted SHA-256 . It targets portable kappa-v1, uses Kappa source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0, and was checked with the repository-local compiler whose SHA-256 is . From the repository root, run:

cd artifacts/ch9-system-f-checker
../../.local-tools/kappa/bin/kappa check corpus.kp
../../.local-tools/kappa/bin/kappa test  corpus.kp
../../.local-tools/kappa/bin/kappa run   corpus.kp
../../.local-tools/kappa/bin/kappa audit corpus.kp

The complete concise run output is:

PASS identity type-beta
PASS derivation replay
PASS surface rejection
PASS alpha and type scope
PASS term capture avoidance
PASS type capture avoidance
PASS Church-product eta boundary
PASS compatible constructor descent
PASS reduct typing and evidence
PASS malformed evidence rejection
PASS ill-formed context rejection
All 11 Chapter 9 corpus cases passed.

The check is silent. The test reports one passed source file and no failures, unsupported cases, or harness errors; audit is []. The preserved check-clean mutation artifacts/ch9-system-f-checker/mutant-no-lambda-descent.patch, SHA-256 , replaces compatible descent below Lam by the empty reduct list. Applying it to a disposable copy with patch -p1 < mutant-no-lambda-descent.patch leaves kappa check successful, but kappa test reports FAIL compatible constructor descent and the conditional aggregate Chapter 9 corpus failed.

The corpus implements the exact five-constructor grammar, context-formation guards, de Bruijn substitutions, derivation evidence and independent replay, and compatible one-step beta reduction. Its finite runs prove neither preservation, confluence, normalization, consistency, nor an eta principle.

Chapter 6: finite relations

Reproducibility record for exercise 10.10. artifacts/ch10-parametricity-calculator/corpus.kp has accepted SHA-256 . It targets portable kappa-v1 and was checked with Kappa source commit and compiler SHA-256 , built by GHC 9.14.1 for arm64 macOS. From artifacts/ch10-parametricity-calculator/, run

../../.local-tools/kappa/bin/kappa check corpus.kp
../../.local-tools/kappa/bin/kappa test  corpus.kp
../../.local-tools/kappa/bin/kappa run   corpus.kp
../../.local-tools/kappa/bin/kappa audit corpus.kp

The check is silent, the test reports one passing corpus, and audit is []. The run reports ten named witnesses, including

PASS output beta-identity witnesses the two client outputs

Its fixed-point line reports PASS fixed-point singleton is rejected because Bottom Bottom is absent. The conditional final line is

All 10 Chapter 10 corpus cases passed.

The earlier lines separately exercise finite identity membership, graph membership, graph arrow lifting, the initial counter pair, step and observer liftings along the two-step path, and both independently computed client outputs.

The preserved check-clean mutation artifacts/ch10-parametricity-calculator/mutant-ignore-strictness.patch, SHA-256 , removes the $\mathrm{\perp }R\mathrm{\perp }$ test. Apply it to a disposable copy with patch -p1 < mutant-ignore-strictness.patch. Kappa check still succeeds, but Kappa test reports both FAIL fixed-point singleton is rejected because Bottom Bottom is absent and the conditional aggregate Chapter 10 corpus failed.

The finite witness lists execute only the instances printed by the program. They do not universally quantify over all beta-classes and therefore prove neither the abstraction theorem, the full counter arrow obligations, the graph lemma, nor identity extension. The fixed-point row witnesses the necessity of strictness; it does not construct a domain model or verify admissibility.

Chapter 9: finite kind checking

Reproducibility record for exercise 11.9. artifacts/ch11-fomega-checker/ has accepted SHA-256

and targets portable kappa-v1. It was checked with Kappa source commit

and compiler SHA-256

built by GHC 9.14.1 for arm64 macOS 26.3.1. From the repository root, run kappa check, kappa test, kappa run, and kappa audit on artifacts/ch11-fomega-checker/corpus.kp; the run ends All 4 Chapter 11 corpus cases passed. It implements finite kind/application checking, a direct closed double-power computation, and a distinct-normal-head comparison; it does not implement the term-level dmap checker or prove confluence, normalization, or decidability.

Chapter 10: finite package checker

Reproducibility record for exercise 12.10. artifacts/ch12-existential-package-checker/ has accepted SHA-256 907bb62a47bcb8fcd1bfb5b060cd274ad04956be4819758d3449c78bab5bfab8 and targets portable kappa-v1. It was checked with the same Kappa source commit, compiler binary, GHC version, and arm64 macOS platform recorded for the Chapter 11 corpus immediately above. Run the same four commands on artifacts/ch12-existential-package-checker/corpus.kp; the run ends All 4 Chapter 12 corpus cases passed. It implements finite syntax-directed existential pack/unpack checking, the no-escape test, compatible call-by-value evaluation, and two concrete representations. The fixed-record case is an explicitly rejected outside-grammar node. It does not prove representation independence.

Chapter 11: finite qualified-type resolution

Reproducibility record for exercise 11.8. The directory artifacts/ch13-qualified-resolver/ contains a portable Kappa implementation of the finite ${\mathrm{QTC}}_0$ resolver from chapter 11. Class tags, type trees, instance heads, premises, local evidence, and evidence trees are explicit data; Kappa’s own implicit or type-class machinery is not used as an oracle. The public resolver first validates nonoverlap, constructor-headed formation, and the proper-subterm condition. Its structural work bound uses both the requested type and the largest premise list, and the module exports no raw helper that can bypass validation.

The accepted source has SHA-256

It targets portable kappa-v1 and was checked with the repository-local compiler built from source commit

The README records the compiler, specification, and conformance-ledger digests. Run

cd artifacts/ch13-qualified-resolver
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The run prints seven PASS lines and ends with

All 7 Chapter 13 corpus cases passed.

The audit result is []. Three hidden accepted assertions check exact-local selection before superclass evidence, the structural work bound on three distinct sibling premises, and rejection of a primitive Eq Int clause that overlaps the effective projection derived from Ord Int. Four typechecking mutations respectively bypass normal validation order, erase the proper-subterm guard, discard local evidence at the public boundary, and disable effective superclass lookup. Each changes the exact output and makes kappa test exit with status one; the README and transcript record their source digests.

The finite run checks validation, selection priority, and evidence-tree construction on the named corpus. It proves neither universal resolution termination or functionality, inference soundness or principality, dictionary-elaboration typing or operational correspondence, nor coherence. No unsafe feature, admitted lemma, or unchecked termination escape is used.

Chapter 12: finite module matching and identity allocation

Reproducibility record for exercise 12.11. The directory artifacts/ch14-ml-modules/ contains the portable Kappa companion to the reduced module calculus of chapter 12. Its finite signatures represent manifest, hidden, and first-component-dependent static identities; hierarchy matching is covariant, functor matching is contravariant in its domain, and opaque sealing and generative application thread an internal fresh-name supply. A separate applicative mode uses structural identities and is not part of the chapter’s principal generative calculus. The target elaborator records only existential, product, and arrow shapes.

The accepted source has SHA-256

It targets portable kappa-v1 and was checked with the repository-local compiler built from source commit

The compiler binary, specification, and conformance-ledger digests are recorded in the companion README. Run

cd artifacts/ch14-ml-modules
kappa check corpus.kp
kappa test  corpus.kp
kappa run   corpus.kp
kappa audit corpus.kp

The run prints nine PASS lines and ends with

All 9 ML-modules corpus cases passed.

The audit result is []. Three independently replayed, typechecking mutations respectively ignore first-component sharing, reuse an opaque-seal supply, and give generative applications an applicative identity; each changes the exact oracle and makes kappa test exit with status one. The README and TRANSCRIPT.txt record their source digests and outputs.

The finite run checks the observable cases named by the seminar problem. It does not prove signature matching, singleton self-recognition, elaboration soundness or simulation, representation independence, principal matching, or any theorem about Kappa. No unsafe feature, admitted lemma, or unchecked termination escape is used.

Chapter 15: finite linking and definedness

Reproducibility record for exercise 15.6. The portable source is artifacts/ch15-mixml-definedness/corpus.kp. Its SHA-256 is

Acceptance used the repository-local compiler built with GHC 9.14.1 for arm64 macOS 26.3.1 from the clean Kappa source commit

The compiler binary SHA-256 is

From the repository root, the exact commands are

kappa check \
  artifacts/ch15-mixml-definedness/corpus.kp
kappa test \
  artifacts/ch15-mixml-definedness/corpus.kp
kappa run \
  artifacts/ch15-mixml-definedness/corpus.kp
kappa audit \
  artifacts/ch15-mixml-definedness/corpus.kp

Check is silent and test passes one corpus. The exact run output is

PASS ordered accepted
PASS early-read rejected
PASS duplicate-export rejected
PASS type-mismatch rejected
PASS cycle rejected
All 5 Chapter 15 corpus cases passed.

Audit prints []. Hidden assertions require the complete two-component merge and rejection of both orders of the cyclic initialization. The program constructs ${\mathsf{Mix}}_0$’s finite merged signature and checks its initialization invariant. It does not implement full MixML or LTG and proves no metatheorem.

Chapter 16: finite evidence resolution

Reproducibility record for exercise 16.15. The portable Kappa source is artifacts/ch16-mtc-resolution/corpus.kp. Its SHA-256 is

It was checked with the repository-pinned Kappa compiler at source commit

The tested compiler binary has SHA-256

From the repository root, run

kappa check artifacts/ch16-mtc-resolution/corpus.kp
kappa test  artifacts/ch16-mtc-resolution/corpus.kp
kappa run   artifacts/ch16-mtc-resolution/corpus.kp
kappa audit artifacts/ch16-mtc-resolution/corpus.kp

The run reports six passing output cases and ends with

All 6 Chapter 16 corpus cases passed.

The audit result is []. The standard-acceptance case additionally checks a forty-premise admissible stress declaration and rejects deliberately misnamed evidence. Three typechecking mutations are killed by the inline oracle: accepting every environment (SHA-256 46e76b4f…a768668), restoring an incomplete linear fuel bound (b5c29031…98b79), and omitting the evidence-name comparison (83bea00f…b3729). Each makes kappa test exit with status 1. The complete accepted-and-mutation command transcript has SHA-256 250cb8bc 4a877ff4 0845dd79 0d2bde55 628894a9 992b976f ce937041 cffbde50.

The archived modular-implicits checkout is separate read-only source evidence. Its clean Git identity is 92e45da5 c8a4c2db 8b2cd5be 28a5bec2 ac2181f1, and the concrete specimen is testsuite/tests/typing-modular_implicits/show.ml. The book does not present that historical OCaml compiler as a book-authored executable.

The Kappa run illustrates validation, search, error classification, and evidence insertion for the finite ${\mathsf{MTC}}_0$ sublanguage. It is not a mechanization of the chapter’s proofs, the published higher-order module calculus, current OCaml, or SI.

Chapter 17: the Brown–Palsberg $F_{\omega }$ self-representation artifact

Reproducibility record for exercise 17.10.

The portable seminar companion is artifacts/ch17-fomega-selfrepr/corpus.kp, distinct from the historical Brown–Palsberg reproduction recorded below. It implements a finite four-constructor quotation, unquotation, size fold, normality test, and quotation-image check as ordinary Kappa data. Its accepted SHA-256 is 721072d5d241c7d8ff18faa38e9d01a5cb89d26270345e44eb9c9a4f82505276; it uses portable kappa-v1 at the repository Kappa pin. Run

kappa check artifacts/ch17-fomega-selfrepr/corpus.kp
kappa test  artifacts/ch17-fomega-selfrepr/corpus.kp
kappa run   artifacts/ch17-fomega-selfrepr/corpus.kp
kappa audit artifacts/ch17-fomega-selfrepr/corpus.kp

The run prints six PASS lines and then this summary:

The audit prints []. The README records three typechecking negative controls: swapping application children, omitting the application argument from size, and accepting a lambda-headed application as normal. Each makes kappa test fail. The corpus checks only the finite fold equations, not full $F_{\omega }$ kinding or normalization.

The published POPL 2016 artifact is preserved unchanged in the reference library. Its ZIP has SHA-256 1bfeb2261f0970cc012d2bdc 481b6dda ec99fd62 b1d24d1f 4ebec1bc a5b0b045 and contains 101 regular files. The release does not pin GHC, Cabal, dependencies, or a package index, and its build script uses the obsolete cabal sandbox workflow. An exact reconstruction of the authors’ historical environment is therefore not determined by the archive.

The directory artifacts/ch17-fomega-selfrepr/ contains a separately labeled modern compatibility check. On GHC 9.14.1 and Cabal 3.16.1.0, an unmodified fresh extraction fails because liftIO is not in scope. The recorded patch adds only the missing imports of liftIO and join; it changes no definition, type, algorithm, test, or $F_{\omega }$ specimen. Applied to another fresh extraction, the port builds offline and passes all 94 unit tests. For each of the 53 specimens selected by the published script, the corresponding modern executable prints exactly Succeeded.

The original runners do not reliably communicate failure through their exit status. The replay therefore asserts output text and includes negative controls: unequal terms print Failed. even though that runner exits successfully, while an ill-typed specimen and malformed input produce the expected diagnostics. The companion README records the exact commands, host, dependency plan, patch digest, and captured summary. These runs confirm the behavior of the implementation and published examples under the stated port. They do not replace the local proofs of quotation, unquotation, and the syntax-directed operations in section 7.14, and they are not presented as a reconstruction of the unpinned 2015 toolchain.

The local proof also repairs four source transcriptions. In the term-equivalence display before the paper’s Theorem 6.3, the application conclusion is $e_1^{\prime }{e}_2^{\prime }$, not $e_2^{\prime }{e}_2^{\prime }$. In the normal-form proof, $K_{\mathsf{Nat}}$ must be $K_{\mathsf{Bools}}$. The constructor-abstraction premise in Appendix Lemma A.33 is the judgment for its body, rather than a copy of the quantified result judgment. Finally, the constructor-application case in Appendix Lemma A.32 uses $\mathrm{\neg }(\mathsf{normal}(e)\wedge \mathsf{neutral}(e))$; it does not assert the stronger conjunction $\mathrm{\neg }\mathsf{normal}(e)\wedge \mathsf{neutral}(e)$. The book’s displayed definitions and proofs use these corrected forms and distinguish term beta from constructor normalization explicitly.

The reference library also contains frozen dossiers for later planned developments, including the status-bounded Higher-OTT/Narya material. A dossier becomes a book supplement only when its owning chapter has a complete local theorem and a reproducible command record. No scaffold claims an executable result merely because a reference artifact has been archived.

Chapter 8: deterministic Kernel bounded subtyping

Reproducibility record for exercise 18.16.

The directory artifacts/ch18-subtyping/ contains a Kappa implementation of the deterministic Kernel subtype algorithm of section 8.6. Types, finite-map records, and ordered bound contexts are object-language nominal data; the supplement does not ask Kappa’s own type relation to stand in for the calculus being tested.

The companion targets the portable kappa-v1 profile and pins the clean Kappa source commit 53ce3a88e6e cf3f6729a3e02e75d836d00f301c0. The accepted corpus SHA-256 is 458064b9068692b1613e316a7c526790bb082e0393822e8fe2f60faef14b647c. Its README records the specification, conformance-ledger, accepted-source, and compiler digests, GHC 9.14.1, arm64 macOS 26.3.1, relevant conformance limits, and the accepted-output summary. From the repository root, run

kappa check \
  artifacts/ch18-subtyping/corpus.kp
kappa test \
  artifacts/ch18-subtyping/corpus.kp

The check is silent, and the harness typechecks and interprets seven cases: the equality, top, and bottom priority branches; incompatible-shape failure; source-bound promotion without target promotion; record width, depth, and permutation; arrow variance and its false reverse; direct alpha-equality of renamed binders; invariant universal bounds whose body comparison requires renaming and source-bound promotion; different-bound failure; and an explicit full- boundary specimen. To print the trace, run

kappa run \
  artifacts/ch18-subtyping/corpus.kp

Its final line is

All 7 subtyping corpus cases passed.

The boundary helper runs a single displayed full-universal rule. Both premises lie in Kernel; this is not a full- decision procedure. The separate audit command prints []: the program contains no unsafe/debug facility, admitted lemma, or unchecked termination escape. No Kappa compiler defect or conformance-suite change was required. This tree-walking interpreter run checks implementation behavior. It neither mechanizes termination, soundness, completeness, or undecidability nor claims interpreter–native-backend parity.

Chapter 19: finite polar biunification

Reproducibility record for exercise 19.7. The source artifacts/ch19-polar-biunification/corpus.kp implements the nonrecursive finite work-list boundary. Its SHA-256 is

Acceptance used the same GHC 9.14.1, arm64 macOS 26.3.1 compiler built from clean Kappa source commit

Its binary SHA-256 is

The exact commands are

kappa check \
  artifacts/ch19-polar-biunification/corpus.kp
kappa test \
  artifacts/ch19-polar-biunification/corpus.kp
kappa run \
  artifacts/ch19-polar-biunification/corpus.kp
kappa audit \
  artifacts/ch19-polar-biunification/corpus.kp

The exact run output is

PASS upper negative-meet
PASS lower positive-join
PASS arrow contravariant
PASS mismatch rejected
PASS occurs rejected
All 5 Chapter 19 corpus cases passed.

Check is silent, test passes one corpus, and audit prints []. The named run covers the upper, lower, arrow, mismatch, and occurs-check cases; hidden assertions exercise a nested arrow mismatch, join-left/meet-right decomposition, rejection of an unsupported variable-to-variable bound, and incompatible lower/upper bounds on one variable. It ends with All 5 Chapter 19 corpus cases passed.. This is not an implementation of MLsub, MLstruct, MLstruct+, or Simple-sub and proves no inference theorem.

Chapter 9: finite-graph semantic subtyping

Reproducibility record for exercise 20.19.

The directory artifacts/ch20-semantic-subtyping/ contains a Kappa implementation of the ${\lambda }_{\mathsf{FG}}$ subtype decision procedure and annotated synthesis examples from chapter 9. Types, clauses, graph obligations, interfaces, and terms are object-language nominal data; Kappa’s own type relation is not used as the semantic-subtyping oracle.

The companion targets the portable kappa-v1 profile and pins a clean Kappa source commit: $$\mathtt{\text{53ce3a88e6ecf3f6729a3e02e75d836d00f301c0}}.$$ The accepted corpus has SHA-256 $$\begin{array}{c}\mathtt{\text{85b031cf3fb30e4e32c3d68936a0ae50}}\\ \mathtt{\text{e0476853c3c466e25189dae9f4513a63}}.\end{array}$$ Its README records the specification and conformance-ledger digests, compiler digest, GHC 9.14.1, arm64 macOS 26.3.1, the finite saturation bound, and the accepted-output summary. From the repository root, run

kappa check \
  artifacts/ch20-semantic-subtyping/corpus.kp
kappa test \
  artifacts/ch20-semantic-subtyping/corpus.kp

The check is silent and the inline harness passes one corpus. The trace is printed by

kappa run \
  artifacts/ch20-semantic-subtyping/corpus.kp

and ends with

All 8 semantic-subtyping corpus cases passed.

The cases exercise the $\mathrm{\Omega }$ distinction between $0\to 1$ and $1\to 1$; arrow variance and overload inclusion; complement and arrow decomposition; products and Boolean subtyping; direct overloaded application at $\mathsf{Nat}\vee \mathsf{Bool}$; binder typecase refinement; mandatory branch scope before empty-branch suppression; binder freshness; the one-interface self-application; and rejection of malformed or unsafe annotations.

The separate audit command prints []. Removing the full-subset $\mathrm{\Omega }$ guard makes the first case fail, while replacing universal arrow-subset decomposition by existential choice makes the first three fail. Bypassing either pre-suppression branch scope or binder freshness makes the typecase case fail. No Kappa compiler defect or conformance-suite change was required. These tree-walking runs check implementation behavior for the displayed finite algorithm and examples. They do not prove DNF correctness, simulation soundness or completeness, checker characterization, preservation, progress, or safety, and they do not claim interpreter–native-backend parity.

Chapter 21: top-free disjoint merge

Reproducibility record for exercise 21.9.

The portable companion is artifacts/ch21-disjoint-merge/corpus.kp. It represents source types, algorithmic disjointness, coercive subtyping, merge formation, contributors, and projection observations as ordinary Kappa data; Kappa’s type relation is not an intersection-subtyping oracle. The accepted corpus SHA-256 is 7b99505d82f52b4ab819c3b84ea90ee2a3d57560265ba9e3a2042e7c2ffb7f5f. It was checked with compiler source commit 53ce3a88e6ecf3f6729a3e02e75d836d00f301c0; the tested local compiler binary has SHA-256 476688a4b6078aaef4e7a23f46383a3879df40d391bca7d6878545197a002d01. Run

kappa check artifacts/ch21-disjoint-merge/corpus.kp
kappa test  artifacts/ch21-disjoint-merge/corpus.kp
kappa run   artifacts/ch21-disjoint-merge/corpus.kp
kappa audit artifacts/ch21-disjoint-merge/corpus.kp

The run prints eight named PASS lines and ends with

All 8 Chapter 21 corpus cases passed.

The audit prints []. The nested-product case replays S-Prod and S-L${}_1$ before selecting the left merge contributor; it prevents syntactic equality from masquerading as subtyping. The last case computes the left and right projection observations $1$ and $2$; it does not merely compare the integer literals. The finite run proves none of semantic-disjointness decision, coercion uniqueness, preservation, coherence, or safety. No Kappa defect or conformance-suite change was required. The distribution case traverses intersections on both sides, and the final success summary is conditional on all eight case booleans.

Chapter 10: difference-constraint certificates and finite inference

Reproducibility record for exercise 22.11.

The directory artifacts/ch22-refinements/ contains a Kappa implementation of the graph construction, certificate replay, and finite qualifier search used in chapter 10. Difference atoms, identified weighted edges, paths, cycles, program steps, and qualifiers are object-language nominal data; Kappa’s own type relation is not used as a refinement oracle.

The companion targets the portable kappa-v1 profile and pins a clean Kappa source commit: $$\mathtt{\text{53ce3a88e6ecf3f6729a3e02e75d836d00f301c0}}.$$ The accepted corpus has SHA-256 $$\begin{array}{c}\mathtt{\text{7a98ca0800fd473a0875e69490ad3dcb}}\\ \mathtt{\text{cdeb4174c0bc86e6ce280179dc27753b}}.\end{array}$$ Its README records the specification and conformance-ledger digests, compiler digest, GHC 9.14.1, arm64 macOS 26.3.1, the input-derived search bound, and the accepted-output summary. From the repository root, run

kappa check \
  artifacts/ch22-refinements/corpus.kp
kappa test \
  artifacts/ch22-refinements/corpus.kp

The check is silent and the inline harness passes one corpus. The trace is printed by

kappa run \
  artifacts/ch22-refinements/corpus.kp

and ends with

All 8 refinement-certificate corpus cases passed.

The cases exercise graph and VC generation for last; nonempty and empty literal preconditions; the missing-input-bound rejection; lastOrZero’s read-bearing branch; negative-cycle search and replay; rejection of missing, nonadjacent, open, and nonnegative certificates; finite qualifier inference for the recursive array loop; and failure of both a missing and a nearby-but-insufficient upper qualifier.

The separate audit command prints []. Weakening the generated lower bound makes the missing-bound case fail. Bypassing edge adjacency, or admitting a zero-weight contradiction cycle, makes the malformed-certificate case fail. Weakening the exact upper qualifier makes finite inference fail. All four mutations make the inline harness exit unsuccessfully. No Kappa compiler defect or conformance-suite change was required. These tree-walking runs check implementation behavior for the displayed graph construction, certificate replay, examples, and finite enumeration. They do not prove certificate soundness or completeness, checker correctness, preservation, progress, array safety, Liquid relative completeness, or proof-carrying-code soundness, and they do not claim interpreter–native-backend parity.

Chapter 11: finite elaboration and cast-machine traces

Reproducibility record for exercise 23.15.

The directory artifacts/ch23-gradual-typing/ contains a finite Kappa implementation of the source syntax, source typing and cast insertion, and a refocused target machine for chapter 11. Gradual types, source and target terms, source positions, blame labels, evaluation frames, machine states, and observations are object-language nominal data; Kappa’s own type relation is not used as a gradual-typing oracle.

The companion targets portable kappa-v1 and pins Kappa source commit 53ce3a88 e6ecf3f6 729a3e02 e75d836d 00f301c0. The accepted corpus has SHA-256 $$\begin{array}{c}\mathtt{\text{a57d16f9a88b0fd601d827f47b8ce303}}\\ \mathtt{\text{73931d67a6d5f1bc498a1023a36b999e}}.\end{array}$$ Its README records the specification, conformance-ledger, and compiler digests, GHC 9.14.1, arm64 macOS 26.3.1, the exact output, three negative mutations, and the evidence boundary; TRANSCRIPT.txt records the accepted and mutated runs. From the repository root, run

kappa check \
  artifacts/ch23-gradual-typing/corpus.kp
kappa test \
  artifacts/ch23-gradual-typing/corpus.kp
kappa run \
  artifacts/ch23-gradual-typing/corpus.kp
kappa audit \
  artifacts/ch23-gradual-typing/corpus.kp

The check is silent, the inline harness passes one corpus, the trace ends with

All 5 gradual-cast corpus cases passed.

and the audit prints []. The cases inspect an elaborated application tree and run elaborated source programs through successful and failing ground projection, both higher-order blame directions, and the precise-blame/less-precise-value counterexample. Mutating label complementation, unequal-tag rejection, or the argument-label slot makes the same inline test fail. No compiler or conformance-suite change was required. These executions are not proofs of safety, blame safety, simulation, either gradual guarantee, or any theorem about Kappa.

Chapter 12: explicit recursion and finite PCF approximants

Reproducibility record for exercise 24.17.

The directory artifacts/ch24-recursion/ contains a Kappa implementation of three deliberately separate executable fragments from chapter 12: eager iso-recursive typing and reduction, contractive regular-tree equality, and a call-by-name PCF stack machine. Their types, terms, work queues, and machine states are object-language nominal data; Kappa’s own type relation is not used as an oracle for the displayed calculi.

The companion targets the portable kappa-v1 profile. Its pinned Kappa source commit is 53ce3a88 e6ecf3f6 729a3e02 e75d836d 00f301c0. The frozen digests are

The README records GHC 9.14.1, arm64 macOS 26.3.1, the regular-equality and PCF budgets, and the accepted-output summary. From the repository root, all four verification commands are

kappa check \
  artifacts/ch24-recursion/corpus.kp
kappa test \
  artifacts/ch24-recursion/corpus.kp
kappa run \
  artifacts/ch24-recursion/corpus.kp
kappa audit \
  artifacts/ch24-recursion/corpus.kp

The check is silent; the inline harness reports one passed corpus; the audit prints []; and the run ends with

All 6 Chapter 24 corpus cases passed.

The cases type and expose a recursive list cell; type and calculate the two-step recursive-type divergence cycle; accept two alpha-variant regular stream descriptions; reject a constructor mismatch and an unguarded binder; evaluate recursive PCF addition to five; and exhaust a finite approximant for fix x : Nat. x.

Three genuine source mutations were applied separately and tested with the same inline oracle.

1. Replacing the unfold (fold v) transition by a stuck result made both iso-recursive cases fail. The mutated source SHA-256 was $$\begin{array}{c}\mathtt{\text{e932af27f9813a7a9b4e28d2447fbff7}}\\ \mathtt{\text{5bb5722ef5cebbbce505ce98a4101101}}.\end{array}$$

2. Replacing visited-pair continuation by rejection made regular-tree equality fail. The mutated source SHA-256 was $$\begin{array}{c}\mathtt{\text{f5bbd587915b4535d80fff7cf62afa2c}}\\ \mathtt{\text{1d1af9ec4f88747f28d6be31c1bfc961}}.\end{array}$$

3. Replacing the PCF fixed-point transition by a stuck result made both PCF cases fail. The mutated source SHA-256 was $$\begin{array}{c}\mathtt{\text{1f8997c21c8285fe30e10825f38bca41}}\\ \mathtt{\text{34b50bc8885a5a99c850bae276cedd9b}}.\end{array}$$

In each run kappa test exited 1 with a stdout mismatch. Restoring the accepted source digest restored all four gates.

No Kappa compiler defect or conformance-suite change was required. Fuel exhaustion is not treated as proof of divergence. These tree-walking runs check implementation behavior for the displayed examples; they do not prove safety, regular-equality decision, domain equations, adequacy, divergence, or step-indexed compatibility, and they do not claim interpreter–native-backend parity.