论文标题
教功能性程序员逻辑和元数据
Teaching Functional Programmers Logic and Metatheory
论文作者
论文摘要
我们为在功能编程方面有一定经验的学生提供了一种新颖的方法来教授逻辑和逻辑元素。我们将逻辑中的概念定义为一系列功能程序，用证明助手isabelle/hol的语言定义。这使我们能够制作教科书中通常不清楚的概念，可以通过执行定义来实验定义，并详细证明元态定理。我们已经调查了学生对我们的教学方法的看法，以确定其有用性，并发现学生认为我们的形式化有助于他们了解逻辑上的概念，并且他们将其作为学习工具进行了实验。但是，这种方法还不足以使学生对设计和实施自己的正式系统的能力充满信心。需要进一步的研究来确认和概括我们的调查结果，但我们的最初结果似乎很有希望。
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof assistant Isabelle/HOL. This allows us to make notions which are often unclear in textbooks precise, to experiment with definitions by executing them, and to prove metatheoretical theorems in full detail. We have surveyed student perceptions of our teaching approach to determine its usefulness and found that students felt that our formalizations helped them understand concepts in logic, and that they experimented with them as a learning tool. However, the approach was not enough to make students feel confident in their abilities to design and implement their own formal systems. Further studies are needed to confirm and generalize the results of our survey, but our initial results seem promising.
