iris.tex

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


\usepackage[english]{babel}
\usepackage[babel=true]{microtype}
\usepackage{geometry}

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

\input{setup}


\title{\bfseries The Iris 4.2~dev Reference}
\author{\url{https://iris-project.org/}}


\begin{document}

\maketitle
\thispagestyle{empty}
\vfill
\begin{abstract}
This document formally describes 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{https://iris-project.org}.
\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.
For a list of changes in Iris since then, please consult our changelog at \url{https://gitlab.mpi-sws.org/iris/iris/blob/master/CHANGELOG.md}.
\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{extended-logic}
\endgroup
\clearpage\begingroup
\input{language}
\endgroup
\clearpage\begingroup
\input{program-logic}
\endgroup
\clearpage\begingroup
\input{derived}
\endgroup
\clearpage\begingroup
\input{paradoxes}
\endgroup
\clearpage\begingroup
\input{heaplang}
\endgroup
\clearpage\begingroup
\printbibliography
\endgroup

\end{document}