iris.tex 1.36 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
\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[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry}

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

\input{setup}


Ralf Jung's avatar
Ralf Jung committed
19
\title{\bfseries The Iris 2.0 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
31
32
33
34
35
\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
36
37
\tableofcontents

38
\clearpage\begingroup
39
\input{algebra}
40
\endgroup\clearpage\begingroup
41
\input{constructions}
Ralf Jung's avatar
Ralf Jung committed
42
\endgroup\clearpage\begingroup
43
\input{base-logic}
Ralf Jung's avatar
Ralf Jung committed
44
\endgroup\clearpage\begingroup
45
46
\input{model}
\endgroup\clearpage\begingroup
47
48
\input{ghost-state}
\endgroup\clearpage\begingroup
49
50
\input{language}
\endgroup\clearpage\begingroup
51
52
\input{program-logic}
\endgroup\clearpage\begingroup
53
54
\input{derived}
\endgroup\clearpage\begingroup
55
\printbibliography
56
\endgroup
57
58

\end{document}