some more cbv gtt

jfp-paper/jfp-gtt.tex

@@ -11,19 +11,19 @@
 
 \title{Gradual Type Theory}
 
-\author[M.S. New]
+\author[M.S. New, D.R. Licata and Amal Ahmed]
        {Max S. New\\
         Northeastern University\\
         %% \email{maxnew@ccs.neu.edu}
        }
 
-\author[D.R. Licata]
+\author[M.S. New, D.R. Licata and Amal Ahmed]
        {Daniel R. Licata \\
         Wesleyan University\\
         %% \email{drlicata@wesleyan.edu}
        }
 
-\author[A. Ahmed]
+\author[M.S. New, D.R. Licata and A. Ahmed]
        {Amal Ahmed \\
         Northeastern University\\
         %% \email{amal@ccs.neu.edu}
@@ -60,15 +60,20 @@ computational $\lambda$-calculus $\lambda_c$.
     \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\\
 
+      V ::= & x \mid \lambda x:A. M
+        \mid \inl{V} \mid \inr{V} \\
+        \mid () \\
+        \mid (V_1,M_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 \inl{M} \mid \inr{M} \\
+        \mid \abort{M} \mid \caseofXthenYelseZ M {\inl x_1. M_1}{\inr x_2.M_2}\\
         \mid () \\
-        \mid (V_1,V_2) \\
+        \mid (V_1,M_2) \\
         \mid \pmpairWtoinZ M N \mid\pmpairWtoXYinZ M x y N \\
         \mid \letXbeYinZ{M}{x}{N}\\
         \mid \lambda x:A.M \mid M\,N\\
@@ -110,20 +115,20 @@ computational $\lambda$-calculus $\lambda_c$.
 Uniqueness Principles Proofs
 
 \begin{mathpar}
-  \inferrule
+  \inferrule*[Right=UL]
   {
-  \inferrule
+  \inferrule*[Right=Trans]
   {
-  M \ltdyn \letXbeYinZ M f f \and
-  \inferrule
-  {
-  \inferrule
+    \inferrule*[Right=Let-Id]{}{M \ltdyn \letXbeYinZ M f f} \and
+  \inferrule*[Right=Let-Cong]
+  {M \ltdyn M \and
+  \inferrule*[Right=Trans]
   {f \ltdyn \lambda x:A_1. f x\and
-  \inferrule
+  \inferrule*[Right=Lam-Cong]
   {
-  \inferrule
+  \inferrule*[Right=UR]
   {
-  \inferrule
+  \inferrule*[Right=App-Cong]
   {
   f \ltdyn g, x \ltdyn y \vdash f \ltdyn g\and
   \inferrule
@@ -182,12 +187,99 @@ Translation of CBV into CBPV
   {\Gamma \vdash M : A}
   {\bvtopv{\Gamma} \vdash \bvtopv{M} : F \bvtopv{A}}
 
+  \inferrule
+  {\Gamma \vdash V : A}
+  {\bvtopv{\Gamma} \vdash \bvtopvpure{M} : \bvtopv A}
+
   \inferrule
   {\Phi \vdash M \ltdyn M' : A \ltdyn A'}
   {\bvtopv{\Phi} \vdash \bvtopv{M} \ltdyn \bvtopv{M'} : \bvtopv{A} \ltdyn \bvtopv{A'}}
+
+  \inferrule
+  {\Phi \vdash V \ltdyn V' : A \ltdyn A'\and}
+  {\bvtopv{\Phi} \vdash \bvtopvpure{V} \ltdyn \bvtopvpure{V'} : \bvtopv{A} \ltdyn \bvtopv{A'}}
+
+  \inferrule
+  {\Gamma \vdash V : A}
+  {\bvtopv\Gamma \vdash \bvtopv{V} \equidyn \ret \bvtopvpure{V} : F \bvtopv{A}}
+
+  \inferrule
+  {\Gamma \vdash V : A \and \Gamma, x:A \vdash M : B}
+  {\bvtopv\Gamma \vdash \bvtopv{(M[V/x])} \equidyn \bvtopv{M}[\bvtopvpure{V}/x] : \bvtopv{B}}
+\end{mathpar}
+
+Order-stuff
+\begin{mathpar}
+  \inferrule
+  {M \ltdyn M' \ltdyn M''}
+  {M \ltdyn M''}
+
+  \inferrule
+  {}
+  {M \ltdyn M}
+
+  \inferrule
+  {x \ltdyn x' \vdash M \ltdyn M' \and V \ltdyn V'}
+  {M[V/x] \ltdyn M'[V'/x']}
+\end{mathpar}
+
+Let-reasoning
+\begin{mathpar}
+  \inferrule
+  {}
+  {\letXbeYinZ M x x \equidyn M}
+
+  \inferrule
+  {x \not\in FV(N)}
+  {\letXbeYinZ M x \letXbeYinZ {M'} {x'} N \equidyn
+    \letXbeYinZ {(\letXbeYinZ M x M')} {x'} N
+  }
+
+  \inferrule
+  {}
+  {\letXbeYinZ V x M \equidyn M[V/x]}
+\end{mathpar}
+
+Evaluation Order Rules
+\begin{mathpar}
+  \inferrule
+  {}
+  {M\,N \equidyn \letXbeYinZ M f \letXbeYinZ N x f\,x}
+
+  \inferrule
+  {}
+  {\pmpairWtoinZ M N \equidyn \letXbeYinZ M z \pmpairWtoinZ z N}
+
+  \inferrule
+  {}
+  {(M,N) \equidyn \letXbeYinZ M x \letXbeYinZ N y (x,y)}
+
+  \inferrule
+  {}
+  {\pmpairWtoXYinZ M x y N \equidyn \letXbeYinZ M z \pmpairWtoXYinZ z x y N}
+
+  \inferrule
+  {}
+  {\inl M \equidyn \letXbeYinZ M z \inl z}
+
+  \inferrule
+  {}
+  {\inr M \equidyn \letXbeYinZ M z \inr z}
+
+  \inferrule
+  {}
+  {\caseofXthenYelseZ M {\inl x_1. N_1}{\inr x_2. N_2}
+    \equidyn \letXbeYinZ M z \caseofXthenYelseZ z {\inl x_1. N_1}{\inr x_2. N_2}
+  }
+\end{mathpar}
+
+$\beta\eta$ Rules
+\begin{mathpar}
+  
 \end{mathpar}
 
 \begin{align*}
+  \bvtopv{(x_0:A_0,\ldots)} &= x_0:\bvtopv{A_0},\ldots\\
   \bvtopv{\dyn} &= \dynv\\
   \bvtopv{1} &= 1\\
   \bvtopv{(A_1 \times A_2)} &= \bvtopv{A_1} \times \bvtopv{A_2}\\
@@ -201,9 +293,17 @@ Translation of CBV into CBPV
   \bvtopv{(\lambda x:A. M)} &= \ret \thunk {\lambda x:\bvtopv{A}. \bvtopv{M}}\\
   \bvtopv{(M \, N)} &= \bindXtoYinZ {\bvtopv{M}} f \bindXtoYinZ {\bvtopv{N}} x {(\force f)\, x}\\
   \bvtopv{(M_1,M_2)} &= \bindXtoYinZ {\bvtopv{M_1}} {x_1} \bindXtoYinZ {\bvtopv{M_2}} {x_2}  \ret (x_1,x_2)\\
-  \bvtopv{\pmpairWtoXYinZ M {x_1}{x_2} N} &= \bindXtoYinZ {\bvtopv M} x \pmpairWtoXYinZ x {x_1}{x_2} {\bvtopv N}
+  \bvtopv{\pmpairWtoXYinZ M {x_1}{x_2} N} &= \bindXtoYinZ {\bvtopv M} x \pmpairWtoXYinZ x {x_1}{x_2} {\bvtopv N}\\\\
+  \bvtopvpure{x} &= x\\
+  \bvtopvpure{(\lambda x:A. M)} &= \thunk {\lambda x:\bvtopv{A}. \bvtopv{M}}\\
+  \bvtopvpure{(\inl V)} &= \inl \bvtopvpure {V}\\
+  \bvtopvpure{(\inr V)} &= \inl \bvtopvpure {V}\\
+  \bvtopvpure{(V_1,V_2)} &= (\bvtopvpure{V_1}, \bvtopvpure{V_2})\\
 \end{align*}
 
+%% List of Types:
+%% ?, ->, 1, *, 0, +
+
 %% \label{lastpage}
 
 \end{document}