Visualizing Type-Checking Proofs: An Educational Web-Based System for an Extended Simply Typed Lambda Calculus
Abstract
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
Fields of Study & Subjects
Logic
programming
and type systems
Mathematics
Computing
and Information Processing
Software Engineering and Design Patterns
Publication details
- Journal / source
- Computer Science Journal of Moldova
- Volume
- 33
- Issue
- 3
- Pages
- 430–455
- Publication date
- 1 January 2026
- Language
- EN