Electronic Proceedings in Theoretical Computer Science (Jun 2014)

Polymorphic Types in ACL2

  • Benjamin Selfridge,
  • Eric Smith

DOI
https://doi.org/10.4204/EPTCS.152.4
Journal volume & issue
Vol. 152, no. Proc. ACL2 2014
pp. 49 – 59

Abstract

Read online

This paper describes a tool suite for the ACL2 programming language which incorporates certain ideas from the Hindley-Milner paradigm of functional programming (as exemplified in popular languages like ML and Haskell), including a "typed" style of programming with the ability to define polymorphic types. These ideas are introduced via macros into the language of ACL2, taking advantage of ACL2's guard-checking mechanism to perform type checking on both function definitions and theorems. Finally, we discuss how these macros were used to implement features of Specware, a software specification and implementation system.