From 8cf7e913dc482a455ed887bc2fa6ef305a0016ea Mon Sep 17 00:00:00 2001
From: Amal Ahmed <amal@ccs.neu.edu>
Date: Mon, 9 Jul 2018 13:20:56 +0200
Subject: [PATCH] figures smaller
---
paper/gtt.tex | 22 ++++++++++++++++++++++
1 file changed, 22 insertions(+)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 4f482eb..8495b51 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -4435,6 +4435,7 @@ a truly dynamically typed style of programming, where one can perform
case-analysis on the dynamic types at runtime, in addition to the type
assertions provided by upcasts and downcasts.
\begin{figure}
+\begin{small}
\begin{mathpar}
\inferrule
{\Gamma\pipe \Delta \vdash V : \dynv\\
@@ -4470,6 +4471,7 @@ assertions provided by upcasts and downcasts.
{\dncast{\dynv\to\dync}{\dync}\bullet}
{\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)
\end{mathpar}
+ \end{small}
\caption{Natural Dynamic Type Extension of GTT}
\end{figure}
@@ -4717,6 +4719,7 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
\end{shortonly}
\begin{figure}
+\begin{small}
\begin{mathpar}
1 \ltdyn \bool\and
A + A \equidyn \bool \times A\and
@@ -4782,6 +4785,7 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
\end{longonly}
\end{mathpar}
+\end{small}
\vspace{-0.4in}
\caption{Scheme-like Extension to GTT}
\label{fig:scheme}
@@ -4894,6 +4898,7 @@ As in previous work, this is proven correct by an analysis of the type
dynamism relation.
\begin{figure}
+\begin{small}
\begin{mathpar}
x:\sem{A} \vdash \sem{\upcast{A}{A'}} : \sem{A'}\and
\bullet:\sem{\u B'} \vdash \sem{\dncast{\u B}{\u B'}} : \sem{\u B}\\
@@ -4961,6 +4966,7 @@ dynamism relation.
\bindXtoYinZ \bullet {x'} \sdncast{\u B}{\u B'}\force x'
\end{array}
\end{mathpar}
+ \end{small}
\caption{Cast to Contract Translation}
\label{fig:cast-to-contract}
\end{figure}
@@ -4979,6 +4985,7 @@ system except the $A \ltdyn \dynv$ and similar $\u B \ltdyn \dync$
rules use the $\dynv, \dync$ are top rules and transitivity.
\begin{figure}
+\begin{small}
\begin{mathpar}
\inferrule
{A \in \{\dynv, 1\}}
@@ -5029,6 +5036,7 @@ rules use the $\dynv, \dync$ are top rules and transitivity.
{A \ltdyn A' \and \u B \ltdyn \u B'}
{A \to \u B \ltdyn A' \to \u B'}
\end{mathpar}
+ \end{small}
\caption{Normalized Type Dynamism Relation}
\label{fig:normalized}
\end{figure}
@@ -6494,6 +6502,7 @@ Dual to the treatment of values, stacks consist only of
\emph{elimination} forms.
\begin{figure}
+\begin{small}
\begin{mathpar}
\begin{array}{lcl}
A & \bnfdef & X \mid \mu X.A \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 \\
@@ -6511,10 +6520,12 @@ Dual to the treatment of values, stacks consist only of
S & ::= & \bullet \mid \bindXtoYinZ S x M \mid S\, V \mid \pi S \mid \pi' S
\end{array}
\end{mathpar}
+ \end{small}
\caption{Operational CBPV Syntax}
\end{figure}
\begin{longfigure}
+\begin{small}
\begin{mathpar}
\inferrule
{}
@@ -6624,10 +6635,12 @@ Dual to the treatment of values, stacks consist only of
{\Gamma \vdash M \ltdyn M' : {\nu \u Y. \u B}}
{\Gamma \vdash \unroll M \ltdyn \unroll M' : \u B[{\nu \u Y. \u B}/\u Y]}
\end{mathpar}
+ \end{small}
\caption{CBPV Inequational Theory (Congruence Rules)}
\end{longfigure}
\begin{longfigure}
+\begin{small}
\begin{mathpar}
\inferrule
{}
@@ -6713,10 +6726,12 @@ Dual to the treatment of values, stacks consist only of
{\Gamma \vdash M : \nu \u Y. \u B}
{\Gamma \vdash M \equidyn \rollty{\nu \u Y.\u B}\unroll M : \nu \u Y. \u B}
\end{mathpar}
+ \end{small}
\caption{CBPV $\beta, \eta$ rules}
\end{longfigure}
\begin{longfigure}
+\begin{small}
\begin{mathpar}
\inferrule
{}
@@ -6775,6 +6790,7 @@ Dual to the treatment of values, stacks consist only of
\Gamma \pipe \u B \vdash S_1 \ltdyn S_2 : \u B'}
{\Gamma \pipe \u B \vdash S_1'[S_1] \ltdyn S_2'[S_2] : \u B''}
\end{mathpar}
+ \end{small}
\caption{CBPV logical and error rules}
\end{longfigure}
@@ -7474,6 +7490,7 @@ defined for terms of type $\cdot \vdash M : \u F (1+1)$, which we
consider to be the type of whole programs.
\begin{figure}
+\begin{small}
\begin{mathpar}
S[\err] \stepzero \err\\
S[\caseofXthenYelseZ{\inl V}{x_1. M_1}{x_2. M_2}] \stepzero S[M_1[V/x_1]]\\
@@ -7496,6 +7513,7 @@ consider to be the type of whole programs.
{M_1 \stepsin{i} M_2 \and M_2 \bigstepsin j M_3}
{M_1 \bigstepsin {i+j} M_3}
\end{mathpar}
+ \end{small}
\caption{CBPV Operational Semantics}
\label{fig:cbpv-operational-semantics}
\end{figure}
@@ -7570,6 +7588,7 @@ And define a typing $C : (\Gamma \vdash \u B) \Rightarrow (\Gamma'
\vdash C[M] : \u B'$ (and similarly for values/stacks).
\begin{longfigure}
+\begin{small}
\begin{mathpar}
\begin{array}{rcl}
C_V & ::= [\cdot] & \rollty{\mu X.A}C_V \mid \inl{C_V} \mid \inr{C_V} \mid \\
@@ -7583,6 +7602,7 @@ And define a typing $C : (\Gamma \vdash \u B) \Rightarrow (\Gamma'
C_S &=& \pi C_S \mid \pi' C_S \mid S\,C_V\mid C_S\,V\mid \bindXtoYinZ {C_S} x M \mid \bindXtoYinZ S x C_M
\end{array}
\end{mathpar}
+ \end{small}
\caption{CBPV Context}
\end{longfigure}
@@ -7848,6 +7868,7 @@ We also get the following ``base case'' of our relation.
\end{longproof}
\begin{figure}
+\begin{small}
\begin{mathpar}
{\itylrof\apreorder{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2
\qquad\qquad\qquad{\itylrof\apreorder{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S
@@ -7872,6 +7893,7 @@ We also get the following ``base case'' of our relation.
S_1 \itylr i {\u F A} S_2 & = & \forall j\leq i, V_1 \itylr j A V_2.~ S_1[\ret V_1] \ix\apreorder j \result(S_2[\ret V_2])
\end{array}
\end{mathpar}
+ \end{small}
\caption{Logical Relation from a Preorder $\apreorder$}
\label{fig:lr}
\end{figure}
--
GitLab