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


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"
}