diff -r 9c968d0de9a0 -r 2ce98ee39990 handouts/inferences.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/handouts/inferences.tex	Sat Oct 04 13:17:18 2014 +0100
@@ -0,0 +1,91 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{proof}
+
+\begin{document}
+
+\section*{Inference Rules}
+
+\begin{enumerate}
+\item Frequently used inference rules:
+
+\begin{center}
+\mbox{\infer{F,\Gamma \vdash F}{}}\medskip
+
+\mbox{\infer{\Gamma \vdash F_2}
+            {\Gamma \vdash F_1 \Rightarrow F_2 & \Gamma \vdash F_1}}
+\hspace{10mm}
+\mbox{\infer{\Gamma \vdash F_1 \Rightarrow F_2}
+            {F_1, \Gamma \vdash F_2}}\medskip
+
+\mbox{\infer{\Gamma \vdash P \;\textit{says}\; F}
+            {\Gamma \vdash F}}
+\hspace{10mm}
+\mbox{\infer[\star]{\Gamma \vdash F}
+            {\Gamma \vdash P \;\textit{controls}\; F & \Gamma \vdash P
+              \;\textit{says}\; F}}\medskip
+
+\mbox{\infer{\Gamma \vdash P \;\textit{says}\;F_2}
+            {\Gamma \vdash P \;\textit{says}\; (F_1 \Rightarrow F_2) & 
+             \Gamma \vdash P \;\textit{says}\;F_1}}\medskip
+
+\mbox{\infer{\Gamma \vdash F[x := t]}
+            {\Gamma \vdash \forall x. F}}\medskip
+
+\mbox{\infer{\Gamma \vdash F_1 \wedge F_2}
+            {\Gamma \vdash F_1 & \Gamma \vdash F_2}}
+\hspace{10mm}
+\mbox{\infer{\Gamma \vdash F_1}
+            {\Gamma \vdash F_1 \wedge F_2}}
+\hspace{10mm}
+\mbox{\infer{\Gamma \vdash F_2}
+            {\Gamma \vdash F_1 \wedge F_2}}\medskip
+
+\mbox{\infer[\star]{\Gamma \vdash Q\;\textit{says}\; F}{\Gamma \vdash P\mapsto Q &
+    \Gamma \vdash P\;\textit{says}\; F}}
+\end{center}
+
+\item Less frequently used inference rules:
+
+\begin{center}
+\mbox{\infer{\Gamma \vdash slev(P) < slev(Q)}
+            {\Gamma \vdash slev(P) = l_1 & \Gamma \vdash slev(Q) = l_2 &
+              \Gamma \vdash l_1 < l_2}}\medskip
+
+\mbox{\infer{\Gamma \vdash slev(P) = slev(Q)}
+            {\Gamma \vdash slev(P) = l & \Gamma \vdash slev(Q) = l}}\medskip
+
+\mbox{\infer{\Gamma \vdash l_1 < l_3}
+            {\Gamma \vdash l_1 < l_2 & \Gamma \vdash l_2 < l_3}}\medskip
+
+\mbox{\infer[\star]{\Gamma \vdash P \mapsto R}{\Gamma \vdash P\mapsto Q & \Gamma
+    \vdash Q \mapsto R}}\medskip
+
+
+\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}
+\hspace{5mm}
+\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}
+\hspace{5mm}
+\mbox{\infer{\Gamma \vdash F_3}{\Gamma \vdash F_1 \vee F_2 & F_1, \Gamma
+    \vdash F_3 & F_2, \Gamma \vdash F_3}}\medskip
+
+\mbox{\infer[c\;\mbox{must be a fresh variable}]{\Gamma \vdash \forall
+    x. F}{\Gamma \vdash F[x := c]}}\medskip
+
+\mbox{\infer{\Gamma \vdash \textit{true}}{}}\medskip
+
+\mbox{\infer[\star]{\Gamma \vdash P\;\textit{controls}\; F}{\Gamma \vdash P\mapsto Q
+    & \Gamma \vdash Q\;\textit{controls} F}}
+
+
+\end{center}
+\end{enumerate}
+
+
+$\star$ derived rules
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: