SPLASH-E '26: "Curated Semantic Mutants: ..."
Curated Semantic Mutants: Multi-purpose Artifacts for Grading and Hinting Student Test Suites
Rebecca Williams Earle and Jonathan Bell
(Northeastern University, USA)
Mutation testing can evaluate a student's test suite, but traditional mutation tools do not encode which generated faults a course rubric should weight or what feedback should be delivered to students that do not detect a mutant. We report a human-LLM workflow that pairs each curated semantic mutant with an instructor-approved seed phrase for an on-demand LLM expansion. Deployed across two semesters of CS 3100, an introductory software-engineering course (N=1,893 submissions), the workflow provided automated per-submission feedback about undetected curated faults. In a deployment with on-demand hint expansions, 46% of students requested at least one, at roughly three cents each. At the failing submission--unit-pair level, requested expansions were associated with improvement on the next submission at 1.62 times the rate of pairs with no request, though because requests were self-selected this is not a causal estimate. A same-code comparison also shows that the curated semantic-mutant set contains a fraction of the mutants a traditional mutation engine produces. We do not compare this LLM-assisted approach with an instructor curating and writing mutants and hints by hand; whether it is cheaper or better remains an open question.
Article Search
Article: splashws26splashemain-p58-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842688
SPLASH-E '26: "More Pie for the Little Typer ..."
More Pie for the Little Typer
Zhang Qixiang, Ding Feng, Li Daoxin, and Martin Henz
(National University of Singapore, Singapore)
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 written as flat terms with no goal-directed workflow. We reimplement Pie from scratch in TypeScript and add three extensions that make it more accessible and extensible for learners. Tactics build proofs by goal-directed steps yet extract an ordinary, reusable term; named holes extend Pie’s single unnamed placeholder so that several open goals can each report their own type and context; and user-defined inductive types come with automatically generated eliminators. An interactive proof canvas renders these tactic proofs and lets a learner build them by direct manipulation. On this core we add PieLoT, an AI assistant: a self-supervised fine-tuned tactic predictor and a Socratic hint service that explains rather than solves. We report the design, worked examples, and a preliminary evaluation of how the system overcomes the limitations of Pie’s original implementation. The result is a browser-based, extensible, AI-guided proof environment built on a minimal, transparent core.
Article Search
Article: splashws26splashemain-p25-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842687
SPLASH-E '26: "Curated Semantic Mutants: ..."
Curated Semantic Mutants: Multi-purpose Artifacts for Grading and Hinting Student Test Suites
Rebecca Williams Earle and Jonathan Bell
(Northeastern University, USA)
Mutation testing can evaluate a student's test suite, but traditional mutation tools do not encode which generated faults a course rubric should weight or what feedback should be delivered to students that do not detect a mutant. We report a human-LLM workflow that pairs each curated semantic mutant with an instructor-approved seed phrase for an on-demand LLM expansion. Deployed across two semesters of CS 3100, an introductory software-engineering course (N=1,893 submissions), the workflow provided automated per-submission feedback about undetected curated faults. In a deployment with on-demand hint expansions, 46% of students requested at least one, at roughly three cents each. At the failing submission--unit-pair level, requested expansions were associated with improvement on the next submission at 1.62 times the rate of pairs with no request, though because requests were self-selected this is not a causal estimate. A same-code comparison also shows that the curated semantic-mutant set contains a fraction of the mutants a traditional mutation engine produces. We do not compare this LLM-assisted approach with an instructor curating and writing mutants and hints by hand; whether it is cheaper or better remains an open question.
Article Search
Article: splashws26splashemain-p58-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842688
SPLASH-E '26: "More Pie for the Little Typer ..."
More Pie for the Little Typer
Zhang Qixiang, Ding Feng, Li Daoxin, and Martin Henz
(National University of Singapore, Singapore)
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 written as flat terms with no goal-directed workflow. We reimplement Pie from scratch in TypeScript and add three extensions that make it more accessible and extensible for learners. Tactics build proofs by goal-directed steps yet extract an ordinary, reusable term; named holes extend Pie’s single unnamed placeholder so that several open goals can each report their own type and context; and user-defined inductive types come with automatically generated eliminators. An interactive proof canvas renders these tactic proofs and lets a learner build them by direct manipulation. On this core we add PieLoT, an AI assistant: a self-supervised fine-tuned tactic predictor and a Socratic hint service that explains rather than solves. We report the design, worked examples, and a preliminary evaluation of how the system overcomes the limitations of Pie’s original implementation. The result is a browser-based, extensible, AI-guided proof environment built on a minimal, transparent core.
Article Search
Article: splashws26splashemain-p25-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842687
SPLASH-E '26: "Visualizing Turing Machines ..."
Visualizing Turing Machines and Multitape Turing Machines
David Anthony K. Fields, Sophia G. Turano, Andrés M. Garced, and Marco T. Morazán
(Seton Hall University, USA)
An important computational model studied in Formal Languages and Automata Theory is the Turing machine and its extensions, including the multitape Turing machine. Designing such machines is challenging because they operate at a low level of abstraction, making it difficult to understand why words in an unrestricted language are accepted or rejected or why a function computes the correct value. Furthermore, many students may struggle to understand how to design such machines using nondeterminism or mutation. To address these problems, this article presents two new dynamic visualization tools for machine execution: one for Turing machines and one for multitape Turing machines, both of which are integrated into the domain-specific language FSM. These tools visually trace all computations that may be performed in a stepwise manner and support students in validating and verifying their designs. In addition to tracing an arbitrary machine designed by the programmer, the tools display when state invariant predicates hold or fail to hold. The results of a formative empirical study exploring student perceptions suggest that the tools are well received and help students understand, debug, validate, and verify their designs. In addition, the results suggest that students believe the tools help them understand nondeterminism.
Article Search
Article: splashws26splashemain-p81-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842689
SPLASH-E '26: "Visualizing Turing Machines ..."
Visualizing Turing Machines and Multitape Turing Machines
David Anthony K. Fields, Sophia G. Turano, Andrés M. Garced, and Marco T. Morazán
(Seton Hall University, USA)
An important computational model studied in Formal Languages and Automata Theory is the Turing machine and its extensions, including the multitape Turing machine. Designing such machines is challenging because they operate at a low level of abstraction, making it difficult to understand why words in an unrestricted language are accepted or rejected or why a function computes the correct value. Furthermore, many students may struggle to understand how to design such machines using nondeterminism or mutation. To address these problems, this article presents two new dynamic visualization tools for machine execution: one for Turing machines and one for multitape Turing machines, both of which are integrated into the domain-specific language FSM. These tools visually trace all computations that may be performed in a stepwise manner and support students in validating and verifying their designs. In addition to tracing an arbitrary machine designed by the programmer, the tools display when state invariant predicates hold or fail to hold. The results of a formative empirical study exploring student perceptions suggest that the tools are well received and help students understand, debug, validate, and verify their designs. In addition, the results suggest that students believe the tools help them understand nondeterminism.
Article Search
Article: splashws26splashemain-p81-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842689
SPLASH-E '26: "More Pie for the Little Typer ..."
More Pie for the Little Typer
Zhang Qixiang, Ding Feng, Li Daoxin, and Martin Henz
(National University of Singapore, Singapore)
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 written as flat terms with no goal-directed workflow. We reimplement Pie from scratch in TypeScript and add three extensions that make it more accessible and extensible for learners. Tactics build proofs by goal-directed steps yet extract an ordinary, reusable term; named holes extend Pie’s single unnamed placeholder so that several open goals can each report their own type and context; and user-defined inductive types come with automatically generated eliminators. An interactive proof canvas renders these tactic proofs and lets a learner build them by direct manipulation. On this core we add PieLoT, an AI assistant: a self-supervised fine-tuned tactic predictor and a Socratic hint service that explains rather than solves. We report the design, worked examples, and a preliminary evaluation of how the system overcomes the limitations of Pie’s original implementation. The result is a browser-based, extensible, AI-guided proof environment built on a minimal, transparent core.
Article Search
Article: splashws26splashemain-p25-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842687
SPLASH-E '26: "Introducing Hoare Logic in ..."
Introducing Hoare Logic in the Undergraduate CS Curriculum: In Memoriam of Tony Hoare
Marco T. Morazán
(Seton Hall University, USA)
Hoare Logic is one of the most significant intellectual achievements in Computer Science, providing a foundation for reasoning about imperative programs. This intellectual milestone was developed leaning on historical developments in the field, has profoundly shaped program development, and continues to influence modern mechanized verification. Surprisingly, however, Hoare Logic receives only limited attention in most undergraduate computer science curricula. Often, it is relegated to an advanced course in Programming Languages or in Program Verification. This is unfortunate, because Hoare Logic and formal methods can be directly used to design programs as demonstrated by Hoare, Dijkstra, Gries, and others. This article proposes an approach to address this curricular gap. Rather than relegating Hoare Logic to advanced electives, it can be introduced throughout the undergraduate curriculum. The broader goal is to promote a cultural shift in computer science toward greater acceptance of formal methods.
Article Search
Article: splashws26splashemain-p22-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842686
SPLASH-E '26: "Visualizing Turing Machines ..."
Visualizing Turing Machines and Multitape Turing Machines
David Anthony K. Fields, Sophia G. Turano, Andrés M. Garced, and Marco T. Morazán
(Seton Hall University, USA)
An important computational model studied in Formal Languages and Automata Theory is the Turing machine and its extensions, including the multitape Turing machine. Designing such machines is challenging because they operate at a low level of abstraction, making it difficult to understand why words in an unrestricted language are accepted or rejected or why a function computes the correct value. Furthermore, many students may struggle to understand how to design such machines using nondeterminism or mutation. To address these problems, this article presents two new dynamic visualization tools for machine execution: one for Turing machines and one for multitape Turing machines, both of which are integrated into the domain-specific language FSM. These tools visually trace all computations that may be performed in a stepwise manner and support students in validating and verifying their designs. In addition to tracing an arbitrary machine designed by the programmer, the tools display when state invariant predicates hold or fail to hold. The results of a formative empirical study exploring student perceptions suggest that the tools are well received and help students understand, debug, validate, and verify their designs. In addition, the results suggest that students believe the tools help them understand nondeterminism.
Article Search
Article: splashws26splashemain-p81-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842689
SPLASH-E '26: "More Pie for the Little Typer ..."
More Pie for the Little Typer
Zhang Qixiang, Ding Feng, Li Daoxin, and Martin Henz
(National University of Singapore, Singapore)
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 written as flat terms with no goal-directed workflow. We reimplement Pie from scratch in TypeScript and add three extensions that make it more accessible and extensible for learners. Tactics build proofs by goal-directed steps yet extract an ordinary, reusable term; named holes extend Pie’s single unnamed placeholder so that several open goals can each report their own type and context; and user-defined inductive types come with automatically generated eliminators. An interactive proof canvas renders these tactic proofs and lets a learner build them by direct manipulation. On this core we add PieLoT, an AI assistant: a self-supervised fine-tuned tactic predictor and a Socratic hint service that explains rather than solves. We report the design, worked examples, and a preliminary evaluation of how the system overcomes the limitations of Pie’s original implementation. The result is a browser-based, extensible, AI-guided proof environment built on a minimal, transparent core.
Article Search
Article: splashws26splashemain-p25-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842687
SPLASH-E '26: "Visualizing Turing Machines ..."
Visualizing Turing Machines and Multitape Turing Machines
David Anthony K. Fields, Sophia G. Turano, Andrés M. Garced, and Marco T. Morazán
(Seton Hall University, USA)
An important computational model studied in Formal Languages and Automata Theory is the Turing machine and its extensions, including the multitape Turing machine. Designing such machines is challenging because they operate at a low level of abstraction, making it difficult to understand why words in an unrestricted language are accepted or rejected or why a function computes the correct value. Furthermore, many students may struggle to understand how to design such machines using nondeterminism or mutation. To address these problems, this article presents two new dynamic visualization tools for machine execution: one for Turing machines and one for multitape Turing machines, both of which are integrated into the domain-specific language FSM. These tools visually trace all computations that may be performed in a stepwise manner and support students in validating and verifying their designs. In addition to tracing an arbitrary machine designed by the programmer, the tools display when state invariant predicates hold or fail to hold. The results of a formative empirical study exploring student perceptions suggest that the tools are well received and help students understand, debug, validate, and verify their designs. In addition, the results suggest that students believe the tools help them understand nondeterminism.
Article Search
Article: splashws26splashemain-p81-p (type: Full Paper (11 pages + appendices + references)) doi:10.1145/3841644.3842689