iris.tex 2.11 KB
 Ralf Jung committed Jan 31, 2016 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 Ralf Jung committed Oct 22, 2016 11 \usepackage{geometry} Ralf Jung committed Jan 31, 2016 12 13 14 15 16 17 18 \usepackage[backend=biber]{biblatex} \bibliography{bib} \input{setup} Ralf Jung committed Nov 27, 2017 19 \title{\bfseries The Iris 3.1 Documentation} Ralf Jung committed Oct 22, 2016 20 \author{\url{http://plv.mpi-sws.org/iris/}} Ralf Jung committed Jan 31, 2016 21 22 Ralf Jung committed Oct 22, 2016 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 committed Dec 11, 2017 35 \clearpage\begingroup Ralf Jung committed Jan 31, 2016 36 \tableofcontents Ralf Jung committed Dec 11, 2017 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 committed Dec 12, 2017 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 committed Dec 11, 2017 47 48 \end{itemize} \endgroup Ralf Jung committed Jan 31, 2016 49 Ralf Jung committed Feb 02, 2016 50 \clearpage\begingroup Ralf Jung committed Jan 31, 2016 51 \input{algebra} Ralf Jung committed Dec 11, 2017 52 53 \endgroup \clearpage\begingroup Ralf Jung committed Feb 29, 2016 54 \input{constructions} Ralf Jung committed Dec 11, 2017 55 56 \endgroup \clearpage\begingroup Ralf Jung committed Oct 04, 2016 57 \input{base-logic} Ralf Jung committed Dec 11, 2017 58 59 \endgroup \clearpage\begingroup Ralf Jung committed Mar 12, 2016 60 \input{model} Ralf Jung committed Dec 11, 2017 61 62 \endgroup \clearpage\begingroup Ralf Jung committed Oct 06, 2016 63 \input{ghost-state} Ralf Jung committed Dec 11, 2017 64 65 \endgroup \clearpage\begingroup Robbert Krebbers committed Oct 17, 2016 66 \input{language} Ralf Jung committed Dec 11, 2017 67 68 \endgroup \clearpage\begingroup Ralf Jung committed Oct 04, 2016 69 \input{program-logic} Ralf Jung committed Dec 11, 2017 70 71 \endgroup \clearpage\begingroup Ralf Jung committed Mar 07, 2016 72 \input{derived} Ralf Jung committed Dec 11, 2017 73 74 \endgroup \clearpage\begingroup Ralf Jung committed Jan 23, 2017 75 \input{paradoxes} Ralf Jung committed Dec 11, 2017 76 77 \endgroup \clearpage\begingroup Ralf Jung committed Feb 02, 2016 78 \printbibliography Ralf Jung committed Feb 29, 2016 79 \endgroup Ralf Jung committed Jan 31, 2016 80 81 \end{document}