The objective of the "Dracula" project is to provide a programming environment for the ACL2 language and theorem prover. ACL2, short for A Computational Logic for Applicative Common Lisp, is a programming language and theorem prover. DrRacket is a graphical programming environment for Racket, Scheme, ACL2, and other programming languages. This page provides instructions for downloading the software, working in Racket's ACL2 language, writing interactive graphical programs, and for reporting bugs.

Keep reading below for installation instructions, and check out the links on the left for tutorials, examples, and bug report instructions.

Dracula has been used to teach a first-year undergraduate logic course at Northeastern University. A report on this course was presented at the ACL2 Workshop in 2007, and can be found here.


  1. Installation
  2. Running Dracula
  3. Uninstalling
  4. Acknowledgements



Installing Dracula:

Running Dracula




Thanks to Rex Page for the inspiration for this project, Dale Vaillancourt for the initial implementation, and Matthias Felleisen for his constant support. Thanks to Zoe Zhang, Carter Schonwald, and Ken McGrady for their contributions to Dracula. Thanks to J Moore, Matt Kaufmann, Pete Manolios, Ruben Gamboa, and the rest of the ACL2 community for their support and constructive suggestions.