From 976acd32e27e5513d351442680e8fb5b7fc408b4 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 11 Jul 2018 09:21:50 +0100
Subject: [PATCH] long version citation fixes

---
 paper/gtt.tex | 12 ++++++------
 paper/max.bib | 14 +++++++++++++-
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/paper/gtt.tex b/paper/gtt.tex
index 8e234e5..6b0e848 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1158,7 +1158,7 @@ that can perform effects with the possibility of terminating
   such computations are delayed values.
 \begin{longonly}  
   $U \u F$ is a monad on value
-  types~\citep{moggi}, while $\u F U$ is a comonad on computation types.
+  types~\citep{moggi91}, while $\u F U$ is a comonad on computation types.
 \end{longonly}
 
 \emph{Computation types}
@@ -1987,7 +1987,7 @@ graduality and $\beta,\eta$.
 
 Because the GTT term equidynamism relation $\equidyn$ includes the
 congruence and $\beta\eta$ axioms of the CBPV equational theory, types
-inherit the universal properties they have there~\cite{cpbv}.  We recall
+inherit the universal properties they have there~\cite{levy03cbpvbook}.  We recall
 some relevant definitions and facts.
 
 \begin{definition}[Isomorphism] ~
@@ -2006,7 +2006,7 @@ some relevant definitions and facts.
 \end{definition}
 Note that a value isomorphism is a strong condition, and an isomorphism
 in call-by-value between types $A$ and $A'$ corresponds to a computation
-isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy16popl}.
+isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy17popl}.
 
 \smallskip
 
@@ -2060,7 +2060,7 @@ isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy16popl}.
     %%   doesn't seem to be true?
 \item $\u F 0$ is not \emph{strictly} initial among computation types,
   though.  Proof sketch: a domain model along the lines of
-  \citep{cbn-gtt} with only non-termination and type errors shows this,
+  \citep{newlicata2018-fscd} with only non-termination and type errors shows this,
   because there $\u F 0$ and $\top$ are isomorphic (the same object is
   both initial and terminal), so if $\u F 0$ were strictly initial (any
   type $\u B$ with a stack $\bullet : B \vdash S : \u F 0$ is isomorphic
@@ -6921,7 +6921,7 @@ the same type.
 %% translation of each complex value, e.g.
 %% $\simpp{\caseofXthenYelseZ V {x_1. E_1}{x_2. E_2}} = 
 %%   \bindXtoYinZ {\simp V} x \caseofXthenYelseZ x {x_1. \simp {E_1}}{x_2. \simp {E_2}}$.
-%% We could replace this translation with one as in \cite{levybook} that
+%% We could replace this translation with one as in \cite{levy03cbpvbook} that
 %% introduces fewer administrative redices, but this translation is simpler
 %% and suffices for reasoning up to observational equivalence.
 
@@ -6929,7 +6929,7 @@ the same type.
 The \emph{de-complexification} procedure is defined as follows.
 %
 We note that this translation is not the one presented in
-\cite{levybook}, but rather a more inefficient version that, in CPS
+\cite{levy03cbpvbook}, but rather a more inefficient version that, in CPS
 terminology, introduces many administrative redices.
 %
 Since we are only proving results up to observational equivalence
diff --git a/paper/max.bib b/paper/max.bib
index aac0b7d..af0733e 100644
--- a/paper/max.bib
+++ b/paper/max.bib
@@ -1128,4 +1128,16 @@ pages="396--410",
  title  = {A Spectrum of Type Soundness and Performance},
  booktitle = icfp18,
  year = {2018}
-}
\ No newline at end of file
+}
+
+@inproceedings{nakano,
+  title={A modality for recursion},
+  author={Nakano, Hiroshi},
+  booktitle={Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on},
+}
+@inproceedings{levy17popl,
+ author = {Levy, Paul Blain},
+ title = {Contextual Isomorphisms},
+ booktitle = popl,
+ year={2017},
+} 
\ No newline at end of file
-- 
GitLab