Fix Your Types

Sol Swords
(Centaur Technology, Inc.)
Jared Davis
(Centaur Technology, Inc.)

When using existing ACL2 datatype frameworks, many theorems require type hypotheses. These hypotheses slow down the theorem prover, are tedious to write, and are easy to forget. We describe a principled approach to types that provides strong type safety and execution efficiency while avoiding type hypotheses, and we present a library that automates this approach. Using this approach, types help you catch programming errors and then get out of the way of theorem proving.

In Matt Kaufmann and David L. Rager: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2015), Austin, Texas, USA, 1-2 October 2015, Electronic Proceedings in Theoretical Computer Science 192, pp. 3–16.
Published: 18th September 2015.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: