More Pie for the Little Typer: Accessible, Extensible, and AI-Guided Proof Education
Pie, the dependently typed teaching language of The Little Typer, is pedagogically near-ideal: just enough to teach dependent types and proof, and no black boxes. Yet its original implementation imposes barriers of its own: a heavyweight local setup, no interactive feedback, a fixed set of built-in types, and proofs wr...
Qi-Xiang Zhang, Feng Ding, Dao-Xin Li et al.
· 0 citations