Fix Your Types

TL;DR

This paper introduces a principled approach to types in ACL2 that enhances type safety and execution efficiency, eliminates the need for type hypotheses, and automates the process through a dedicated library.

Contribution

It presents a novel type system for ACL2 that improves proof performance and safety without requiring explicit type hypotheses, supported by an automation library.

Findings

Reduces theorem proving time by eliminating type hypotheses

Enhances type safety and error detection in ACL2

Automates type management with a dedicated library

Abstract

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.