Attaching Efficient Executability to Partial Functions in ACL2

S. Ray

In M. Kaufmann and J S. Moore, editors, 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, November 2004

Abstract

We describe a macro defpun-exec to attach executable bodies to partial functions in ACL2. The macro makes use of two new features mbe and defexec, introduced in ACL2 from version 2.8, that allow a clean separation of execution efficiency from logical elegance.

Relevant files

Paper (ps, pdf)
Slides for ACL2 2004 (ps, pdf)
Supporting materials: See the directory books/workshops/2004/ray/support/ in the current ACL2 distribution. (Note: You need the workshops tarball. See the instructions for installing ACL2 in the ACL2 homepage.)

BibTex

@Inproceedings{ray-attaching,
  title     = "{Attaching Efficient Executability to Partial Functions in ACL2}",
  author    = "S. Ray",
  editor    = "M. Kaufmann and J S. Moore",
  booktitle = "{$5$th International Workshop on the ACL2 Theorem Prover and Its Applications
                (ACL2 2004)}",
  month     = nov,
  address   = "{Austin, TX}",
  year      = "2004"
}