Formalization of fixed-point arithmetic in HOL
From MaRDI portal
Recommendations
Cites work
- Constructing the real numbers in HOL
- Correct Hardware Design and Verification Methods
- scientific article; zbMATH DE number 1670746 (Why is no real title available?)
- scientific article; zbMATH DE number 1670752 (Why is no real title available?)
- scientific article; zbMATH DE number 1979556 (Why is no real title available?)
- scientific article; zbMATH DE number 1485863 (Why is no real title available?)
- scientific article; zbMATH DE number 1852167 (Why is no real title available?)
- scientific article; zbMATH DE number 1863384 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
Cited in
(10)- Functional verification of high performance adders in \textsc{Coq}
- On the formalization of gamma function in HOL
- Formalization of linear space theory in the higher-order logic proving system
- Error analysis of digital filters using HOL theorem proving
- A parameterized floating-point formalizaton in HOL Light
- On the Formalization of Z-Transform in HOL
- scientific article; zbMATH DE number 2086952 (Why is no real title available?)
- Theorem Proving in Higher Order Logics
- Formal Methods in Computer-Aided Design
- Tight Error Analysis in Fixed-Point Arithmetic
This page was built for publication: Formalization of fixed-point arithmetic in HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q816219)
