From 7170871312035b8ef9bae9d50a476ac1fceda8b3 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Fri, 3 Jan 2020 15:44:54 -0500
Subject: [PATCH] some translation
---
jfp-paper/jfp-gtt.tex | 30 ++++++++++++++++++++++++++++++
1 file changed, 30 insertions(+)
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index d66c61c..10067a4 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -1,3 +1,4 @@
+\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}
--
GitLab