Scholarlink

This paper evaluates the educational impact of proof assistants in computer science education through a feasibility study. We developed a methodology using interactive theorem proving to measure students’ understanding of computer science concepts, focusing on instruction set architectures within the Coq proof assistant. Through pre/post assessments and structured learning tasks, we evaluated both our testing framework and students’ learning outcomes, providing insights for classroom integration of proof assistants.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Feasibility Study on Leveraging Proof Assistants for Educational Purposes

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Fernand Dubler,
  • Ulrich Ultes-Nitsche,
  • Dorian Guyot

摘要

This paper evaluates the educational impact of proof assistants in computer science education through a feasibility study. We developed a methodology using interactive theorem proving to measure students’ understanding of computer science concepts, focusing on instruction set architectures within the Coq proof assistant. Through pre/post assessments and structured learning tasks, we evaluated both our testing framework and students’ learning outcomes, providing insights for classroom integration of proof assistants.