lib/monads: add AFP document setup
Abstract and author list for upcoming AFP entry. Author list is determined separate for each session (ML_Utils, Eisbach_Tools, Monads) by lines added/removed over the repo history. Acknowledgements are from the repo history. The latter might be incomplete, because git has trouble following more than a single file through renames, and these files were renamed a lot. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
ee07f0ccf3
commit
5c021c3789
|
@ -7,6 +7,7 @@
|
||||||
chapter Lib
|
chapter Lib
|
||||||
|
|
||||||
session Monads (lib) = HOL +
|
session Monads (lib) = HOL +
|
||||||
|
options [document = pdf]
|
||||||
|
|
||||||
sessions
|
sessions
|
||||||
"HOL-Library"
|
"HOL-Library"
|
||||||
|
@ -52,3 +53,6 @@ session Monads (lib) = HOL +
|
||||||
Strengthen
|
Strengthen
|
||||||
Nondet_Strengthen_Setup
|
Nondet_Strengthen_Setup
|
||||||
Strengthen_Demo
|
Strengthen_Demo
|
||||||
|
|
||||||
|
document_files
|
||||||
|
"root.tex"
|
||||||
|
|
|
@ -0,0 +1,81 @@
|
||||||
|
%
|
||||||
|
% Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
|
||||||
|
%
|
||||||
|
% SPDX-License-Identifier: CC-BY-SA-4.0
|
||||||
|
%
|
||||||
|
|
||||||
|
\documentclass[11pt,a4paper]{article}
|
||||||
|
\usepackage[T1]{fontenc}
|
||||||
|
\usepackage{isabelle,isabellesym}
|
||||||
|
|
||||||
|
% this should be the last package used
|
||||||
|
\usepackage{pdfsetup}
|
||||||
|
|
||||||
|
% urls in roman style, theory text in math-similar italics
|
||||||
|
\urlstyle{rm}
|
||||||
|
\isabellestyle{tt}
|
||||||
|
|
||||||
|
|
||||||
|
\begin{document}
|
||||||
|
|
||||||
|
\title{State Monad Library}
|
||||||
|
\author{David Greenaway,
|
||||||
|
Gerwin Klein,
|
||||||
|
Corey Lewis,
|
||||||
|
Daniel Matichuk,
|
||||||
|
Thomas Sewell}
|
||||||
|
\maketitle
|
||||||
|
|
||||||
|
\begin{abstract}
|
||||||
|
This entry contains a library of different state monads with a large set of
|
||||||
|
operators, laws, Hoare Logic, weakest precondition rules, and corresponding
|
||||||
|
automation. The formalisation is designed for reasoning about total and
|
||||||
|
partial correctness, as well as for reasoning about failure separately from
|
||||||
|
normal behaviour. Partial correctness in this context ignores program failure.
|
||||||
|
Total correctness implies the absence of program failure.
|
||||||
|
|
||||||
|
The main monads formalised in this entry are a non-deterministic state monad
|
||||||
|
with failure, and a state-based trace monad for modelling concurrent executions.
|
||||||
|
Both support roughly the same set of operators. They come with a standard
|
||||||
|
Hoare Logic and Rely-Guarantee logic respectively. The entry also contains an
|
||||||
|
option reader monad that combines well with the non-deterministic state monad.
|
||||||
|
The option reader monad provides additional operators useful for building
|
||||||
|
state projections that can be used both in monadic functions and Hoare-Logic
|
||||||
|
assertions, enhancing specification re-use in proofs.
|
||||||
|
|
||||||
|
This monad library is used in the verification of the seL4 microkernel and
|
||||||
|
predates some of the monad developments in the Isabelle library. In
|
||||||
|
particular, it defines its own syntax for do-notation, which can be overridden
|
||||||
|
with the generic monad syntax in the Isabelle library. We have opted not to do
|
||||||
|
so by default, because the overloading-based syntax from the Isabelle library
|
||||||
|
often necessitates additional type annotations when mixing different monad
|
||||||
|
types within one specification. For similar reasons, no attempt is made to
|
||||||
|
state generic state monad laws in a type class or locale and then instantiate
|
||||||
|
them for the two main monad instances. The resulting duplication from two
|
||||||
|
instances is still easy to handle, but if more instances are added to this
|
||||||
|
library, additional work on genericity would be useful.
|
||||||
|
|
||||||
|
This library has grown over more than a decade with many substantial
|
||||||
|
contributions. We would specifically like to acknowledge the contributions by
|
||||||
|
Nelson Billing, Andrew Boyton, Matthew Brecknell, David Cock, Matthias Daum,
|
||||||
|
Alejandro Gomez-Londono, Rafal Kolanski, Japheth Lim, Michael McInerney, Toby
|
||||||
|
Murray, Lars Noschinski, Edward Pierzchalski, Sean Seefried, Miki Tanaka, Vernon
|
||||||
|
Tang, and Simon Windwood.
|
||||||
|
\end{abstract}
|
||||||
|
|
||||||
|
\tableofcontents
|
||||||
|
|
||||||
|
\parindent 0pt\parskip 0.5ex
|
||||||
|
|
||||||
|
% generated text of all theories
|
||||||
|
\input{session}
|
||||||
|
|
||||||
|
\bibliographystyle{abbrv}
|
||||||
|
\bibliography{root}
|
||||||
|
|
||||||
|
\end{document}
|
||||||
|
|
||||||
|
%%% Local Variables:
|
||||||
|
%%% mode: latex
|
||||||
|
%%% TeX-master: t
|
||||||
|
%%% End:
|
Loading…
Reference in New Issue