Fast machine words in Isabelle/HOL

DOI10.1007/978-3-319-94821-8_23MaRDI QIDQ1791180zbMATH OpenOpenAlexFDO

Authors Andreas Lochbihler

Publication date 4 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94821-8_23

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A verified compiler from Isabelle/HOL to CakeML
• Data refinement in Isabelle/HOL
• The Isabelle collections framework
• Lyndon words formalized in Isabelle/HOL
• An Interpretation of Isabelle/HOL in HOL Light

Cited in

(4)

• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Primitive Floats in Coq
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Lyndon words formalized in Isabelle/HOL

Describes a project that uses

Uses Software

• Isabelle/HOL
• Coq
• Maude
• CeTA
• CakeML
• HOL-TestGen
• Fiat
• GRAT
• JavaFAN
• PVS
• Isabelle
• CertiCoq

This page was built for publication: Fast machine words in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1791180)