Skip to content
Snippets Groups Projects
iris.tex 1.36 KiB
Newer Older
\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[backend=biber]{biblatex}
\bibliography{bib}

\input{setup}


\title{\bfseries The Iris 3.0 Documentation}
Ralf Jung's avatar
Ralf Jung committed
\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/FP/iris-coq/}.
For further information, visit the Iris project website at \url{http://plv.mpi-sws.org/iris/}.
\end{abstract}

\clearpage
\clearpage\begingroup
\endgroup\clearpage\begingroup
Ralf Jung's avatar
Ralf Jung committed
\endgroup\clearpage\begingroup
\input{base-logic}
Ralf Jung's avatar
Ralf Jung committed
\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