Fix Your Types

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.

In Proceedings ACL2 2015, arXiv:1509.05526

References in corpus (6)

• Bit-Blasting ACL2 Theorems
• Data Definitions in the ACL2 Sedan
• Abstract Stobjs and Their Application to ISA Modeling
• A formalisation of XMAS
• Development of a Translator from LLVM to ACL2
• Polymorphic Types in ACL2

Cited by in corpus (6)

• Second-Order Functions and Theorems in ACL2
• Term-Level Reasoning in Support of Bit-blasting
• Syntheto: A Surface Language for APT and ACL2
• On Automating Proofs of Multiplier Adder Trees using the RTL Books
• A Formalization of the Yul Language and Some Verified Yul Code Transformations
• Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32