Formalising MiniSail in Isabelle
Sail is a language for specifying instruction-set architectures and has been used to model various production and research architectures. Designed to be engineer friendly, Sail is an imperative first-order language with a light-weight dependent type system. The latest redesign of the Sail type system has been done in conjunction with the development of a core calculus, MiniSail, along with paper proofs of type safety.
This talk presents work to mechanise MiniSail in Isabelle, making use of the Nominal2 Isabelle library to address binding structures and alpha-equivalence. The mechanisation includes the definition of the MiniSail type system and operational semantics, as well as proofs of preservation and progress. We outline the experience of using Nominal2 to do this mechanisation and the follow-on work to mechanise a Sail type-validator and a Sail to MiniSail converter.