MiniSail - A kernel language for the ISA specification language SAIL (Q7361176)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry MiniSail
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | MiniSail - A kernel language for the ISA specification language SAIL |
AFP entry MiniSail |
Statements
18 June 2021
0 references
Mark Wassell
0 references
MiniSail - A kernel language for the ISA specification language SAIL (English)
0 references
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.
0 references
