Merge branch 'master' of github.ccs.neu.edu:coqatoos/cbv-gradual-type-theory

jfp-paper/defs.tex

@@ -165,6 +165,25 @@
 \newcommand\cbvtocbpvty[1]{#1^{ty}}
 \newcommand\purely{\downarrow}
 
+% Stack formatting
+\newenvironment{stackAux}[2]{%
+\setlength{\arraycolsep}{0pt}
+\begin{array}[#1]{#2}}{
+\end{array}\ignorespacesafterend}
+\newenvironment{stackCC}{
+\begin{stackAux}{c}{c}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackCL}{
+\begin{stackAux}{c}{l}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackTL}{
+\begin{stackAux}{t}{l}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackTR}{
+\begin{stackAux}{t}{r}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackBC}{
+\begin{stackAux}{b}{c}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackBL}{
+\begin{stackAux}{b}{l}}{\end{stackAux}\ignorespacesafterend}
+
 %% Local Variables:
 %% compile-command: "./latexrun jfp-gtt.tex"
 %% End:
+

jfp-paper/max.bib

@@ -90,6 +90,10 @@
 @STRING{popl14 =    popl # ", San Diego, California" }
 @STRING{popl15 =    popl # ", Mumbai, India" }
 @STRING{popl16 =    popl # ", St. Petersburg, Florida" }
+@STRING{popl17 =    popl # ", Paris, France" }
+@STRING{popl18 =    popl # ", Los Angeles, California" }
+@STRING{popl19 =    popl # ", Cascais, Portugal" }
+@STRING{popl20 =    popl # ", New Orleans, Louisiana" }
 % ----
 @STRING{icfp =      "{I}nternational {C}onference on {F}unctional {P}rogramming
                     ({ICFP})" }
@@ -124,6 +128,7 @@
 @STRING{oopsla89 =  oopsla }
 @STRING{oopsla98 =  oopsla # ", Vancouver, British Columbia" }
 @STRING{oopsla08 =  oopsla # ", Nashville, Tennessee" }
+@STRING{oopsla12 =  oopsla # ", Tucson, Arizona" }
 % ----
 @STRING{lics =      "IEEE Symposium on Logic in Computer Science (LICS)" }
 @STRING{lics91 =    lics # ", Amsterdam, The Netherlands" }
@@ -771,15 +776,6 @@ year = "2001"}
  year = {2011},
 }
 
-@article{extended,
-  author    = {Max S. New and
-               Daniel R. Licata},
-  title     = {Call-by-name Gradual Type Theory},
-  journal   = {CoRR},
-  year      = {2018},
-  url       = {http://arxiv.org/abs/1802.00061},
-}
-
 @article{newlicata2018-fscd,
   author    = {Max S. New and
                Daniel R. Licata},
@@ -1112,14 +1108,14 @@ pages="396--410",
  advisor = {Reddy, Uday},
  title = {Parametricity As a Notion of Uniformity in Reflexive Graphs},
  year = {2002},
- publisher = {University of Illinois at Urbana-Champaign},
+ school = {University of Illinois at Urbana-Champaign},
  address = {Champaign, IL, USA},
 }
 
 @inproceedings{vitousekswordssiek:2017,
  author = {Vitousek, Michael M. and Swords, Cameron and Siek, Jeremy G.},
  title = {Big Types in Little Runtime: Open-world Soundness and Collaborative Blame for Gradual Type Systems},
- series = {POPL 2017},
+ booktitle=popl17,
  year = {2017},
 } 
 
@@ -1188,7 +1184,7 @@ pages="36--54",
 @inproceedings{greenberg-manifest,
  author = {Greenberg, Michael and Pierce, Benjamin C. and Weirich, Stephanie},
  title = {Contracts Made Manifest},
- series = {POPL '10},
+ booktitle = popl10,
  year = 2010
 }
 
@@ -1210,14 +1206,14 @@ year={2004}
 @inproceedings{chaperonesimpersonators,
  author = {Strickland, T. Stephen and Tobin-Hochstadt, Sam and Findler, Robert Bruce and Flatt, Matthew},
  title = {Chaperones and Impersonators: Run-time Support for Reasonable Interposition},
- series = oopsla,
+ booktitle =oopsla12,
  year = {2012},
 }
 
 @inproceedings{XuPJC09,
  author = {Xu, Dana N. and Peyton Jones, Simon and Claessen, Koen},
  title = {Static Contract Checking for Haskell},
- series = popl09,
+ booktitle = popl09,
  year = {2009},
 }
 
@@ -1236,10 +1232,12 @@ year="2006",
   year      = {2018},
   url       = {http://arxiv.org/abs/1802.00061},
 }
-@Unpublished{newlicataahmed19:extended,
+
+@article{newlicataahmed19:extended,
 author = {Max S. New and Daniel R. Licata and Amal Ahmed},
 title = {Gradual Type Theory (Extend Version)},
 year = {2018},
+journal = {CoRR},
 url = {https://arxiv.org/abs/1811.02440},
 }