1 Dracula

Dracula is a DrScheme language level that provides an interface to the ACL2 theorem prover and emulates its executable component. This section is still under construction; for a tutorial, sample code, and instructions to install, upgrade, or remove Dracula, see the Dracula webpage.