cbv function uniqueness proof

jfp-paper/jfp-gtt.tex

 \documentclass{jfp1}
 
+\usepackage{amssymb}
+\usepackage{mathpartir}
+\usepackage{tikz-cd}
+\usepackage{environ}
+\usepackage{xcolor}
+
+\input{defs}
+
 \title{Gradual Type Theory}
 
 \author[M.S. New]
@@ -25,6 +33,7 @@
 \pagerange{\pageref{firstpage}--\pageref{lastpage}}
 \doi{S0956796801004857}
 
+
 \newtheorem{lemma}{Lemma}[section]
 
 \begin{document}
@@ -39,6 +48,136 @@
 
 hi
 
-\label{lastpage}
+\section{Call-by-value Gradual Type Theory}
+
+We now present call-by-value Gradual Type Theory, which axiomatizes
+gradual type casts in a call-by-value language. It is based on Moggi's
+computational $\lambda$-calculus $\lambda_c$.
+
+\begin{figure}
+  \begin{mathpar}
+    \begin{array}{rl}
+      A ::= & \colorbox{lightgray}{\dyn} \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 \mid A_1 \to A_2\\
+
+      M ::= & \begin{array}{l}
+        \colorbox{lightgray}{$\upcast{A}{A'} M$}
+        \colorbox{lightgray}{$\dncast{A} {A'} M$}
+        \mid x \\
+        \mid \err_{A} \\
+        \mid \inl{V} \mid \inr{V} \\
+        \mid \abort{V} \mid \caseofXthenYelseZ M {x_1. M_1}{x_2.M_2}\\
+        \mid () \\
+        \mid (V_1,V_2) \\
+        \mid \pmpairWtoinZ M N \mid\pmpairWtoXYinZ M x y N \\
+        \mid \letXbeYinZ{M}{x}{N}\\
+        \mid \lambda x:A.M \mid M\,N\\
+      \end{array}\\
+
+      %% \Gamma ::= & \cdot \mid \Gamma, x : A & 
+      %% \colorbox{lightgray}{$\Phi$} ::= & \colorbox{lightgray}{$\cdot \mid \Phi, x \ltdyn x': A \ltdyn A'$} &
+    \end{array}
+  \end{mathpar}
+  \caption{CBV GTT}
+\end{figure}
+
+\begin{mathpar}
+  \inferrule
+  {\Gamma \vdash M : A \and A \ltdyn A'}
+  {\Gamma \vdash \upcast A {A'} M : A'}
+
+  \inferrule
+  {\Gamma \vdash M : A' \and A \ltdyn A'}
+  {\Gamma \vdash \dncast A {A'} M : A}
+
+  \inferrule
+  {\Phi \vdash M \ltdyn N : A \ltdyn A' \and A' \ltdyn A''}
+  {\Phi \vdash M \ltdyn \upcast{A'}{A''}N : A \ltdyn A''}
+
+  \inferrule
+  {\Phi \vdash M \ltdyn N : A \ltdyn A'' \and A \ltdyn A' \ltdyn A''}
+  {\Phi \vdash \upcast{A}{A'}M \ltdyn N : A' \ltdyn A''}
+
+  \inferrule
+  {\Phi \vdash M \ltdyn N : A' \ltdyn A'' \and A \ltdyn A'}
+  {\Phi \vdash \dncast{A}{A'}M \ltdyn N : A \ltdyn A''}
+
+  \inferrule
+  {\Phi \vdash M \ltdyn N : A \ltdyn A'' \and A \ltdyn A' \ltdyn A''}
+  {\Phi \vdash M \ltdyn \dncast{A'}{A''}N : A \ltdyn A'}
+\end{mathpar}
+
+Uniqueness Principles Proofs
+
+\begin{mathpar}
+  \inferrule
+  {
+  \inferrule
+  {
+  M \ltdyn \letXbeYinZ M f f \and
+  \inferrule
+  {
+  \inferrule
+  {f \ltdyn \lambda x:A_1. f x\and
+  \inferrule
+  {
+  \inferrule
+  {
+  \inferrule
+  {
+  f \ltdyn g, x \ltdyn y \vdash f \ltdyn g\and
+  \inferrule
+  {\inferrule
+  {}
+  {f \ltdyn g, x \ltdyn y \vdash x \ltdyn y}}
+  {f \ltdyn g, x \ltdyn y \vdash x \ltdyn (\dncast{A_1}{A_1'}y)}
+  }
+  {f \ltdyn g, x \ltdyn y \vdash f x \ltdyn g (\dncast{A_1}{A_1'}y)}
+  }
+  {f \ltdyn g, x \ltdyn y \vdash f x \ltdyn \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))}}
+  {f \ltdyn g \vdash \lambda x:A_1. f x \ltdyn {\lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))}}}
+  {f \ltdyn g \vdash f \ltdyn {\lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))}
+  }}
+  {\letXbeYinZ M f f \ltdyn {\letXbeYinZ M g \lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))}}}
+  {M \ltdyn {\letXbeYinZ M g \lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))} : A_1 \to A_2 \ltdyn A_1' \to A_2'}}
+  {\upcast {A_1 \to A_2}{A_1' \to A_2'}M \ltdyn {\letXbeYinZ M g \lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))} : A_1' \to A_2'}
+
+  \inferrule
+  {
+  \inferrule
+  {
+    \inferrule
+    {M \ltdyn M}
+    {M \ltdyn {\upcast {A_1 \to A_2}{A_1' \to A_2'}M}}
+    \and
+    \inferrule
+    {
+    \inferrule
+    {
+    \inferrule
+    {
+    \inferrule
+    {g \ltdyn f, y \vdash g \ltdyn f \and
+    \inferrule
+    {y \ltdyn y}
+    {\dncast{A_1}{A_1'}y \ltdyn y}}
+    {g \ltdyn f, y \vdash g (\dncast{A_1}{A_1'}y) \ltdyn f y}}
+    {g \ltdyn f, y \vdash \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y)) \ltdyn f y}}
+    {g \ltdyn f \vdash \lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y)) \ltdyn \lambda y:A_1'. f y}
+      \and
+      \lambda y:A_1'. f y \ltdyn f
+    }
+    {g \ltdyn f \vdash \lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y)) \ltdyn f}
+  }
+  {{\letXbeYinZ M g \lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))} \ltdyn
+  \letXbeYinZ {\upcast {A_1 \to A_2}{A_1' \to A_2'}M} f f}
+  \and \letXbeYinZ {\upcast {A_1 \to A_2}{A_1' \to A_2'}M} f f \ltdyn {\upcast {A_1 \to A_2}{A_1' \to A_2'}M}}
+  {{\letXbeYinZ M g \lambda y:A_1'. \upcast{A_2}{A_2'}(g (\dncast{A_1}{A_1'}y))} \ltdyn {\upcast {A_1 \to A_2}{A_1' \to A_2'}M} : A_1' \to A_2'}
+\end{mathpar}
+
+%% \label{lastpage}
 
 \end{document}
+
+%% Local Variables:
+%% compile-command: "./latexrun jfp-gtt.tex"
+%% End: