start writing up judgmental structure

main.tex

+\documentclass{article}
+
+\usepackage{amsmath,amssymb}
+\usepackage{tikz-cd}
+\usepackage{mathpartir}
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{definition}{Definition}
+
+\newcommand{\type}{\,\,\text{type}}
+\newcommand{\ctx}{\,\,\text{ctx}}
+\newcommand{\ltdyn}{\sqsubseteq}
+\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
+\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
+
+\newcommand{\Set}{\text{Set}}
+\newcommand{\relto}{\to}
+\newcommand{\M}{\mathcal{M}}
+\newcommand{\sq}{\square}
+\newcommand{\lett}{\text{let}\,\,}
+
+\begin{document}
+\title{Call-by-value Gradual Type Theory}
+\author{Max S. New, Daniel R. Licata and Amal Ahmed}
+\maketitle
+
+\begin{figure}
+  \begin{mathpar}
+    A \type \and
+    \Gamma \ctx\\
+
+    \inferrule
+    {A \type \and A' \type}
+    {A \ltdynv A'}
+
+    \inferrule
+    {A \type \and A' \type}
+    {A \ltdynt A'}\\
+
+    \inferrule
+    {\Gamma \ctx \and A \type}
+    {\Gamma \vdash^v v : A}
+
+    \inferrule
+    {\Gamma \ctx \and A \type}
+    {\Gamma \vdash^T t : A}\\
+
+    \inferrule
+    {\Gamma \ctx\and \Gamma' \ctx}
+    {\Phi_v : \Gamma \ltdynv \Gamma'}
+
+    \inferrule
+    {\Gamma \ctx\and \Gamma' \ctx}
+    {\Phi_t : \Gamma \ltdyn \Gamma'}\\
+
+    \inferrule
+    {\Phi_v : \Gamma \ltdyn \Gamma'\and
+      \Gamma \vdash^v v : A \and
+      \Gamma' \vdash^v v' : A'
+    }
+    {\Phi_v \vdash^v v \ltdynv v' : A \ltdynv A'}
+
+    \inferrule
+    {\Phi : \Gamma \ltdyn \Gamma'\and
+      \Gamma \vdash^T t : A \and
+      \Gamma' \vdash^T t' : A'
+    }
+    {\Phi \vdash^T t \ltdyn t' : A \ltdyn A'}
+  \end{mathpar}
+  \caption{GTTv Judgments and their Pressupositions}
+\end{figure}
+
+\begin{figure}
+  \begin{mathpar}
+    \inferrule{x:A \in \Gamma}
+    {\Gamma \vdash^v x : A}
+
+    \inferrule{\gamma : \pi_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
+      \Gamma \vdash v : B
+    }{\Delta \vdash v[\gamma] : B}
+
+    \inferrule{\gamma : \pi_{x:A \in \Gamma} \Delta \vdash \gamma(x) : A\and
+      \Gamma \vdash t : B
+    }{\Delta \vdash t[\gamma] : B}
+
+    \inferrule{\Gamma \vdash v : A}
+    {\Gamma \vdash \ret v : A}
+
+    \inferrule{\Gamma \vdash t : A\and \Gamma, x : A \vdash u : B}
+    {\Gamma \vdash \lett x = t; u : B}
+
+    \lett x = \ret v; t \cong t[v/x]\\
+    v[\gamma][\delta] = v[\delta \circ \gamma]\\
+    t[\gamma][\delta] = t[\delta \circ \gamma]\
+    v[x/x,\ldots] = v\\
+    t[x/x,\ldots] = t\\
+
+    \lett x = (\lett y = r; s); t \cong \lett y = r; \lett x = s; t\\
+  \end{mathpar}
+  \caption{GTTv Judgmental Term, Value Rules}
+\end{figure}
+
+
+\end{document}
+
+%% Local Variables:
+%% compile-command: "pdflatex main.tex"
+%% End: