Kami: a platform for high-level parametric hardware specification and its modular verification

<jats:p>It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reasoning fo...

Full description

Bibliographic Details
Main Authors: Choi, Joonwon, Vijayaraghavan, Muralidaran, Sherman, Benjamin, Chlipala, Adam, Arvind
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory
Format: Article
Language:English
Published: Association for Computing Machinery (ACM) 2021
Online Access:https://hdl.handle.net/1721.1/134865