Abstract
MiniSail is a kernel language for Sail, an instruction set
architecture (ISA) specification language. Sail is an imperative
language with a light-weight dependent type system similar to
refinement type systems. From an ISA specification, the Sail compiler
can generate theorem prover code and C (or OCaml) to give an
executable emulator for an architecture. The idea behind MiniSail is
to capture the key and novel features of Sail in terms of their
syntax, typing rules and operational semantics, and to confirm that
they work together by proving progress and preservation lemmas. We use
the Nominal2 library to handle binding.
License
Topics
Session MiniSail
- Nominal-Utils
- Syntax
- IVSubst
- BTVSubst
- Wellformed
- RCLogic
- SyntaxL
- WellformedL
- Typing
- Operational
- SubstMethods
- RCLogicL
- TypingL
- ContextSubtypingL
- IVSubstTypingL
- BTVSubstTypingL
- Safety
- MiniSail
Auto-related entries
- Operational Semantics formally proven in HOL-CSP
- A Formal Development of a Polychronous Polytimed Coordination Language
- Logical Relations for PCF
- A Correctness Proof for the Volpano/Smith Security Typing System
- Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors