[isabelle] 2 new AFP entries



There are two new entries available in the AFP:

Source Coding Theorem
by Quentin Hibon and Lawrence Paulson

  This document contains a proof of the necessary condition on the code
  rate of a source code, namely that this code rate is bounded by the
  entropy of the source. This represents one half of Shannon's source
  coding theorem, which is itself an equivalence.

https://www.isa-afp.org/entries/Source_Coding_Theorem.shtml


A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
by Zhe Hou, David Sanan, Alwen Tiu, and Yang Liu

  We formalise the SPARCv8 instruction set architecture (ISA) which is
  used in processors such as LEON3. Our formalisation can be specialised
  to any SPARCv8 CPU, here we use LEON3 as a running example. Our model
  covers the operational semantics for all the instructions in the
  integer unit of the SPARCv8 architecture and it supports Isabelle code
  export, which effectively turns the Isabelle model into a SPARCv8 CPU
  simulator. We prove the language-based non-interference property for
  the LEON3 processor.  Our model is based on deterministic monad, which
  is a modified version of the non-deterministic monad from NICTA/l4v.

https://www.isa-afp.org/entries/SPARCv8.shtml


Enjoy!
Gerwin







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.