Institutul de Matematică şi Informatică "Vladimir Andrunachievici"
Universitatea de Stat din MoldovaRO EN
Visualizing Type-Checking Proofs: An Educational Web-Based System for an Extended Simply Typed Lambda Calculus
Authors: Ján Perháč and Vladyslav Futrak
Keywords: Educational tool, Simply typed lambda calculus, Type theory, Type checking, Visualizing proofs.
– 0.47 Mb
Keywords: Educational tool, Simply typed lambda calculus, Type theory, Type checking, Visualizing proofs.
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 connects theory and practical learning in type theory education.Department of Computers and Informatics
Faculty of Electrical Engineering and Informatics
Technical University of Kosice
Letna 9, 042 00 Kosice, Slovak Republic
ORCID: https://orcid.org/0000-0001-6347-2409
ORCID: https://orcid.org/0009-0004-4023-9507
E-mail: ,
Faculty of Electrical Engineering and Informatics
Technical University of Kosice
Letna 9, 042 00 Kosice, Slovak Republic
ORCID: https://orcid.org/0000-0001-6347-2409
ORCID: https://orcid.org/0009-0004-4023-9507
E-mail: ,
DOI
https://doi.org/10.56415/csjm.v33.20Fulltext
– 0.47 Mb
Contents
- The 3X2A Strategy for Societal Adaptation in the GenAI Era: A Framework for Human-AI Synergy
- Effective diagnosis of brain tumor classification by using novel DCNN
- Improving Anomaly Detection in the HDFS Dataset with Novel Machine Learning Models and Techniques
- Addressing the limitations related to thresholds in scoring-based decision support tools through graphical visualisation
- Enhanced Botnet Detection and Neutralization through Machine Learning: A Synergistic Analysis of Host Activity, Network Patterns with Explainable Insights
- Optimal size of data packets in computer networks
- Visualizing Type-Checking Proofs: An Educational Web-Based System for an Extended Simply Typed Lambda Calculus
