Commit f5afe8ce authored by Rene Thiemann's avatar Rene Thiemann
Browse files

metadata and sitegen for MiniSail

parent 336dfa0f0b93
......@@ -10691,3 +10691,21 @@ abstract =
countably many agents. It includes proofs of soundness and
completeness for a variant of the axiom system PA + DIST! + NEC!. The
completeness proof builds on the Epistemic Logic theory.
[MiniSail]
title = MiniSail - A kernel language for the ISA specification language SAIL
author = Mark Wassell <mailto:mpwassell@gmail.com>
topic = Computer science/Programming languages/Type systems
date = 2021-06-18
notify = mpwassell@gmail.com
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.
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>MiniSail - A kernel language for the ISA specification language SAIL - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="../rss.xml">
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax = {
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
processEscapes: true,
svg: {
fontCache: 'global'
}
};
</script>
<script id="MathJax-script" async src="../components/mathjax/es5/tex-mml-chtml.js"></script>
</head>
<body class="mathjax_ignore">
<table width="100%">
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="../index.html">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="../about.html">About</a></td>
</tr>
<tr>
<td class="nav"><a href="../submitting.html">Submission</a></td>
</tr>
<tr>
<td class="nav"><a href="../updating.html">Updating Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../using.html">Using Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../search.html">Search</a></td>
</tr>
<tr>
<td class="nav"><a href="../statistics.html">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="../topics.html">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="../download.html">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">M</font>iniSail
<font class="first">-</font>
<font class="first">A</font>
kernel
language
for
the
<font class="first">I</font>SA
specification
language
<font class="first">S</font>AIL
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">MiniSail - A kernel language for the ISA specification language SAIL</td>
</tr>
<tr>
<td class="datahead">
Author:
</td>
<td class="data">
Mark Wassell (mpwassell /at/ gmail /dot/ com)
</td>
</tr>
<tr>
<td class="datahead">Submission date:</td>
<td class="data">2021-06-18</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
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.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{MiniSail-AFP,
author = {Mark Wassell},
title = {MiniSail - A kernel language for the ISA specification language SAIL},
journal = {Archive of Formal Proofs},
month = jun,
year = 2021,
note = {\url{https://isa-afp.org/entries/MiniSail.html},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td>
</tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Native_Word.html">Native_Word</a>, <a href="Nominal2.html">Nominal2</a>, <a href="Show.html">Show</a> </td></tr>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/MiniSail/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/MiniSail/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/MiniSail/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-MiniSail-current.tar.gz">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
</body>
</html>
\ No newline at end of file
......@@ -158,7 +158,7 @@ added cast operators for default-size words (revision fc1f1fb8dd30)<br></td>
<td class="data"><a href="Word_Lib.html">Word_Lib</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Collections.html">Collections</a>, <a href="Datatype_Order_Generator.html">Datatype_Order_Generator</a>, <a href="Iptables_Semantics.html">Iptables_Semantics</a>, <a href="JinjaThreads.html">JinjaThreads</a>, <a href="Mersenne_Primes.html">Mersenne_Primes</a>, <a href="ROBDD.html">ROBDD</a>, <a href="Separation_Logic_Imperative_HOL.html">Separation_Logic_Imperative_HOL</a>, <a href="WebAssembly.html">WebAssembly</a> </td></tr>
<td class="data"><a href="Collections.html">Collections</a>, <a href="Datatype_Order_Generator.html">Datatype_Order_Generator</a>, <a href="Iptables_Semantics.html">Iptables_Semantics</a>, <a href="JinjaThreads.html">JinjaThreads</a>, <a href="Mersenne_Primes.html">Mersenne_Primes</a>, <a href="MiniSail.html">MiniSail</a>, <a href="ROBDD.html">ROBDD</a>, <a href="Separation_Logic_Imperative_HOL.html">Separation_Logic_Imperative_HOL</a>, <a href="WebAssembly.html">WebAssembly</a> </td></tr>
......
......@@ -149,7 +149,7 @@ HOL/Nominal in the Isabelle distribution.
<td class="data"><a href="FinFun.html">FinFun</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Goedel_HFSet_Semanticless.html">Goedel_HFSet_Semanticless</a>, <a href="Incompleteness.html">Incompleteness</a>, <a href="LambdaAuth.html">LambdaAuth</a>, <a href="Launchbury.html">Launchbury</a>, <a href="Modal_Logics_for_NTS.html">Modal_Logics_for_NTS</a>, <a href="Rewriting_Z.html">Rewriting_Z</a>, <a href="Robinson_Arithmetic.html">Robinson_Arithmetic</a> </td></tr>
<td class="data"><a href="Goedel_HFSet_Semanticless.html">Goedel_HFSet_Semanticless</a>, <a href="Incompleteness.html">Incompleteness</a>, <a href="LambdaAuth.html">LambdaAuth</a>, <a href="Launchbury.html">Launchbury</a>, <a href="MiniSail.html">MiniSail</a>, <a href="Modal_Logics_for_NTS.html">Modal_Logics_for_NTS</a>, <a href="Rewriting_Z.html">Rewriting_Z</a>, <a href="Robinson_Arithmetic.html">Robinson_Arithmetic</a> </td></tr>
......
......@@ -152,7 +152,7 @@ datatypes similar to Haskell's "deriving Show".</td>
<td class="data"><a href="Deriving.html">Deriving</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="CakeML.html">CakeML</a>, <a href="CakeML_Codegen.html">CakeML_Codegen</a>, <a href="Certification_Monads.html">Certification_Monads</a>, <a href="Dict_Construction.html">Dict_Construction</a>, <a href="Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a>, <a href="Monad_Memo_DP.html">Monad_Memo_DP</a>, <a href="Polynomial_Factorization.html">Polynomial_Factorization</a>, <a href="Polynomials.html">Polynomials</a>, <a href="Real_Impl.html">Real_Impl</a>, <a href="XML.html">XML</a> </td></tr>
<td class="data"><a href="Affine_Arithmetic.html">Affine_Arithmetic</a>, <a href="AI_Planning_Languages_Semantics.html">AI_Planning_Languages_Semantics</a>, <a href="CakeML.html">CakeML</a>, <a href="CakeML_Codegen.html">CakeML_Codegen</a>, <a href="Certification_Monads.html">Certification_Monads</a>, <a href="Dict_Construction.html">Dict_Construction</a>, <a href="MiniSail.html">MiniSail</a>, <a href="Modular_arithmetic_LLL_and_HNF_algorithms.html">Modular_arithmetic_LLL_and_HNF_algorithms</a>, <a href="Monad_Memo_DP.html">Monad_Memo_DP</a>, <a href="Polynomial_Factorization.html">Polynomial_Factorization</a>, <a href="Polynomials.html">Polynomials</a>, <a href="Real_Impl.html">Real_Impl</a>, <a href="XML.html">XML</a> </td></tr>
......
......@@ -96,6 +96,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<a href="https://www21.in.tum.de/team/kreuzer/">Katharina Kreuzer</a>
and <a href="https://www21.in.tum.de/~eberlm">Manuel Eberl</a>
</td>
</tr>
<tr>
<td class="entry">
2021-06-18: <a href="entries/MiniSail.html">MiniSail - A kernel language for the ISA specification language SAIL</a>
<br>
Author:
Mark Wassell
</td>
</tr>
<tr>
<td class="entry">
......
......@@ -27,6 +27,24 @@ of the same colour in said interval. The proof goes along the lines of
Waerden&#39;s Theorem is then called the Van der Waerden Number.
Finding the Van der Waerden Number is still an open problem for most
values of $k$ and $l$.</description>
</item>
<item>
<title>MiniSail - A kernel language for the ISA specification language SAIL</title>
<link>https://www.isa-afp.org/entries/MiniSail.html</link>
<guid>https://www.isa-afp.org/entries/MiniSail.html</guid>
<dc:creator> Mark Wassell </dc:creator>
<pubDate>18 Jun 2021 00:00:00 +0000</pubDate>
<description>
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.</description>
</item>
<item>
<title>Public Announcement Logic</title>
......@@ -547,23 +565,5 @@ sets. This last result is used to prove the countable chain condition
for Cohen posets. We work in the set theory framework of Isabelle/ZF,
using the Axiom of Choice as needed.</description>
</item>
<item>
<title>Topological semantics for paraconsistent and paracomplete logics</title>
<link>https://www.isa-afp.org/entries/Topological_Semantics.html</link>
<guid>https://www.isa-afp.org/entries/Topological_Semantics.html</guid>
<dc:creator> David Fuenmayor </dc:creator>
<pubDate>17 Dec 2020 00:00:00 +0000</pubDate>
<description>
We introduce a generalized topological semantics for paraconsistent
and paracomplete logics by drawing upon early works on topological
Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey &amp;
Tarski, etc.). In particular, this work exemplarily illustrates the
shallow semantical embeddings approach (&lt;a
href=&#34;http://dx.doi.org/10.1007/s11787-012-0052-y&#34;&gt;SSE&lt;/a&gt;)
employing the proof assistant Isabelle/HOL. By means of the SSE
technique we can effectively harness theorem provers, model finders
and &#39;hammers&#39; for reasoning with quantified non-classical
logics.</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -393,6 +393,7 @@
<a href="entries/WHATandWHERE_Security.html">WHATandWHERE_Security</a> &nbsp;
<a href="entries/VolpanoSmith.html">VolpanoSmith</a> &nbsp;
<a href="entries/Physical_Quantities.html">Physical_Quantities</a> &nbsp;
<a href="entries/MiniSail.html">MiniSail</a> &nbsp;
<strong>Logics:</strong>
<a href="entries/ConcurrentIMP.html">ConcurrentIMP</a> &nbsp;
<a href="entries/Refine_Monadic.html">Refine_Monadic</a> &nbsp;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment