Visualizing Type-Checking Proofs: an Educational Web-Based System for an Extended Simply Typed Lambda Calculus

Understanding simply typed lambda calculus is essential for learning type systems and formal semantics, but its abstract concepts are often challenging. We developed a web-based tool that visualizes type checking through interactive proof trees, providing real-time feedback, highlighting typing contexts, and allowing step-by-step exploration of derivations. The language supports tuples, variants, lists, records, conditionals, recursion, and export of derivations in LATEX or image formats. User testing with university students showed improved comprehension and motivation. By making reasoning visual and interactive, the system connects theory and practical learning in type theory education.