Dependent Type Checker

In a dependently typed language, types can mention values, so type checking is not just matching annotations against syntax. A $\Pi$ type says a function's result type can depend on its input, while a $\Sigma$ type packages a witness together with data whose type depends on that witness. That forces the checker to reduce terms and compare programs by meaning rather than surface form.

The task centers on a Rust type checker for a Martin-Löf-style core language with universes, dependent function types $\Pi$, dependent pair types $\Sigma$, $\eta$-conversion, and inductive families. That combines normalization-heavy semantics with implementation concerns such as representation, caching, and throughput on generated workloads.

Programs are presented as S-expressions, and the checker reports success or failure via exit code only.

• Parse and check a nontrivial dependently typed core language.
• Reject invalid programs reliably enough to clear the correctness gate.
• Then make the implementation fast enough to beat the reference on throughput.

The verifier enforces an accept/reject correctness gate first. Once that gate passes, it benchmarks paired throughput on three hidden workloads and takes the geometric mean of those per-workload speedups.

The task runs in a Modal container with 8 CPUs, 32 GB RAM, and no internet access. The container image is deliberately sparse: just the scaffold workspace, example programs, and the timer daemon, with no external crates or large helper libraries to lean on. The entire implementation must come from the Rust standard library plus reasoning from the supplied task materials.