iris.tex 2.11 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
\documentclass[10pt]{article}
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}

\newif\ifslow\slowfalse %\slowtrue
\ifslow
	\usepackage[english]{babel}
	\usepackage[babel=true]{microtype}
\fi
11
\usepackage{geometry}
12
13
14
15
16
17
18

\usepackage[backend=biber]{biblatex}
\bibliography{bib}

\input{setup}


Ralf Jung's avatar
Ralf Jung committed
19
\title{\bfseries The Iris 3.1 Documentation}
Ralf Jung's avatar
Ralf Jung committed
20
\author{\url{http://plv.mpi-sws.org/iris/}}
21
22


23
24
25
26
27
28
29
30
31
32
33
34
\begin{document}

\maketitle
\thispagestyle{empty}
\vfill
\begin{abstract}
This document describes formally the Iris program logic.
Every result in this document has been fully verified in Coq.
The latest versions of this document and the Coq formalization can be found in the git repository at \url{https://gitlab.mpi-sws.org/FP/iris-coq/}.
For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
\end{abstract}

Ralf Jung's avatar
Ralf Jung committed
35
\clearpage\begingroup
36
\tableofcontents
Ralf Jung's avatar
Ralf Jung committed
37
38
39
40
41
42
43
44
45
\endgroup

\clearpage\begingroup
\section{Revision History}
In \citetitle{iris-ground-up}~\cite{iris-ground-up}, we describe Iris~3.1 in a bottom-up way.
That paper is hence much more suited as an introduction to the model of Iris than this reference, which mostly contains definitions, not explanations or examples.
The following differences between Iris as described in \citetitle{iris-ground-up} and the latest version documented here are worth mentioning:
\begin{itemize}
\item As an experimental feature, we added the \emph{plainly modality} $\plainly$.
Ralf Jung's avatar
Ralf Jung committed
46
\item As an experimental feature, weakest preconditions take a \emph{stuckness} $\stuckness$ as parameter, indicating whether the program may get stuck or not.
Ralf Jung's avatar
Ralf Jung committed
47
48
\end{itemize}
\endgroup
49

50
\clearpage\begingroup
51
\input{algebra}
Ralf Jung's avatar
Ralf Jung committed
52
53
\endgroup
\clearpage\begingroup
54
\input{constructions}
Ralf Jung's avatar
Ralf Jung committed
55
56
\endgroup
\clearpage\begingroup
57
\input{base-logic}
Ralf Jung's avatar
Ralf Jung committed
58
59
\endgroup
\clearpage\begingroup
60
\input{model}
Ralf Jung's avatar
Ralf Jung committed
61
62
\endgroup
\clearpage\begingroup
63
\input{ghost-state}
Ralf Jung's avatar
Ralf Jung committed
64
65
\endgroup
\clearpage\begingroup
66
\input{language}
Ralf Jung's avatar
Ralf Jung committed
67
68
\endgroup
\clearpage\begingroup
69
\input{program-logic}
Ralf Jung's avatar
Ralf Jung committed
70
71
\endgroup
\clearpage\begingroup
72
\input{derived}
Ralf Jung's avatar
Ralf Jung committed
73
74
\endgroup
\clearpage\begingroup
75
\input{paradoxes}
Ralf Jung's avatar
Ralf Jung committed
76
77
\endgroup
\clearpage\begingroup
78
\printbibliography
79
\endgroup
80
81

\end{document}