DrACuLa - the programming environment for the ACL2 theorem prover in DrScheme: ACL2 in DrScheme. Teaching undergraduates to develop software in a formal framework such as ACL2 poses two immediate challenges. First, students typically do not know applicative programming and are often unfamiliar with ACL2’s syntax. Second, for motivational reasons, students prefer to work on projects that involve designing interactive, graphical applications. In this paper, we present DRACULA, a pedagogic programming environment that partially solves these problems. The environment adds a subset of Applicative Common Lisp to DRSCHEME, an integrated programming environment for Scheme. DRACULA thus inherits DRSCHEME’s pedagogic capabilities, especially its treatment of syntax and run-time errors. Further, DRACULA also comes with a library for programming interactive, graphical games. The library interface forces students to think of a graphical user interface in terms of state-transition functions, enabling them later to prove theorems about their games in ACL2. DRACULA provides a graphical front-end to the ACL2 theorem prover for this purpose. In short, DRACULA allows the formulation of student projects that represent an important intermediate point between data structure exercises in theorem proving and industrial applications
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Caleb Eggensperger: Proof Pad: A New Development Environment for ACL2 (2013) arXiv
- Nipkow, Tobias: Teaching semantics with a proof assistant: no more LSD trip proofs (2012)
- Dillinger, Peter C.; Manolios, Panagiotis; Vroon, Daron; Moore, J Strother: ACL2s: “the ACL2 sedan” (2007)