Reasoning about DrScheme Programs in ACL2
Trends in Functional Programming
2010
Abstract
Beginning programmers need to learn more than the syntax of programming languages. They also need to learn how to reason about the programs they write. Thus we believe that beginners will benefit from tools that help them understand their programs, just as they already benefit from IDEs that help them to build and debug their programs. This paper describes a project aimed at automating some of the techniques required to reason about programs in Beginning Student Language (BSL), the first language in DrScheme’s How to Design Programs curriculum [4]. The automation is based on the theorem prover ACL2.
Topics:Intelligent Tutoring Systems
BibTeX
@inproceedings{wiederrecht-tfp-2010,
title = {Reasoning about DrScheme Programs in ACL2},
author = {Wiederrecht, Melissa and MacLellan, Christopher J. and Gamboa, Ruben},
booktitle = {Trends in Functional Programming},
year = {2010},
doi = {10.1007/978-3-642-22941-1},
}