iris.tex

\documentclass[10pt]{article}
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}

\newif\ifslow\slowfalse %\slowtrue
\ifslow
	\usepackage[english]{babel}
	\usepackage[babel=true]{microtype}
\fi
\usepackage{geometry}

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

\input{setup}


\title{\bfseries The Iris 3.1 Documentation}
\author{\url{http://plv.mpi-sws.org/iris/}}


\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/iris/iris}.
For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
\end{abstract}

\clearpage\begingroup
\tableofcontents
\endgroup

\clearpage\begingroup
\section{Iris from the Ground Up}
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$.
\item As an experimental feature, weakest preconditions take a \emph{stuckness} $\stuckness$ as parameter, indicating whether the program may get stuck or not.
\end{itemize}
\endgroup

\clearpage\begingroup
\input{algebra}
\endgroup
\clearpage\begingroup
\input{constructions}
\endgroup
\clearpage\begingroup
\input{base-logic}
\endgroup
\clearpage\begingroup
\input{model}
\endgroup
\clearpage\begingroup
\input{ghost-state}
\endgroup
\clearpage\begingroup
\input{language}
\endgroup
\clearpage\begingroup
\input{program-logic}
\endgroup
\clearpage\begingroup
\input{derived}
\endgroup
\clearpage\begingroup
\input{paradoxes}
\endgroup
\clearpage\begingroup
\printbibliography
\endgroup

\end{document}