### 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

BSD License

### Topics

- Computer science/Programming languages/Type systems

### Session MiniSail

- Nominal-Utils
- Syntax
- IVSubst
- BTVSubst
- Wellformed
- RCLogic
- SyntaxL
- WellformedL
- Typing
- Operational
- SubstMethods
- RCLogicL
- TypingL
- ContextSubtypingL
- IVSubstTypingL
- BTVSubstTypingL
- Safety
- MiniSail

### Depends on

- Native Word
- Nominal 2
- Haskell’s Show Class in Isabelle/HOL

### 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

## Cite

×

MiniSail-AFP

    @article{MiniSail-AFP,
      author  = {Mark Wassell},
      title   = {MiniSail - A kernel language for the ISA specification language SAIL},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/MiniSail.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Jun 25, 2021 : Isabelle2021