iris.tex 1.85 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}


19
\title{\bfseries The Iris 3.2 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
\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.
Ralf Jung's avatar
Ralf Jung committed
31
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}.
32
33
34
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
\endgroup

\clearpage\begingroup
Ralf Jung's avatar
Ralf Jung committed
40
\section{Iris from the Ground Up}
Ralf Jung's avatar
Ralf Jung committed
41
42
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.
43
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}.
Ralf Jung's avatar
Ralf Jung committed
44
\endgroup
45

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

\end{document}