L3 Instruction Set Models for Isabelle/HOL

L3 is capable of exporting specifications to Isabelle/HOL. The following files are needed when importing L3 models into Isabelle/HOL.

• [2017-10-19] L3.ML (Isabelle 2017)
• [2017-09-05] L3.ML (Isabelle 2016-1)
• [2017-09-05] L3.ML (Isabelle 2016)
• [2017-09-05] L3.ML (Isabelle 2015)

• [2017-09-05] L3_Lib.thy (Isabelle 2016-1 or 2017)
• [2017-09-05] L3_Lib.thy (Isabelle 2015 or 2016)

For convenience, the following Isabelle/HOL theories are readily available.

• [2017-09-27] ARM.thy (covers ARMv4 to ARMv7)
• [2017-09-27] ARM_Monadic.thy (state monad version of ARM.thy)
• [2017-09-27] ARMv8.thy
• [2017-10-02] CHERI.thy
• [2017-10-02] CHERI_Monadic.thy (state monad version of CHERI.thy)
• [2017-09-27] MIPS.thy
• [2017-09-27] RISCV.thy (from Prashanth Mundkur at SRI International)
• [2017-09-27] X64.thy