From 528a54c6958363c26d339baf347132b7e8d44a3d Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Sat, 23 Feb 2019 11:39:18 -0500
Subject: [PATCH] start adding recursive value types
---
paper/gtt.tex | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index d9c6f24..117cafa 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1045,8 +1045,8 @@ orderings on types and terms.
\[
\begin{array}{l}
\begin{array}{rl|rl}
- A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 &
- \u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
+ A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 & X \mid \mu X. A
+ \u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B \mid \u Y \mid \u \nu \u Y. \u B\\
V ::= & \begin{array}{l}
\colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \abort{V} \\
@@ -1502,6 +1502,10 @@ in the domain~\citep{newahmed18,newlicata2018-fscd}.
\begin{mathpar}
\framebox{$A \ltdyn A'$ and $\u B \ltdyn \u B'$}
+
+ \inferrule{}{A[\mu X.A/X] \ltdyn \mu X. A}
+
+ \inferrule{A[A'/X] \ltdyn A'}{\mu X. A \ltdyn A'}
\inferrule*[lab=VTyRefl]{ }{A \ltdyn A}
--
GitLab