Fix Your Types

September 21, 2015 · The Ethereal · 🏛 International Workshop on the ACL2 Theorem Prover and Its Applications

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Sol Swords, Jared Davis arXiv ID 1509.06079 Category cs.LO: Logic in CS Cross-listed cs.PL Citations 9 Venue International Workshop on the ACL2 Theorem Prover and Its Applications Last Checked 6 months ago
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.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS