Ignore:
Timestamp:
Oct 31, 2012, 12:59:12 PM (7 years ago)
Author:
mulligan
Message:

Changes to the file including making a start on incorporating Garrigue's typing rules in to the paper. Also added prooftree.sty to get the paper to compile.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2416 r2424  
    33\smartqed
    44
     5\usepackage{amsmath}
    56\usepackage[english]{babel}
    67\usepackage[colorlinks]{hyperref}
    78\usepackage{listings}
    89\usepackage{microtype}
     10\usepackage{prooftree}
     11
     12\newcommand{\ent}{\vdash}
     13\newcommand{\funarr}{\rightarrow}
     14\newcommand{\lam}[2]{\lambda{#1}.{#2}}
     15\newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}}
     16\newcommand{\pair}[2]{\langle #1, #2 \rangle}
     17\newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}}
    918
    1019\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
     
    118127 \item Bounded vs not-bounded.
    119128\end{itemize}
     129
     130\begin{figure}
     131\begin{gather*}
     132\begin{prooftree}
     133(\Gamma(x) = \phi)
     134\justifies
     135K; \Gamma \ent x : \phi
     136\using\rulefont{{\Gamma}x}
     137\end{prooftree}
     138\qquad
     139\begin{prooftree}
     140K; \Gamma, x : \phi \ent r : \psi
     141\justifies
     142K; \Gamma \ent \lam{x}r : \phi \funarr \psi
     143\using\rulefont{{\Gamma}\lambda}
     144\end{prooftree}
     145\qquad
     146\begin{prooftree}
     147K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi
     148\justifies
     149K;\Gamma \ent rs : \psi
     150\using\rulefont{{\Gamma}rs}
     151\end{prooftree}
     152\\[1.5ex]
     153\begin{prooftree}
     154K; \Gamma \ent r : \phi \quad K; \Gamma, x:\phi \ent s : \psi
     155\justifies
     156K; \Gamma \ent \letin{x}{r}{s} : \psi
     157\using\rulefont{{\Gamma}{:=}}
     158\end{prooftree}
     159\qquad
     160\begin{prooftree}
     161(L \subseteq L' \quad H \subseteq H')
     162\justifies
     163K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'}
     164\using\rulefont{{K}i}
     165\end{prooftree}
     166\end{gather*}
     167\caption{Garrigue's typing relation for polymorphic variants}
     168\label{fig.garrigue.typing.relation}
     169\end{figure}
    120170
    121171%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.