Polymorphic Types in ACL2

TL;DR

This paper introduces a macro-based polymorphic type system for ACL2, inspired by Hindley-Milner, enabling typed programming and type checking within ACL2, and demonstrates its application in Specware.

Contribution

It presents a novel macro-based approach to incorporate polymorphic types and type checking into ACL2, inspired by functional programming paradigms.

Findings

Successfully integrated polymorphic types into ACL2

Enabled type checking for functions and theorems

Applied macros to implement features of Specware

Abstract

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.