some translation

jfp-paper/jfp-gtt.tex

+\RequirePackage{amsmath}
 \documentclass{jfp1}
 
 \usepackage{amssymb}
@@ -174,6 +175,35 @@ Uniqueness Principles Proofs
   {{\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}
 
+Translation of CBV into CBPV
+
+\begin{mathpar}
+  \inferrule
+  {\Gamma \vdash M : A}
+  {\bvtopv{\Gamma} \vdash \bvtopv{M} : F \bvtopv{A}}
+
+  \inferrule
+  {\Phi \vdash M \ltdyn M' : A \ltdyn A'}
+  {\bvtopv{\Phi} \vdash \bvtopv{M} \ltdyn \bvtopv{M'} : \bvtopv{A} \ltdyn \bvtopv{A'}}
+\end{mathpar}
+
+\begin{align*}
+  \bvtopv{\dyn} &= \dynv\\
+  \bvtopv{1} &= 1\\
+  \bvtopv{(A_1 \times A_2)} &= \bvtopv{A_1} \times \bvtopv{A_2}\\
+  \bvtopv{0} &= 0\\
+  \bvtopv{(A_1 + A_2)} &= \bvtopv{A_1} + \bvtopv{A_2}\\
+  \bvtopv{(A_1 \to A_2)} &= U(\bvtopv{A_1} \to F \bvtopv{A_2})\\ \\
+  \bvtopv{x} &= \ret x\\
+  \bvtopv{(\letXbeYinZ M x N)} &= \bindXtoYinZ {\bvtopv{M}} x {\bvtopv{N}}\\
+  \bvtopv{(\upcast{A}{A'}M)} &= \bindXtoYinZ {\bvtopv{M}} x {\ret \upcast{\bvtopv{A}}{\bvtopv{A'}}x}\\
+  \bvtopv{(\dncast{A}{A'}M)} &= \dncast{F\bvtopv{A}}{F\bvtopv{A'}}M \\
+  \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}
+\end{align*}
+
 %% \label{lastpage}
 
 \end{document}