CRCD/EI: Integrating Functional Computer-Aided Reasoning into the ComputerScience Curriculum

CRCD/EI：将功能计算机辅助推理融入计算机科学课程

• 批准号: 0844078
• 负责人: Panagiotis Manolios
• 金额: $ 21.03万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-03-13 至 2009-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0844078&HistoricalAwards=false
• 关键词: CRCD; EI; Integrating; Functional; Computer

0417413GA Tech Research Corp - GA Institute of TechnologyManolios"CRCD/EI: Integrating Functional Computer-Aided Reasoning into the Computer Science Curriculum"This project involves the development of tools, courses, modules, and self-paced online materials that integrate computer-aided reasoning into the Computer Science (CS) curriculum. This project is novel in undergraduate CS education. The use of a state-of-the-art theorem proving technology (ACL2) permits students to get instant, reliable feedback, thereby enabling effective learning and self-paced study. ACL2 is a tool consisting of a functional programming language, a logic, and a theorem-prover, that has been used to prove some of the largest and most complicated theorems ever proved about commercially designed systems. The project involves at least two research challenges: taking a necessarily complex, state-of-the-art, theorem proving system and teaching undergraduates how to be effective users in a portion of a semester, and developing effective courses in other areas, such as hardware design and object oriented programming, that are based on the use of computer-aided reasoning. A sequence of mathematical concepts and mechanical tools, with well-designed graphical user-interfaces, allow students to gradually and seamlessly master ACL2. Integration of computer-aided reasoning into current curricula is accomplished through two courses that make essential use of these tools, thereby giving students a deeper and more complete understanding of the material. The courses cover the following topics: computer organization and design, object-oriented programming using the JVM, theorem proving, and formal methods. One of the undergraduate courses focuses on computer organization and design and the other on the Java Virtual Machine (JVM). In these two courses, computer-aided reasoning is used to give students a deeper understanding of the material. They are required to think about the properties systems and components under consideration should enjoy and how to prove that these properties do in fact hold.

0417413 GA Tech Research Corp - GA Institute of TechnologyManolios“CRCD/EI：Integrating Functional Computer-Aided Reasoning into the Computer Science Curriculum“该项目涉及开发工具、课程、模块和自定进度的在线材料，将计算机辅助推理集成到计算机科学（CS）课程中。该项目在计算机科学本科教育中具有一定的创新性。使用最先进的定理证明技术（ACL 2）允许学生获得即时，可靠的反馈，从而实现有效的学习和自定进度的学习。ACL 2是一个由函数式编程语言、逻辑和定理证明器组成的工具，已被用于证明商业设计系统中一些最大和最复杂的定理。该项目涉及至少两个研究挑战：采取必要的复杂，国家的最先进的，定理证明系统和教学本科生如何成为有效的用户在一个学期的一部分，并开发有效的课程在其他领域，如硬件设计和面向对象的编程，是基于使用计算机辅助推理。一系列数学概念和机械工具，以及精心设计的图形用户界面，使学生能够逐步无缝地掌握ACL 2。将计算机辅助推理纳入目前的课程是通过两门课程来完成的，这两门课程基本上使用了这些工具，从而使学生对材料有了更深入、更全面的理解。课程涵盖以下主题：计算机组织和设计，使用JVM的面向对象编程，定理证明和形式化方法。其中一门本科课程侧重于计算机组织和设计，另一门侧重于Java虚拟机（JVM）。在这两门课程中，计算机辅助推理被用来让学生对材料有更深入的理解。他们需要考虑所考虑的系统和组件应该享有的属性，以及如何证明这些属性确实存在。